| ▲ | seanhunter 3 days ago | |
…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... | ||