The Fermat's Last Theorem Project

https://leanprover-community.github.io/blog/posts/FLT-announcement/

by happa • 2 years ago

75 41 2 years ago

leanprover-community.github.io

levn112• 2 years ago

https://www.techrxiv.org/users/717330/articles/702287-on-fer...

voldacar3• 2 years ago

Why post this? This appears to be the writings of a crank.

levn112• 2 years ago

which part

n4r93• 2 years ago

This would definitely benefit from a bit more explanatory text as I'm struggling to understand what you've shown. The crux seems to be that if a^n+b^n=c^n then (c-a)(c-b) divides (a+b-c)^n. I haven't been through all the details of this, but I also don't see how that implies FLT.

hughesjj2• 2 years ago

If I'm not mistaken Fermat's last theroem isn't even featured in the proof. Like nowhere did I see a^n+b^n=c^n referenced in the proof,save for the end of page 1 and 3, but it's never featured in an equality. Just 'this implies this trust me bro'.

rndnumthy2• 2 years ago

What I really like is that this project will not blindly formalize the proof from the 90's. Instead they take a SOTA approach, streamlining and optimizing many parts of the proof. So it will result in a useful artifact for modern number theorists.

Pet_Ant• 2 years ago

SOTA?

lightspot21• 2 years ago

SOTA = state of the art

rndnumthy2• 2 years ago

PDF slides from the talk where the project was launched: https://math.mit.edu/~drew/vantage/BuzzardSlides.pdf

mehulashah• 2 years ago

I wonder if after all that work, we might automatically reduce the proof and discover a simpler one that could have been included in the “margin”.

ultrablack• 2 years ago

I was just about to post my proof, but it didnt fit on Twitter :)

kevinbuzzard5• 2 years ago

I highly doubt that the proof will get small enough to fit into a margin, but history shows that it's not at all unreasonable to expect simplifications/generalisations of the argument to come out of a formalisation (for example this happened with the Liquid Tensor Experiment, where dependence on stable homotopy groups of sphere was completely removed from the argument). I think it is unreasonable to expect that at the end of an FLT formalisation there will be no mention of elliptic curves, modular forms, Galois representations etc (the standard tools used by Wiles to prove the result in the 90s and which have themselves been simplified and generalised by mathematicians such as Taylor and Kisin since then). And you'll need quite a big margin to get all that stuff in.

downboots• 2 years ago

perhaps it was a veiled suggestion to use infinity in the proof (which would not fit in any margin) (?) https://en.wikipedia.org/wiki/Proof_by_infinite_descent

practal7• 2 years ago

Very smart to open up the project from the start to make collaboration possible.

I have ambivalent feelings about this project. On one hand, I think this is great, it approaches things in the right way, and I think the project has a big chance of being very successful.

On the other hand, the more successful mathematics in Lean becomes, the more entrenched a type-theoretic outlook on formalised mathematics will become. I think that is highly problematic as it makes the expression of theorems and theories more involved and complicated than it needs to be. This is not a stopping block, and people like Buzzard can just power through this. Also, that's just my opinion. I am trying to go with Practal a different path and prove this opinion to be true, but that will take time.

cjfd• 2 years ago

I think the type-theoretic outlook on formalized mathematics is actually great, much nicer than set theory anyway. Set theory is a bit like an untyped programming language. You get to ask 'interesting' questions like whether the trivial group is equal to the number 5 which makes sense because both of them are actually a set.

What I am dismayed about is giving yet another area of computing to Microsoft. We all know that Microsoft ensures great care of the long term quality of software, right? Like when you click 'delete' on an email in outlook and have to wait 20 seconds for it to actually disappear.

Why not use coq instead?

msfanboy-aahum• 2 years ago

The main dev of Lean no longer works at MS. So currently there are basically no ties to MS. Lean is developed by the Lean FRO, which aims at being selfsustainable in ~4 yrs from now.

kevinbuzzard5• 2 years ago

Lean is free and open source and nothing to do with MS. Check out https://lean-lang.org/ and https://github.com/leanprover/lean4 -- no mention of MS or MSR (where de Moura was where he developed Lean 3 and started on Lean 4).

I have no doubt that a similar project could be done in Coq. The fact that we're using Lean is a random historical coincidence. If we'd used Coq then you could ask "why not Lean".

practal7• 2 years ago

Type theory vs. set theory is not the only choice. It is possible to combine their strengths in a new foundation: A single mathematical universe, just as in set theory, and higher-order features and abstraction, just as in type theory. Note that the listed strengths of each are the weaknesses of the other.

infogulch• 2 years ago

I have no experience in this area, but when I last looked Lean and mm0 were the interesting theorem proving systems to me. Lean for its momentum and big projects, and mm0 for its goal of producing a minimal kernel proven down to machine code.

Practal seems interesting and I scanned through the paper a year or two ago, but I have no reference point to evaluate it. I'm glad to see that you're still publishing about it.

How would you compare Practal with Lean, and what do you hope to prove (ha) with the project?

practal7• 2 years ago

Well, the most important difference is that Lean exists and is going strong, and Practal doesn't even exist yet.

But the logic Practal is based on exists now. I am currently writing the basics of this logic up as a book [1]. Chapter 2 will be ready soon. I have learnt much about the logic in the last few months, also as a consequence of trying to implement it, and the book is based on this latest understanding. It all is really really simple, and I am trying to give it the proper form so that this becomes obvious.

I very much hope a first implementation is available this year, but this depends on how much I can work on it uninterrupted by money concerns.

