Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Formalizing Fermat's Last Theorem

anthropic.com

Post reply on HN
Print view View original

501–510 of 527 posts

Re: Formalizing Fermat's Last Theorem

#501

Post by make3 »

skobes wrote: post #228
m_w_ wrote: post #7

> Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems. Pretty insane. I suppose it lends further credence to the idea that anything that can be shown to be correct can be done by a model.

Maybe I'm misunderstanding something about how all this works, but can we have any confidence that 13 million lines of AI-generated Lean code are... correct? How have we not merely substituted one verification problem for another?

Lean is adversarial in a way. Lean is better thought of as a constraint language with a verifier that checks if the constraints are respected, than a programming language.

Your job or the LLM's job is to write code that Lean is satisfied with, creating the link between what you're trying to prove, and mathematical axioms.

If you write a bad proof, the Lean constraint checker will tell you, unless there are bugs in Lean itself, or you defined the goal constraint incorrectly.

Re: Formalizing Fermat's Last Theorem

#502

Post by tsimionescu »

bigyabai wrote: post #473
bananaflag wrote: post #436

Earlier quoted context omitted.

The argument was that senescence is as natural as child mortality, and thus naturalness is not a reason not to fight against it.

I don't think that argument holds water? According to WHO, 8 in 10 neonatal deaths are caused by substandard care, not "natural" causes: https://www.who.int/news-room/fact-sheets/detail/child-morta... No matter what standard of care you receive, senescence will gradually kill you even with therapies or treatments to slow it. It's a part of the built-in natural lifecycle that humans can't avoid; it's not analogous to…

> No matter what standard of care you receive, senescence will gradually kill you even with therapies or treatments to slow it.

That doesn't mean that it can't be entirely reversed. We already know that senescence is not a completely required part of life itself, or even of eukaryotic and/or multicellular organisms - as we have known examples of organisms that don't experience it. For example, jellyfish don't experience senescence (they go through a revolving cycle of polyp - jellyfish that can go on forever as far as we can tell). And even if true permanence is out of reach, we also know of animals that live for hundreds of years, and of plants and fungi that live for thousands or tens of thousands of years.

So, having a way to make something like a human (though possibly quite different from what we call a human, to be fair) live for at least a few hundred years if not much more is a very difficult but certainly solvable bioengeneering problem, not some philosophically impossible feat.

Re: Formalizing Fermat's Last Theorem

#503

Post by andriy_koval »

IsTom wrote: post #499
andriy_koval wrote: post #468

Earlier quoted context omitted.

No, once you start formalize this, it becomes complicated. There is a reason why looks like there is no "peano can be derived from zfc" theorem which would close dispute, and my opponents need to throw links on bro math from stackexchange in this discussion.

Per https://en.wikipedia.org/wiki/Peano_axioms#Set-theoretic_mod... > The Peano axioms can be derived from set theoretic constructions of the natural numbers and axioms of set theory such as ZF.[15] If you're going against the general consensus you should present something more than nebulous assertions that it's wrong.

Obviously citation from wikipedia can't be considered as replacement of math proof.

> If you're going against the general consensus you should present something more than nebulous assertions that it's wrong.

burden of proof is on the one who claims something exists.

Re: Formalizing Fermat's Last Theorem

#504

Post by tsimionescu »

qbit42 wrote: post #417
jmusall wrote: post #220

Earlier quoted context omitted.

That must have slipped through Kevin Buzzard's review, which is not entirely unplausible with 29500 theorems to verify... I think they should spend another few billion tokens and let agents try to disprove any of those statements or links between them. Then I'd be a lot more convinced.

You just have to trust the statement and the lean compiler, not the proof. The compiler certainly still has remaining bugs, but I have never seen a bug leading to a false proof in good faith, only via obscure meta programming tricks. The nice thing is that the multiple versions of the compiler are constantly being stress tested. Still, there is plenty of work that could be done to make the compiler more trustworthy /…

