Formalizing Fermat's Last Theorem • Hacker News Board

Re: Formalizing Fermat's Last Theorem

#211

Post by black_knight » Fri, Sep 04, 2026, 9:44 PM UTC

andriy_koval wrote: post #201

black_knight wrote: post #191

Earlier quoted context omitted.

A human can cite previous published results. I am sure a lot of this development was formalising the prerequisites.

> I am sure a lot of this development was formalising the prerequisites How can you be so sure its not result of inefficiency?

Oh, I am quite sure there are inefficiencies! Just that they are not entirely inefficiencies.

I have used Fable for formalisation and it will, unless I catch it, reprove results it previously had proven, inline, in other results.

Re: Formalizing Fermat's Last Theorem

#212

Post by mswphd » Fri, Sep 04, 2026, 9:44 PM UTC

tatjam wrote: post #206

QuesnayJr wrote: post #147

Earlier quoted context omitted.

Of course it is. The interesting thing is that it was able to produce a Lean proof in 11 days, when there's been an ongoing project for several years to do the same thing (though a somewhat different proof) that is nowhere near done.

I think there's a big misunderstanding going on here, translating the proof to Lean is, well... a translation task. Formalizing the proof in a way that's useful (breaks the proof down into relatively independent blocks that can be used for other maths and, importantly, understood individually) is a quite bigger, more creative endeavor. Not sure if LLMs would be able to do it, maybe yes?

note that this is exactly analogous to an LLM being able to slop code some demo, but not build something more generally useful/maintainable (say something suitable for inclusion in a standard library).

Re: Formalizing Fermat's Last Theorem

#213

Post by thrance » Fri, Sep 04, 2026, 9:46 PM UTC

chpatrick wrote: post #131

thrance wrote: post #81

Earlier quoted context omitted.

Come on, you can't compare that with Wiles's proof.

Still unsolved for 87 years.

Meaningless on its own.

Re: Formalizing Fermat's Last Theorem

#214

Post by CaptWorld » Fri, Sep 04, 2026, 9:47 PM UTC

CyLith wrote: post #197

nutjob2 wrote: post #101

Earlier quoted context omitted.

Most people want more life. For most people it's also the most terrifying part of "the natural human experience". If you're happy to die, why be bothered by others' trying to live longer? You won't be around. And assuming people can finance it themselves, is it really a problem for society?

Because living longer is a huge drain on resources that could be better spent on other things. End of life care is expensive and rarely results in a "good" life for the the life being extended.

So I think curing means basically opt in death or something like that. Right now extended life is bad because the person isn't in his prime but curing aging is basically gonna keep him in his prime. This might be what they meant.

Re: Formalizing Fermat's Last Theorem

#215

Post by whateveracct » Fri, Sep 04, 2026, 9:47 PM UTC

vatsachak wrote: post #167

The_Blade wrote: post #164

Earlier quoted context omitted.

physics is like sex: sure, it may give some practical results, but that's not why we do it

I mean at this point there's no doubt that LLM cans be RL maxxed and give you _some working output_ but the next frontier is whether they can create good abstractions, a.k.a use the correct level of expressivity so as to not inline everything yet not play code golf.

my feel after a lot of experience with agentic haskell at scale has been...no they cannot and maybe the opposite lol

Re: Formalizing Fermat's Last Theorem

#216

Post by ojo-rojo » Fri, Sep 04, 2026, 9:47 PM UTC

floweronthehill wrote: post #129

ojo-rojo wrote: post #95

I'm really impressed by mathematicians. It's cool that Fermat had the intuition to conjecture that "aⁿ + bⁿ = cⁿ" could not be satisfied for n > 2, and that other mathematicians can create proofs, and that others still can understand AI's formulation of those proofs. Really cool.

I wonder if AI can come up with mathematical conjectures. As in, they feel it's right but can't prove it. What even happened in Fermat's brain to sense it was true?

Right. Once we see AI start delivering on the creative & intuition side of things that's going to be awesome. Until then I guess we'll live with exhaustive exploration of problem spaces by orchestrating swarms of agents...?

Re: Formalizing Fermat's Last Theorem

#217

Post by behnamoh » Fri, Sep 04, 2026, 9:47 PM UTC

deepsun wrote: post #200

behnamoh wrote: post #198

Earlier quoted context omitted.

For now. That, too, will change in the future.

Same thing was said about cryptocurrency for like 15 years: "_in the future_ it will replace all fiat currency".

AI ≠ crypto.

Re: Formalizing Fermat's Last Theorem

#218

Post by doctoboggan » Fri, Sep 04, 2026, 9:47 PM UTC

sigmar wrote: post #12

>The speed with which we were able to produce this proof demonstrates that it is now possible to formalize large swaths of mathematics, which may both catch errors in the common body of mathematical proofs and reduce the burden of refereeing new work. ^ this section should have been in the first few paragraphs imho. Explaining why this is relevant shouldn't be so far down.

Isn't it the cost we care about, rather than the speed? All we know know is that a frontier AI lab was able to do it in 11 days, we have no idea how much compute they threw at it.

Re: Formalizing Fermat's Last Theorem

#219

Post by slowin » Fri, Sep 04, 2026, 9:48 PM UTC

nutjob2 wrote: post #101

tinfoilhatter wrote: post #75

Earlier quoted context omitted.

It's wild to think that aging is something that needs to be cured, and isn't a part of the natural human experience. I'm so tired of people trying to play the role of God, as well as people that cheer these sorts of things on.

Most people want more life. For most people it's also the most terrifying part of "the natural human experience". If you're happy to die, why be bothered by others' trying to live longer? You won't be around. And assuming people can finance it themselves, is it really a problem for society?

There are cultures where dying isn't feared like it is in Christian based societies. It's considered a natural progression and part of nature.

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

Re: Formalizing Fermat's Last Theorem

#220

Post by jmusall » Fri, Sep 04, 2026, 9:49 PM UTC

KaiserPister wrote: post #39

13M LoC, are we sure it didn't exploit any latent issues in the lean proof system?

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.