So I'm two months into trying to teach a proof of Fermat's Last Theorem to a computer. We already have one interesting story, which I felt was worth sharing.
So I'm two months into trying to teach a proof of Fermat's Last Theorem (FLT) to a computer. Most of "how it's going" is quite tedious and technical to explain: to cut a long story short, Wiles proved an "R=T" theorem and much of the work so far has gone into teaching the computer what R and T are; we still have not finished either definition. However my PhD student Andrew Yang has already proved the abstract commutative algebra result which we need ("if abstract rings R and T satisfy lots of technical conditions then they're equal"), and this is an exciting first step. The current state of the write-up is here, and the system we are using is Lean and its mathematical library mathlib, maintained by the Lean prover community. If you know a bit of Lean and a bit of number theory then feel free to read the contribution guidelines, checkout the project dashboard and claim an issue. As I say, we're two months in. However we already have one interesting story, which I felt was worth sharing. Who knows if it's an indication of what is to come. We're not formalising the old-fashioned 1990s proof of FLT. Since then, work of many people (Diamond/Fujiwara, Kisin, Taylor, Scholze and several others) led to the proof being generalised and simplified, and part of the motivation of my work is not to just get FLT over the line but to prove these more general and powerful results. Why? Because if the AI mathematics revolution actually happens (which it might) and if Lean turns out to be an important component (which it might) then computers will be in a better position to start helping humans to push back the boundaries of modern number theory because of this formalization work, as they'll have access to key modern definitions in a form which they understand. One concept which was not used in Wiles' original proof but which is being used in the proof we're formalizing, is crystalline cohomology, a theory developed in the 60s and 70s in Paris, with the foundations laid down by…