This being 13M lines of entirely agent-generated code, we can't be certain it's written in good faith and doesn't actually exploit some weird metaprogramming trick. The agents' goal was to write a proof that Lean prints "correct" on, not to check that the proof of the FLT was valid (which they wouldn't be able to do anyway).

Re: Formalizing Fermat's Last Theorem

#505

Post by thaumasiotes »

gus_massa wrote: post #489
thaumasiotes wrote: post #256

Earlier quoted context omitted.

>> Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems. > Pretty insane. I don't think the count of "intermediate theorems" tells you anything. Here's something from an algebra textbook: --- Let G be a group, let H be a subgroup [of G], and let N be a normal subgroup [of G]. Then H ∨ N = HN = { hn | h ∈ H, n ∈ N }. --- This says that the subgroup closure of H and N, the smallest s…

It looks like an exercise for a course in "Algebra 2" in my university. (A different course name in other universities.) I probably should know it. Give me 30 minutes to prove it. (Part of the magic is in "normal".) My algebraic friends surely know it and they would never include it in a paper because everyone knows it. I'm surprised it's not in mathlib. Perhaps it is and the AI made a copy. Perhaps it isn't and it i…

> Perhaps it isn't and it is a nice PR for beginners.

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.)

Re: Formalizing Fermat's Last Theorem

#506

Post by andersonpico »

Vakaiser wrote: post #9

We'll increasingly observe announcements of this kind as AI tooling scales. As impressive as agentic coding is, it pales in comparison to the value proposition of medical, mathematical, and physics research. I optimistically expect to witness the advent of a global 'panacea' in my lifetime thanks to AI's efforts. Cost effective large scale genetic engineering, a cure for every disease, potentially even a cure for agi…

> I optimistically expect to witness the advent of a global 'panacea' in my lifetime thanks to AI's efforts

this is a religious belief, maybe you should stop to really examine that (because it might be unintentionally so), but just know that it is obvious to anyone reading these words (anyone who is not mesmerized by technology)

Re: Formalizing Fermat's Last Theorem

#507

Post by [deleted] »

dang wrote: post #123
lalitmaganti wrote: post #3

I suggest also reading Kevin Buzzard's blog post which was just posted: https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-h... Provides great context on this accomplishment, what it means but also doesn't mean.

Thanks! I've added that link to the toptext. I'd really like to make it the top link (and relegate https://www.anthropic.com/research/formalizing-fermats-last-... to the toptext) since HN has been tracking the work of https://news.ycombinator.com/user?id=kevinbuzzard for a long time and we're big fans. But I guess that would be overkill.

[deleted]

Re: Formalizing Fermat's Last Theorem

#508

Post by jonesn11 »

dang wrote: post #123
lalitmaganti wrote: post #3

I suggest also reading Kevin Buzzard's blog post which was just posted: https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-h... Provides great context on this accomplishment, what it means but also doesn't mean.

Thanks! I've added that link to the toptext. I'd really like to make it the top link (and relegate https://www.anthropic.com/research/formalizing-fermats-last-... to the toptext) since HN has been tracking the work of https://news.ycombinator.com/user?id=kevinbuzzard for a long time and we're big fans. But I guess that would be overkill.

""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. My guess is that it is unlikely that Anthropic are going to do this; they will feel that their job is done with the formalization (and they did not formalize the modern proof anyway)."" lol if you say so buddy...

Re: Formalizing Fermat's Last Theorem

#510

Post by nbardy »

p-e-w wrote: post #293
bryanlarsen wrote: post #192

Earlier quoted context omitted.

SemiAnalysis estimates their profit margin to be 70%. To be losing money on inference implies that their costs are almost 4X higher than SemiAnalysis has calculated. That's not credible.

I don’t see how they could credibly estimate inference costs without knowing the model size.

You can estimate the model size by looking at tokens per second and comparing to open source models
Post reply on HN