Will FLT be formalized soon?

Stream: new members

[Lars Ericson]

Thank you @Oisin McGuinness, @Kevin Buzzard and @Junyan Xu for the category theory links, I will study these.

Terry Tao has a new post on "AI Anthology". I put a bunch of Lean-related ChatGPT sessions I did in the comments. I asked various ChatGPTs for the axioms of category theory and entered some long dialogues. I also asked for theorems in math that use category theory but aren't about category theory, and got a good list.

On the 3rd day of the NSF webinar they had an AMS guy speak. On day 2 I think someone showed a project that generates English text from Lean proofs. It occurred to me to ask if AMS would publish Lean proofs directly or as mechanically-produced English translations (so, stylized in an unambiguous way), and encourage people to supply Lean proofs to formally verify new results. I didn't hear the moderator pass this question on (though it was 1 of exactly 2 for that session in the chat, and got upvoted 4x), but I think it's a good idea that would align the interests of pure blackboard mathematicians and interactive theorem proving people. Mathematicians use LaTeX every day to write up proofs, either directly or in markup language that supports MathJax. So that is a model for blackboard mathematicians adopting software in their daily methodology. To me it seems a very easy stretch of the imagination to add Lean to that day-to-day. Someone used the metaphor of building a proof in Lean as "programming" the proof, so an activity like programming. Applied mathematicians write code all the time. It's not too much of a stretch to imagine LaTeX-using blackboard mathematicians programming their proofs. Also noted by Ursula Martin was the problem of "weasel words" in proofs: Complicated constructions alluded to with phrases like "analogous to". She pointed to Wiles' proof of FLT. The proof of FLT in blackboard format was not accepted for several years after publication. Weasel words would be eliminated and proof acceptance would be immediate if Wiles programmed his proofs in Lean. To stir the pot I encouraged Terry Tao to take on FLT in Lean in the comments on his post on the NSF webinar, suggesting it would take him only 2 weeks to polish it off.

[Johan Commelin]

I think that suggestion to Tao is not helpful in any sense.

[Kevin Buzzard]

Agreed :-/

[Jireh Loreaux]

two weeks ... :question::exclamation::rofl:

[Johan Commelin]

@Lars Ericson Are you intentionally trying to be provocative?

[Jireh Loreaux]

@Lars Ericson I think you have several misconceptions about formal verification. For example, "A formally verified proof would take 0 years and 0 faith to accept" is false. For a detailed explanation, see my post in another thread.

Moreover, the idea that anyone alone (or even a team) could crank out a formally verified proof of FLT in two weeks (at this point in time) is ludicrous. Do you have experience with formalization? How long did it take you to formalize something simple? Something complex?

Does it matter if no single person has the entire proof of FLT in their heads? This is what writing is for after all. And how would formalizing it in Lean change this?

[Jireh Loreaux]

In fairness, because the statement of FLT involves such simple objects (ℕ with ^ and + and <), a formally verified proof would be accepted quickly, but it is folly to think that nothing in formal verification requires human checking.

[Matthew Ballard]

I have discovered a truly marvelous formalization of this proposition which my editor buffer is too small to contain!

[Jireh Loreaux]

