Lean proof of Fermat's Last Theorem [pdf]

Re:Lean proof of Fermat's Last Theorem [pdf] by cubefox on Wednesday August 20, 2025 @03:36PM (#44965503)

> At the time of writing, these notes do not contain anywhere near a proof of FLT, or even a sketch proof. Over the next few years, we will be building parts of the argument, following a strategy constructed by Taylor, taking into account Buzzard’s comments on what would be easy or hard to do in Lean.

So the title of the paper is misleading at this time.

[ Parent | on HN ]

Re:Lean proof of Fermat's Last Theorem [pdf] by kevinbuzzard on Wednesday August 20, 2025 @04:04PM (#44965844)

That is correct, the title is currently misleading (arguably the title of every paper I ever wrote was misleading just after I wrote the title, I guess). If you are interested in seeing more details of the proof I'll be following, they are here https://web.stanford.edu/~dkim04/automorphy-lifting/ . This is a Stanford course Taylor gave this year on a "2025 proof of FLT".

[ Parent | on HN ]

Re:Lean proof of Fermat's Last Theorem [pdf] by golol on Wednesday August 20, 2025 @04:13PM (#44965926)

Hey Mr. Buzzard I want to say I find your work and enthusiasm with Lean and formalization very cool.

[ Parent | on HN ]