How long will the proof be when completed?

Stream: FLT

[Juho Pitkänen]

Sorry if this is an inappropriate place for this question. I got inspired to ask this after seeing a speedrun of NNG. Obviously, the "final boss" wasn't beaten during the speedrun. I started to wonder whether someone could theoretically beat the boss once the project is done. This would of course take a very long time, but after all there have been speedruns in categories of other games lasting over 24 hours. So, how many characters/lines long might the proof be when complete, order of magnitude -wise? Could the server / client even handle such a long proof?

[Niels Voss]

Are you asking how large the actual FLT proof will be when it is complete, or how large would it be if you explicitly tried to make it really short? Or how long it would be if you had to write it as a single theorem without any auxiliary definitions (if such a thing is actually possible), as if you were actually typing it into NNG4? And if mathlib spends 100000 lines building up the theory of some algebraic structure and the FLT project uses those theorems, do you count the 100000 lines towards the proof length?

[Juho Pitkänen]

Hmm, I didn't really consider those things when thinking about the question. Well, I guess I was thinking of making it as short as possible but without using mathlib. The heuristic for what I'm going for is to pretend someone actually tried to type it or minimized variation thereof into NNG4. I see now that this question might be harder to answer than I initially assumed, as proving something in NNG4 is very different to what Dr. Buzzard is doing

[Niels Voss]

I guess the first thing to consider is whether this is possible in the first place. If you were to just restrict yourself to simple statements like the tactics in NNG4 and not have exact statements that span hundreds of lines, then you would essentially be reasoning in a system that resembles Peano Arithmetic. FLT was proven in informal math, and I think basically everyone believes that it is provable in ZFC (and Lean is even slightly stronger than ZFC), but I don't think anyone knows whether or not FLT is provable in Peano Arithmetic, although many people have speculated that it may be.

If it is provable, then you probably would need some way to make definitions. Definitions are never required, but they can compress proofs by reducing duplication. NNG4 doesn't have the let tactic so unless you want to use let inside a gigantic exact tactic this means that you might get exponential blowup in the size of proofs. If you took Wiles's proof of FLT and got rid of all the definitions, it might take more characters than the number of atoms in the known universe to write down the proof.

[Niels Voss]

This is of course assuming that you are interested in the FLT proof that we currently know about. I don't think humanity will ever know what the theoretical shortest FLT proof is.

[Niels Voss]

Note that you can bypass some of the restrictions of NNG4 by writing a very large exact statement. So hypothetically, you could compress all of the ongoing FLT formalization into a single exact statement (with the caveat that inductive types cannot be defined within a proof, so you'd need access to something like docs#WType). This wouldn't actually shorten the proof, and it might make it much longer.

[Juho Pitkänen]

Oh, I forgot NNG doesn't have let. However, it does have ´have´, which can substitute for it in some circumstances, right? (I'm still a Lean novice). And yeah, I'm interested in the currently known FLT proof.

[Niels Voss]

So have can sometimes work as a substitute for let, but not always. The problem is that when you define something using have, Lean forgets its definition (see https://leanprover-community.github.io/extras/pitfalls.html#using-have-for-data).

[Niels Voss]

I'm not sure how much of mathlib that the FLT project depends on, but given how tightly coupled mathlib is, I suspect that even a single theorem can transitively depend on a large percentage of mathlib. If you just want a rough ballpark estimate, mathlib is currently about 2 million lines of code, so the complete FLT proof, when minified by removing unnecessary theorems from mathlib, would probably depend on at least 1 million lines of Lean code from mathlib.

[Juho Pitkänen]

I see, thanks. I was already suspecting it might be too long to type into NNG, but I didn't realize how limited NNG actually was and how that might make it even longer
.

[Geoffrey Irving]

The distribution of length may be strange, because I would expect that most of the expected length comes from scenarios in which high levels of automation are used to generate very un-golfed proof terms.