"Look ma, I found Fermat's original proof of FLT! What's that? Oh, ignore that default instance I placed somewhere in 500 files worth of Lean code. The proof is really fun." (sorry, I couldn't resist)

import Mathlib.Data.Nat.Basic

@[default_instance 500000]
instance foo : Pow ℕ ℕ where
  pow _ _ := 1

theorem FLT (n x y z : ℕ)
    (_hx : x ≠ 0) (_hy : y ≠ 0) (_hz : z ≠ 0) (_hn : 3 ≤ n) :
    x ^ n + y ^ n ≠ z ^ n :=
  fun.

Lars, this is what I mean by you have to trust definitions. Note that by all appearances, this looks like an (albeit too simple) proof of FLT.

[Jireh Loreaux]

It would be even more surreptitious if you made this a scoped instance in the FLT namespace, and then at the top you just do open scoped FLT.

[Oliver Nash]

Even more evil things are possible:

example : 12^3 - (10^3 + 9^3) = 0 := rfl

[Jireh Loreaux]

Haha, you disproved FLT!

[Kyle Miller]

Hey @Jireh Loreaux, I have priority on that proof of FLT! :upside_down: (Kevin had posted a "99.9% of adults can't solve this level of a logic puzzle game!" tweet for FLT, but the nat pow instances had just moved from core Lean 3 to mathlib, so the puzzle was accidentally broken -- or maybe the real puzzle was to find the right nat pow instance to be able to win :smile:). I suppose since you're second, if we apply the naming rule from logic, this is "Jireh's theorem."

[Jireh Loreaux]

True, but after 100 years we rename it to the Loreaux-Miller theorem. There's no credit like posthumous credit!

[Kyle Miller]

Don't mind the macro rules, FLT really was trivial after all:

import Mathlib.Data.Nat.Basic

macro_rules
  | `(command| theorem FLT $_:bracketedBinder $[$_:bracketedBinder]* : $_ := $pf) =>
    `(command| theorem $(Lean.mkIdent `FLT) : True := $pf)

theorem FLT (n x y z : ℕ)
    (_hx : x ≠ 0) (_hy : y ≠ 0) (_hz : z ≠ 0) (_hn : 3 ≤ n) :
    x ^ n + y ^ n ≠ z ^ n := by
  trivial

#print axioms FLT
/- 'FLT' does not depend on any axioms -/

[Lars Ericson]

A factoid mentioned here is the idea that FLT is so deep and dependent on such broad swaths of mathematics that no one person could possibly have the entire proof in their head. Countering that belief, another conference participant said, in the conference chat, that it was not a matter of limited brain capacity, but rather that of building up a big enough pile of definitions to make the top level expression of the proof more compact.

As @Jireh Loreaux pointed out, there will not be 0 time to acceptance and 0 time to verify for a machine-verified proof. However, the act of coding and checking the proof will concentrate terms to be checked manually. Ursula Martin singled out the use of the phrase "analogous to" in Wiles' proof. Wiles uses the word "analogous" 11 times in the proof, for example "Analogous definitions apply ", "The proof of the following proposition is analogous (but simpler) to the proof of", "defined analogously to" and so on. Martin was claiming, I think, that every use of the word "analogous" corresponds to a hard construction that was elided from the proof. Perhaps these analogies could be coded as functors on categories, or in some other way made more "one step" in the sense that the word "analogous" promises a direct translation. The acceptance of the proof currently comes from multiple mathematicians with Wiles' training and aptitude doing those constructions either in their head or on paper to their own satisfaction, and nobody finding a counterexample. Assuming that no one mathematician can have all the details in their head, it is a crowdsourced acceptance, based on faith in the crowd.

As to the "2 weeks". According to UCLA, Tao is the Mozart of Math. The best there is. While Tao has been active in organizing conferences like the one we are discussing and the IPAM Machine Assisted Proofs workshop, I have not found posts or publications by him where he discusses actually doing a proof on his own in an interactive theorem prover or otherwise going through available training from @Kevin Buzzard.

If Tao trained to learn to read and code proofs to the level of the most difficult proofs in Lean, it is not unreasonable or provocative to expect that he could code FLT in much less time than anybody reading this thread. Maybe not 2 weeks, but maybe much faster than the current assessment of say around 2030 for a team. And maybe he wouldn't need a team. Wiles didn't need a team. It's really a matter of whether he is comfortable and fluent in FLT, more than anybody else, and comfortable and fluent in Lean, as much as the readers of this thread are. It may be unreasonable and provocative to expect that Tao could get as good at Lean as the people on this thread. But I wouldn't bet against him.

It is reasonable to expect that Tao is already or will be consulted for opinions on what kind of proof verification research to fund. I am 100% certain that he will make better funding recommendations if he knows how to translate paper proofs into Lean proofs. I don't think he will take my word for it that he can get it done in 2 weeks. Maybe he will give up after 2 weeks like this person who tried to translate Tao's Real Analysis textbook into Lean. If he takes the challenge, whether or not he gives up, I definitely, sincerely and unprovocatively think he will have a much better idea of both how useful and how hard interactive proof verification technology is, if he sits down and gives it a go anyway. This pragmatic experience will make his funding recommendations much much more relevant.

[Johan Commelin]

You still have no clue of the complexity of the proof of FLT. Here is a thought experiment: suppose you have to write a detailed proof of FLT in ordinary mathematical English, and suppose that you are allowed to take for granted any definition and theorem that has been formalized in any proof assistant (Coq/Isabelle/Mizar/Metamath/Lean/etc...). You are also allowed to consult any library in the world, and ask questions to experts by email. They are guaranteed to reply in < 1 minute.

Then I claim that nobody can get this done in 2 weeks. Simply because there will be too much text to type in. You will have to "copy" by hand several thousands of pages of mathematical english. I think nobody can write 100 pages of mathematical English per day for 14 days in a row. And even if you could, that wouldn't be enough.

The takeaway of my message is not that Tao can't formalize FLT in Lean in 2 weeks (that's just a corollary).
The takeaway is that all your experiments with GPT still haven't given you the slightest sense of what the proof of FLT looks like and how complex it is.

[Kyle Miller]

I heard it took the Mozart of Music about 6 weeks to compose his last three symphonies, which consist of about 200 pages total for the scores, and he probably went into it with a fairly developed ideas. I don't think writing symphonies and formalizing math are very comparable, but I can say 200 is less than thousands and 6 is more than 2.

[Kyle Miller]

Even Stephen King, the prolific author, only writes 6 paperback novel pages (of 300 words each) per day, and these don't have to hold up to any sort of formal verification.

[Joseph Myers]

It's commonly claimed (and also disputed) that some programmers are ten times more productive than others. This might very well apply to formalization as well: some people may be ten times faster than others. But if it does, getting ultra-productive formalizers working on FLT would be making the difference between 500 person-years and 50 person-years, or 100 person-years and 10 person-years; 2 weeks is still orders of magnitude too small.

[Notification Bot]

20 messages were moved here from #Machine Learning for Theorem Proving > AI in math reasoning conference by Scott Morrison.

[Ben Nale]

@Lars Ericson how did you come up with two weeks? Why not 1 week? Or better ... 2 days?

[Lars Ericson]

Maybe it's not possible in any weeks. I've heard here a fairly strong Yes vote to the idea that, given enough time, FLT can be expressed in ZFC and PA. I did a ChatGPT search on the question "Does Wiles' proof of Fermat's Last Theorem require large cardinals?" Colin McClarty 2010 and Laura Fontanella 2019 say Yes. Thomas Scanlon 2021 and Alexander Razborov 2022 say No. McClarty 2023 says Yes again. The question reduces to whether semistable elliptic curves can be constructed without using Grothendieck's universes.

[Jason Rute]

Colin McClarty 2010 and Laura Fontanella 2019 say Yes. Thomas Scanlon 2021 and Alexander Razborov 2022 say No. McClarty 2023 says Yes again.yy

Please tell me you looked up these references before parroting sometime ChatGPT said!

[Jason Rute]

Also to be clear, you can use universes (or large cardinals) in Lean as Lean’s logic can handle them. (And you certainly don’t need to worry about finding a proof in PA.)

[Jason Rute]

The challenge with FLT is that it is a difficult and large theorem (so much so that Kevin says no one can hold it in their head) which also depends on a lot of background mathematics from across the spectrum of math.

[Jason Rute]

Formalization is time consuming, and it is even more so if the math is less well understood or if the background material isn’t already formalized.

[Lars Ericson]

McClarty 2010:

"Wiles explains how his search for the proof was blocked at one point by a specific problem of arithmetic. He says "the turning point in this and indeed in the whole proof came" when the search led him to two cohomology invariants and "I learned that it followed from Tate's account of Grothendieck duality theory for complete intersections that these two invariants were equal" [Wiles, 1995, p. 451]. The body of the proof (pp. 486-7) cites a source: "For a summary of the duality statements used in this context, see [Mazur, 1977, ?11.3].... To justify the reduction in detail see the arguments in [Mazur, 1977, ?11.3]." Mazur does not give complete proofs but cites Grothendieck and Dieudonne [ 1961 ] which we abbreviate EGA III, and Deligne and Rapoport [ 1973] which cites the same parts of EGA III. Grothendieck and Dieudonne use functor categories between locally small categories (p. 349). From the view point of ZFC these locally small categories are proper classes. A function between proper classes is a proper class, so any "set" of functions between two proper classes is a collection of proper classes. Let us call such a collection a superclass. If we are concerned to rise in rank as little as possible then by apt choice of details we can say in ZFC+U locally small categories have the rank of the universe U and the functor categories between them are superclasses one rank higher. Limiting the rise in rank this way is actually pointless in ZFC+U which has sets of rank β above U for every ordinal number β but it would be crucial if we wanted to use weaker extensions of ZFC which only add proper classes and a limited number of ranks above them. Anyway that will not be the end of our rise in rank, since categorical manipulation of these superclass categories means placing them into categories of yet higher rank. Grothendieck's foundation for this was universes as he says on the first page of chapter 0 of the book version of EGA [Grothendieck and Dieudonne, 1971, p. 19]."

Fontanella 2019: "Independence results have always caused a certain embarrassment in the community of mathematicians. When a mathematical problem is proven to be independent from ZFC, suddenly it is labeled as ‘just set theoretical’ or ‘vague’ and no longer mathematical in the traditional sense. A precise definition of what ‘ordinary mathematics’ means should then take into account this attitude towards those problems which, at first, seem to emerge naturally as intrinsically relevant questions for mathematical research, then are dismissed after proven to require strong axioms. A simple move would be to claim that independent problems are legitimate mathematical questions that yet are ‘unsolvable’. In this perspective, then, any attempt to answer such questions with stronger assumptions can only be seen as speculative. Surely, many mathematicians navigate these lines of thoughts. For instance, when Nykos (1980) proved in 1980 the consistency of the Normal Moore Space Conjecture from a strongly compact cardinal, he titled his paper ‘A provisional solution to the Normal Moore Space Conjecture’ (emphasis mine). However, if any result assuming large cardinals were just ‘provisional’, as Nykos’ choice of words suggests, then Large Cardinals Axioms would be nothing more than mere hypotheses. Yet, despite the general skepticism towards the legitimacy of these principles, the mathematical community seems to acknowledge them a different status, a stronger role. In fact, we can point out that Wiles’s proof of Fermat’s conjecture was well accepted by the community of number theorists despite the fact that it relies on inaccessible cardinals. Imagine that his proof were assuming Riemann hypothesis instead, would his result even be published? The supporter of the view that ordinary mathematics can all be done in ZFC, or in a much weaker system than ZF, needs to clarify what should be the status of independent problems and of the additional assumptions needed for their solution."

Thomas Scanlon: You got me there. Google Bard invented two entirely fake references for my consumption, just now:

A Note on McClarty's Paper on Wiles' Proof of Fermat's Last Theorem: https://arxiv.org/abs/2101.07684 by Thomas Scanlon

Wiles's Proof of Fermat's Last Theorem: A New Perspective: https://arxiv.org/abs/2007.13670 by John McClarty

In fact all 3 references it gave me are made up. The Razborov one sort of, this is how Bard explains itself:

How about this one: "The Existence of Elliptic Curves Without Grothendieck's Universes" by Alexander Razborov (2022)

That paper does exist, but it is not by Alexander Razborov. It is by Jacob Tsimerman, and it was published in the journal Annals of Mathematics in 2022. The paper proves the existence of elliptic curves over finite fields without using Grothendieck's universes, which is a powerful tool in set theory.

Here is the link to the paper: https://arxiv.org/abs/2007.07370

I apologize for the confusion. I am still under development, and I am sometimes able to generate incorrect or misleading information. I will try my best to avoid this in the future.

I hope you find the paper interesting!

Which, alas, is also fake. Most of the above arxiv references exist, but they are to completely different papers.

[Johan Commelin]

Just imagine how much other BS it shoved down your throat during your research on FLT

[Lars Ericson]

The NY Times wrote an article about the NSF workshop. It pointed to a post by Michael Harris reviewing the workshop. He wrote four posts:

https://siliconreckoner.substack.com/p/right-on-cue-the-military-industrial
https://siliconreckoner.substack.com/p/my-shallow-thoughts-about-deep-learning
https://siliconreckoner.substack.com/p/my-shallow-thoughts-about-deep-learning-917
https://siliconreckoner.substack.com/p/my-shallow-thoughts-about-deep-learning-186

In this one, he highlights the issue of different culture/values in computer science versus mathematics:

After the last panel on Day 3 opened with introductions and with generalities about the value of interdisciplinary work, Heather Macbeth, the moderator, invited the panelists to speak about what mathematicians want from AI. Of course, she said, they wanted "to prove more theorems faster," but what else beside that?

(Here the image of mathematicians as mice on a treadmill flashed through my mind, and as an unseen operator turned up the speed knob I tried to pinpoint the historical moment when proving "more theorems faster" became our principal common aspiration. I'm not saying Macbeth is wrong; surely those concerned are eager to get the Riemann Hypothesis or the Hodge Conjecture out of the way as soon as possible, in order to move on to … whatever comes next. But one might wonder why there is no mathematical version of the "slow food" movement, whose goal would be to savor moments of insight repeatedly, preferably in the company of one's peers, in the way one doesn't tire of listening to certain songs. Whereas when I reread a proof I've already seen it's always for the sake of future productivity, and never for pleasure alone. Is it that way for you too?)

He also wrote a post about Lean and the Liquid Tensor Experiment that has a similar theme:

The conflation of mathematical creation with industrial production can be traced in part to the different roles proof plays in pure mathematics and in software verification. You may or may not care by what route the electricity that powers the machine on which you are reading this article has traveled from the generator to your home. But it matters very much that it will get to you safely, without breaking down or setting off fires or explosions, especially if the generator is a nuclear plant. So verification of the software that structures the grid is an urgent necessity… Donald MacKenzie reminds us in his Mechanizing Proof that this is why proof became important for software developers in the 1960s.
Proof in mathematics plays a much less consequential role. The late geometer Sir Michael Atiyah once described mathematical proof as
"the check that I have understood, … It is the last stage in the operation—an ultimate check—but it isn’t the primary thing at all. "
Or, to repurpose an old Dutch proverb, mathematics is "not about the marbles, but about the game."

There was another discussion, I thought it was Harris but I can't find it, about the size of proofs, for example a 200TB proof, the academic incentives for pure mathematicians to produce more single-authored papers for their career, and a paper with 4000 authors.

The general theme being some reconciliation of work style, incentives and values in the intersection of computer science and mathematics around proof verification.

[David Michael Roberts]

McLarty's paper published in 2020 proves no, you don't need universes for SGA, hence (I believe he claims) for FLT https://doi.org/10.1017/S1755020319000340 = https://arxiv.org/abs/1102.1773

[Lars Ericson]

Glenn Stevens gives this overview of the proof of FLT. It is about 3 paragraphs long in the original. Per above, the task is to expand this to a more concrete 10,000 pages or so of Lean:

FLT is stated as

theorem FLT1 (n : Nat) (a b c: Int)
    (h1: n > 2)
    (h2: a^n + b^n = c^n) :
    a*b*c = 0 := by
  sorry

Through elementary arguments, this becomes

theorem FLT2 (p : Nat) (a b c: Int)
    (h1: Nat.Prime p)
    (h2: p >= 4)
    (h3: a^n + b^n + c^n = 0) :
    a*b*c = 0 := by
  sorry

Fix a prime $p \geq 5$ and suppose $\exists a,b,c \in \Z : a^p + b^p + c^p = 0 \land a b c \neq 0$.
Consider the triple $(a^p,b^p,c^p)$.

By the Hellegouarch and Frey construction, obtain a certain semi-stable elliptic curve $E_{a^p,b^p,c^p}$ defined over $\mathbb{Q}$.

By Wiles' semistable modularity theorem, deduce the existence of a modular form $f_{a^p,b^p,c^p}$ associated to $E_{a^p,b^p,c^p}$ by the Eichler-Shimura correspondence.

Consider a certain irreducible galois representation $\bar\rho_{a^p,b^p,c^p}: G \to GL_2(F_p)$ associated to $f_{a^p,b^p,c^p}$.

By Frey and Serre, $\bar\rho_{a^p,b^p,c^p}$ can ramify only at $2$ and $p$ and is semistable and mild at $2$. This is called little ramification.

It is difficult to make large galois representations with little ramification. A large galois representation with little ramification (I'm paraphrasing here: I don't know what I'm talking about, I'm a human ChatGPT) is called a modular galois representation.

By Ribet's proof of Serre's conjecture, the existence of such a modular galois representation implies a contradiction in the theory of modular forms. FLT follows.

[Lars Ericson]

Recent interview with Wiles: https://plus.maths.org/content/fermats-last-theorem-30-years