Formalizing Fermat's Last Theorem

https://hn.algolia.com/?dateRange=all&page=0&prefix=true&sor...

Giving such a blanket "responsibility" to the author at all is just such a bummer! I say let them do whatever they want, there is always more than one way to express oneself. Someone who was never taught to write a clear thesis in the first paragraph for whatever reason doesn't inherently have less to say.

Haven’t you dramatically overstated your case? Many expositions do not contain an explanation of their value at all. Works of fiction are a good example, and there are many many others. Often it’s the responsibility of the readers & reviewers to decide on questions like value.

The point is that people who spend their time classifying nilpotent Lie groups that admit structure X are out of work if they don't change their perspective. Maybe such problems were never really that interesting, although it was useful to have a group of people acting as human computers to work them out - but well used AI yields for such problems more complete and more reliable results - and so allows researchers to spend their time on other more interesting things. The problem for your run of the mill professional mathematician is that more interesting things are harder ...

This is how the theorem for FLT looks in the particular proof we discuss here:

theorem fermat_last_theorem (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a ^ n + b ^ n ≠ c ^ n

As long as this statement is correct, and the kernel is correct, the proof could be trillion lines of code, and if the kernel says it is correct, it is correct.

This proof was checked against TWO independently built kernels. So you would need TWO kernels to have the same bug to mistakenly accept an incorrect proof.

(Not impossible: such a bug indeed was recently discovered (and patched))

The source article does acknowledge this isn't a replacement for human analysis, but they seem to imagine a vision of mathematical research where there's a bunch of AIs running around proving random things and formalizing them into opaque Lean proofs nobody ever has to read. I'm skeptical whether there's any value in doing that, and to the extent that there is I'm pretty confident it looks more like proving certain directions aren't fruitful for further investigation.

In a sense, the proof is a demonstrator not an end in itself. To mathematics enthusiasts it is significant. To the AI it is Tuesday.

Enjoyed that idea. Not sure how true but it was enjoyable.

My strong hunch is that it was a joke - he knew how difficult the problem was and claiming he had a solution was I think a huge motivating factor for many mathematicians trying to prove it. The greatest nerd snipe troll in history.

How can you be so sure its not result of inefficiency?

The part of the proof that I quoted just proves that the product set HN is closed under multiplication - the product of any two elements in HN is also an element of HN. This is part of proving that HN is a subgroup. You might call it an 'intermediate theorem' to that proof.

My point isn't that this is missing from mathlib, or that this result is part of the work mentioned in the blog post. It's that doing this proof in a way that matches the textbook proof requires you to prove a large number of "intermediate theorems", and that those "intermediate theorems" often look more like computational steps than anything that a mathematician might call "theorems".

In particular, note that the 10 required intermediate theorems I mentioned all refer to free variables.

By the way, there is a steady stream of people who come into the "new members" channel on the Lean zulip and ask for ideas for a minor contribution they can make. The stock answer is generally that the low-hanging fruit has been picked.

But that isn't really accurate. If your goal is to get something, anything, into mathlib with your name on it, you probably can. Choose some undergraduate exercises, try to formalize them using mathlib, and at some point you'll run into some convenience lemmas that you wish were present. You can then produce one of those lemmas and try to get it accepted.

(As part of a project I'm working on, I produced a proof that involved showing that a function was bijective from the already-existing mathlib theorems that it was injective and surjective. There was no one-step existing theorem despite the existence of the injectivity and surjectivity theorems.

When I complained about some other part of my proof, somebody else picked up on that and quickly submitted a convenience theorem directly stating the bijectivity. That's the kind of thing I'm talking about, though you can go more complex than that example.)

They all steal from ACL2 without attribution in the current publication boiler room atmosphere. They get away with it because the AI Cult has information and publication dominance.

There was a brief period that used only language for toy IMO problems, but for serious work like FLT they apparently reverted to established approaches.

I'm not some "LLM is just a next token predictor guy" (GP seems to have a thing against LLMs), but to use LLMs properly you genuinely do need a grounded verifier and a planner. Coding harnesses for example are exactly that.

For some plans, you can AR generate the search tree and that's what subagents being planned around by high level (LLM)agents and such are. Coding agents even with subagents are imperfect even on verifiable tasks only because of that. If you can put a human to simply guide it, it becomes a full system. This is what we all do today whenever we use codex. It's not something that is "never done before".

I also don't subscribe to the purist view which is taken by GP. I prefer to think in terms of concentration inequalities. P(failure rate > r) < epsilon. You get different levels of autonomy for different values of r for the planner and verifier each. If you have a good planner and a good verifier, r is very very small and it's super useful. Autonomy at a given r comes from how much of the planner and how much of the verifier is automated at that r. All levels of autonomy are economically useful. Many values of r are economically useful.

In this case of FLT, the verification was entirely automated using lean, and it is correct upto lean compiler bugs (so a very small r). The planner was essentially a maintained graph (afaik. Prove2me doesn't use A* or any heuristic/evolutionary methods to limit or prune the frontier), AND importantly - I'm not seeing anyone on HN mention this - some human nudges, literally, which nodes to open.

The way to make AI systems more useful is to build great verifiers and great planners, which is what many companies and startups are doing. LLMs are already really really good proposers due to excellent generalization (to be pedantic, multiple stacked specialisations), especially MoE models, making them amenable to proposing at every point in a vast search tree without any adaptation.

Yes, it is possible to do complex tasks purely AR, so long as you can AR simulate the search, which in the case of LLMs corresponds to verbalising the search tree[4]. This is trivially true. Can this be useful? Yes. Can a millenium prize problem be solved purely AR? Sure. It's a hard problem for humans, there is no reason it has to be difficult to reach in the conditional distributions of every future LLM. In the trivial limit, an LLM trained on the solution 100% you can sample it out. An LLM 2 generations behind that may have it at p=0.001, entirely reachable given a planner, but probably not AR. An LLM 1 generation behind may have it at p=0.05, plausibly reachable purely AR.

But the key question is: is `r` smaller or larger if you have a planner versus not? The answer there is obvious. Second, if you have a threshold `r` that decides usefulness, is the set of things you can autonomously do under that threshold higher with planners and verifiers? Again the answer is an obvious yes.

Copy pasting code from chatgpt repeatedly is worse than using a coding harness where it gets grounded feedback, LLM weights kept constant. Keeping the history of things and the overall plan that worked fixed and isolating LLMs to do subtasks is better than developing a whole database in one continuous context. In some cases, the overall plan "tree" can itself be entirely verbalised, but most commonly there is human modifications/steering.

Can pure-LLM coding harnesses with just verifiers one shot most e commerce sites including planning? Yes. But we want to do more with it than e commerce sites. Will it keep improving thus enabling us to do more and more complex things? No obvious reason for a fixed limit to exist in theory[1]. But at any point on the progress curve, using it with a harness always gives better results versus not. Concretely, with fable 5.1, using it without a harness could not prove FLT in reasonable token budgets [3]. However, it is possible for say, idk, GPT9, trained on this, to verbalise this whole proof tree, and also potentially generalize it to another open problem, purely AR, in a reasonable token budget[2]. This was how we got from gsm8k to FLT in the first place.

It's not a binary "AR is useless" "AR is all you need".

[1] the limits are mostly economic, and time is itself a limit, see https://news.ycombinator.com/item?id=49161078 Tl;dr diminishing returns of test time scaling. Noam brown also has a piece about this.

[2] if it's too many tokens that we run out of time or money literally, that is the limit described in [1]. It is not linear or constant scaling necessarily as described again in [1].

[3] [2] is why we have to add token budgets as another axis apart from r and the autonomy level.

[4] And, the distribution conditioned on that verbalisation must be amenable to sampling the verbalisation of the execution of the plan from. This is not a given, see https://arxiv.org/abs/2504.09762 and https://news.ycombinator.com/item?id=49277303

> The work certainly achieves some of the aims of the EPSRC project, and indeed it goes much further in terms of what is formalized (I only promised the EPSRC that I would reduce FLT to the 1980s; this repo proves the whole thing). But I also promised several other things to EPSRC: firstly, that I would be making pull requests to Lean’s mathematics library, adding fundamental objects from modern number theory; this is ongoing. And secondly, and perhaps most importantly, that I would be creating a dynamic document enabling humans to explore the modern proof.

Its like using AI to do your homework in the middle of a class. Yes, in the short term, that solves the problem of completing your homework. But it creates an entirely new problem of if you never did the homework how do you intend to pass the rest of the class or the remainder of college curriculum? A lot of cheaters ... don't.

A project has a long term path for permanent progress across an entire field. An oracle answers a question, sometimes cryptically, then progress in the field permanently ceases.

The value of a research project to determine if a Turing Machine halts with a T or a F on the tape is, to some extent, did it get a T or an F on the tape, but much more so the value is the tendrils of the rest of the field of mathematics pushing into the project at the start and then pushing out to enrich the rest of the field of mathematics at the end.

On the other hand if you have a project to run that Turing machine and see if it ever halts with a T or F as the proof, the result is completely sterile and WRT advancement of the rest of the field the actual result is kinda irrelevant. No postdoc is going to take the skills learned and move on to a position somewhere else and apply those new skills toward advancing something else in the field or describing a new goal or new way to look at the world. We'll get a popular science article about "oh it turns out the answer is indeed 'T'" and thats it. Sterile.

Personally I always thought the theorem proving turing machine would indeed terminate with a "T" and indeed it did. That's nice, and I bet the result settled a lot of bar bets. Aside from that, it will have minimal impact on progress in the field compared to the human project that's actually advancing the field.

Possibly people will be able to parse the 13 million lines of whatever into useful progress elsewhere in the field, possibly not. It'll be hard to get funding for it. OTOH its early days. Might end up useful in the end.

There are many reasons that people living forever would be a problem for society, the most obvious being an ever-increasing population.

I'd also say people may want more life for themselves, but what does that mean at scale, forever?

And granted, I don't know the exact details about Lean. It might be that they don't have an incredibly simple core - as has elsewise been the norm.

zfc itself is not sufficient, you need some layers of extra concepts formalization to fit specific problem domain(e.g. zfc doesn't define even basic arithmetics), which also could have potential issues.

Godel theorems are for systems with basic arithmetic, zfc doesn't include arithmetic, thus are not object of Godel theorems.

How much more magical do you want this to be?

Tool or not it did something you could never have accomplished.

will you not see that people could be truly empowered and yet will instead be oppressed?

It seems to me that it is making everyone (including myself and the researchers we need to cure diseases) lazy and dependent on thinking machines owned by tech companies. Just how autocomplete and gps made us worse at spelling and navigating, llms make us less able to exercise our ability to think and problem solve. This will have 100% strictly negative consequences on you and the world as a whole. .

And even if there was a cure to many diseases the eugenics types who are embedded in worldwide power structures definately arent going to share that universally.

Notably, junk theorems are true. Nobody would debate that the junk theorem is true. The main thing people would say is that junk theorems, while being true, are sensitive to precisely how you encoded mathematics, so despite being true, they are perhaps not conceptually meaningful.

As an example of a junk theorem, sasy you use the definition of the natural numbers using von neumann ordinals

https://en.wikipedia.org/wiki/Set-theoretic_definition_of_na...

Then for any natural numbers n, m, they're implicitly sets. So n \intersect m = min(n,m). This is the wrong way to think about natural numbers. You should not use this ever in proofs. But this isn't because your proofs would be false, but instead because it is a fundamentally confusing way to think about the natural numbers. It is in this sense it is a "junk theorem".

> The first coordinate of the polynomial X^2 (X^3 + X + 1 ) is equal to the prime factorization of 30 .

We defined polynomials as their coefficient functions in my algebra class, and it makes sense that you'd define a prime factorization as a function from primes to N, which naturally extends to a function N->N. So this junk theorem is part of normal math too. It just says in an obtuse way that they're both the function that's 1 at 2, 3, and 5, and 0 elsewhere.

(I swear, did not use an LLM for this)