…and is now being taught in combined “Formal Real Analysis”[1] courses to undergrads, and the lean prover community has a joint project to formalize the proof of Fermat’s Last Theorem, which is a lot of work but is progressing. It’s sort of weird to say there is no progress. It seems to me when you have a fields medal winner publishing lean4 formal proofs on github[2] to go with one of his books you are making a lot of progress.
alt Hacker News
…and is now being taught in combined “Formal Real Analysis”[1] courses to undergrads, and the lean prover community has a joint project to formalize the proof of Fermat’s Last Theorem, which is a lot of work but is progressing. It’s sort of weird to say there is no progress. It seems to me when you have a fields medal winner publishing lean4 formal proofs on github[2] to go with one of his books you are making a lot of progress.
[1] eg https://youtube.com/playlist?list=PLs6rMe3K87LHu03WWh9rEbEhh...
[2] https://github.com/teorth/analysis