In the end, what I am trying to prove with Practal is that formal logic doesn't make things more complicated. It actually makes things simpler.

[1] http://abstractionlogic.com

kevinbuzzard5• 2 years ago

My impression is that some parts of maths work best using set theory, some parts work best using type theory, some work best using a category-theoretic foundation and ignoring size issues etc etc. There's no one "best" foundations, and mathematicians on paper just freely (and mostly unknowingly) switch between foundations depending on what they're doing. This is problematic for a project such as formalising FLT because it involves developing mathematics in a bunch of different areas (algebra, analysis, geometry) where different foundations might be more appropriate (for example getting homological algebra working in dependent type theory has been annoying and hard for all the wrong reasons, and it's taken the Lean community years to figure out how to do it).

So I don't really understand the point made in this post. Dependent type theory makes the expression of some theorems more involved and complicated -- but set theory makes the expression of some other theorems more involved and complicated, simple type theory makes the expression of some others more involved etc etc. You're right that we're just powering through this: but formalising mathematics in Lean sometimes feels like fighting against type theory (and sometimes type theory is a very welcome foundation). The point really is that the Lean community, because of its viewpoint of "formalise all mathematics in one system", has been forced to figure out how to power through the areas where dependent type theory was not the ideal foundation. Maybe the same can be said of Mizar and set theory -- I'm unclear about how much formalisation in Mizar is motivated by "let's do this because it will be unproblematic in set theory" and how much is "let's choose to do battle with set theory". In mathlib we've decided to do everything so doing battle with dependent type theory is a necessary consequence. I find it hard to believe that another foundational choice (such as Practal) solves these sorts of problems: presumably what's actually true is that some stuff which is annoying in Lean is nice in Practal but some other stuff which is nice in Lean is annoying in Practal.

practal7• 2 years ago

So I don't really understand the point made in this post.

I think you understand the point perfectly well. You just don't believe that there can be a logical system better suited to a foundation of mathematics than first-order logic (set theory), simple type theory, or dependent type theory. You believe you will need to compromise, no matter which foundation you choose, so better just to pick your poison and get on with it. And I think pretty much everyone in the theorem proving space has that same opinion, so it is certainly a most reasonable opinion.

But I don't believe that the right logical foundation will make it harder to do mathematics on a computer than on paper, I think it will make it easier. In fact, I am pretty sure I have found that right logical foundation, Abstraction Logic [1]. I believe that it is indeed the best logical foundation, because it is simple and elegant (more so than any other foundation I am aware of), and it seems obvious that first-order logic, simple types, and dependent types are just special cases of it.

But a logic is not a working and proven system such as Lean + mathlib, so a lot of work needs to be done before my belief can be stated as a fact.

[1] http://abstractionlogic.com

TwentyPosts• 2 years ago

Could you elaborate on what alternative to a 'type-theoretic outlook' you're thinking of? Pure set theory? Something without types at all, somehow? I don't know enough about the space to understand how type theory would make things "more complicated" as opposed to just being a helpful tool

practal7• 2 years ago

I am writing about this here: http://abstractionlogic.com

Chapter 1 of the book is already available (you can buy it for £0), and Figure 2 vs. Figure 3 describes how type theory is different from Abstraction Logic, although I don't mention type theory explicitly at this point.

Future chapters take this view of the mathematical universe presented in chapter 1, and give it an algebraic and logical form.

robinzfc• 2 years ago

Another aspect of this is the readability of the resulting text. The role of a proof in mathematics is not only to certify that an assertion is true, but also to communicate to mathematicians why it is true. Lean and Coq verification scripts are not readable in this sense. They do certify that assertions of theorems are true and (at the current state of technology) that the author of the script most likely knows why they are true, but it is close to impossible for a reader to see what is going on in the proof without running the script step by step in software. The Mizar proof language and Isabelle/Isar were designed to communicate as well and proofs written in those languages can be read and understood directly by humans. For a comparison how the same proof of a simple theorem looks like in Lean, Isabelle/HOL, Isabelle/ZF and Mizar see [1], [2] and [3].

[1] https://lawrencecpaulson.github.io/2024/02/28/Gowers_bijecti...

[2] https://isarmathlib.org/func1.html#a_bij_def_alt

[3] https://mizar.uwb.edu.pl/forum/archive/2403/msg00001.html

practal7• 2 years ago

That's a very good point. I have been strongly influenced by Isabelle and Isar, which get a lot of things right.

I think the future looks like this: The resulting text will be natural language (LLM powered), layering upon the actual formal logic. I think Abstraction Logic is actually best suited for this scenario, and I am designing Practal from scratch for it.

pylua3• 2 years ago

I think this is awesome. I do wonder if projects like this will are the first step for humans to completely hand over proving to machines.

criddell• 2 years ago

At first I was going to react to you using "completely" because I thought the obvious thing was that the machines would remain a tool and maybe become collaborators.

Then I started to think about it and now I have the same question. When will a machine spit out a proof that we just can't understand? Just like how a dog will never understand the fundamental theorem of calculus, there are almost certainly ideas and concepts that we can't understand but the machines might.

JoeAltmaier2• 2 years ago

Already happened? The four-color map theorem was a computer program exhaustively going through some solution-space until it found one. Thousands of lines of logic spit out on paper. Probably impossible for any human to comprehend.

throwaway81523• 2 years ago

Why has Lean taken over the formalization world? Previously some big proofs were done in Coq, HOL, etc.

The Fermat's Last Theorem Project

Related Stories