This is the Lean blueprint for the project, which is a human-readable "plan" more or less. The actual Lean proof is ongoing, and will probably take a few more years. Still cool though.
> 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.
Slightly misleading title- this is the overall blueprint for a large ongoing effort by the Imperial College London to formalize FLT in Lean, not the proof itself (which is huge).
The project webpage has more information about the efforts and how to contribute:
> In the words of mathematical historian Howard Eves, "Fermat's Last Theorem has the peculiar distinction of being the mathematical problem for which the greatest number of incorrect proofs have been published."
I'm not an expert but I'd say based on my experience with Lean so far, the answer is yes. eg. I have entered some proofs from the Lean guide and then replaced tactics with `apply?` which searches for tactics to meet the goal, and eg. reduced this example from the guide:
theorem and_commutative (p q : Prop) : p ∧ q → q ∧ p :=
fun hpq : p ∧ q =>
have hp : p := And.left hpq
have hq : q := And.right hpq
show q ∧ p from And.intro hq hp
To this:
theorem and_commutative' (p q : Prop) : p ∧ q → q ∧ p := by
exact fun a ↦ id (And.symm a)
Presumably the same thing could be done for each part of a more complicated proof and could be done so at each step automatically.
I know nothing about theorem provers. Is the idea that you can prove a large number of simpler statements that build on each other until it all implies the top level theorem you're proving (like how IRL math works)? That way you don't have to understand the gargantuan computer program all at once?
It just seems like it would be as hard to verify the accuracy of the code written to prove a complex theorem like FLT as a manuscript written in English. But if you can rely on smaller statements that build on each other, it would make more sense.
I am assuming you mean it's a bigger concern in Lean than other languages because of what people are attempting to do with it (formalize all of math)? Because the language itself, somewhat by design and somewhat by nature, seems to be more future proof than any other language I've ever used.
I think an important thing for something like Lean to gain traction is the availability of learning resources (math 'textbooks') based on the technology so people actually use it for day to day mathematics instead of just formalizing what has already been proven without it.
I don't think many people are going to read Rudin (etc.) then try to rewrite the book or do the exercises in Lean by themselves or read through the mathlib files to see how everything is defined/proved in full generality.
Like a lot of people (I imagine), I'm not a professional mathematician working on advanced, complex problems but I would like to have the ability to have the computer check my solutions to exercises and maybe even aid me with hints for tackling problems if needed.
If math textbooks gave free use for people to rewrite them into computer format and post online it would make life a lot easier.
Yes I am aware of this one, it seems like a good intro.
I am just thinking more along the lines of - other than times where a computer is not available to us, why do we keep using traditional notion/pen and paper at all?
If everything is digitalized no one will have mark homework ever again.
I still don’t understand the excitement here other than it’s related to computers. Will formalizing it make it easier for us to understand the core ideas or arguments? I don’t think it will - that would best be done by reading Wile’s paper which is written with that goal in mind.
Given that it was a research frontier where arguments assume an educated audience, it's probably very difficult to formalize.
Question for the organizers: Is there an inactivity timeout on claimed sub-problems? Say someone “claims” a task and then goes quiet, others hold back; but without claims, you risk duplicate effort, right? How do you balance that?
If there’s a policy already, what counts as “active”? A short status note, a link to a draft, or partial results? If not, would you consider a lightweight scheme:
Soft claim (one task per person);
progress update within 7–14 days (longer for big items);
auto-release if no update;
extensions on request;
Tag some tasks as “pairable” so two people can collaborate openly.
Curious how you’re handling throughput vs inclusion here.
Section #7 is on the Langlands Conjectures. "Conjetures in a proof blueprint?" Curious about the role in the proof.
"The { Wiles } modularity theorem { that cracked FLT } is a special case of more general conjectures due to Robert Langlands. The Langlands program seeks to attach an automorphic form or automorphic representation (a suitable generalization of a modular form) to more general objects of arithmetic algebraic geometry, such as to every elliptic curve over a number field. Most cases of these extended conjectures have not yet been proved. (https://tinyurl.com/yc6kth2m)"
New math is emerging "as we speak" from the group of Gaitsgory (https://tinyurl.com/9r5bsufj), but apply to the (differential) geometric Langlands area, while the quote looks about the algebraic-geometry area (of Weil's triple Rosetta Stone). Yet areas have well understood connections. Both kind of works (new math and formalizing) are very needed. Verifiable proofs have to help to avoid math building collapsing under own weight/richness.
22 comments
[ 2.9 ms ] story [ 46.9 ms ] threadSo the title of the paper is misleading at this time.
The project webpage has more information about the efforts and how to contribute:
https://imperialcollegelondon.github.io/FLT/
Is the consensus that he never had the proof (he was wrong or was joking) -- or that it's possible we just never found the one he had?
It just seems like it would be as hard to verify the accuracy of the code written to prove a complex theorem like FLT as a manuscript written in English. But if you can rely on smaller statements that build on each other, it would make more sense.
I don't think many people are going to read Rudin (etc.) then try to rewrite the book or do the exercises in Lean by themselves or read through the mathlib files to see how everything is defined/proved in full generality.
Like a lot of people (I imagine), I'm not a professional mathematician working on advanced, complex problems but I would like to have the ability to have the computer check my solutions to exercises and maybe even aid me with hints for tackling problems if needed.
If math textbooks gave free use for people to rewrite them into computer format and post online it would make life a lot easier.
https://leanprover-community.github.io/learn.html
I am just thinking more along the lines of - other than times where a computer is not available to us, why do we keep using traditional notion/pen and paper at all?
If everything is digitalized no one will have mark homework ever again.
Given that it was a research frontier where arguments assume an educated audience, it's probably very difficult to formalize.
Soft claim (one task per person); progress update within 7–14 days (longer for big items); auto-release if no update; extensions on request; Tag some tasks as “pairable” so two people can collaborate openly.
Curious how you’re handling throughput vs inclusion here.
"The { Wiles } modularity theorem { that cracked FLT } is a special case of more general conjectures due to Robert Langlands. The Langlands program seeks to attach an automorphic form or automorphic representation (a suitable generalization of a modular form) to more general objects of arithmetic algebraic geometry, such as to every elliptic curve over a number field. Most cases of these extended conjectures have not yet been proved. (https://tinyurl.com/yc6kth2m)"
New math is emerging "as we speak" from the group of Gaitsgory (https://tinyurl.com/9r5bsufj), but apply to the (differential) geometric Langlands area, while the quote looks about the algebraic-geometry area (of Weil's triple Rosetta Stone). Yet areas have well understood connections. Both kind of works (new math and formalizing) are very needed. Verifiable proofs have to help to avoid math building collapsing under own weight/richness.