"Anatomy of a Formal Proof"

[dmm]

A really nice Lean tutorial: arxiv.org/abs/2411.11885

Comments

[dmm]

The use of AI is not covered (AI is mentioned in Conclusion).

[dmm]

Tangentially related: "The Provability of Consistency"

https://x.com/davidad/status/1201824427391893504

> It turns out Peano Arithmetic *can* prove its own consistency, using a slightly different operationalization of “consistency” than Gödel’s—one which does seem closer to what Hilbert really meant.

https://arxiv.org/abs/1902.07404

by https://en.wikipedia.org/wiki/Sergei_N._Artemov

[anhinga_anhinga]

test