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

451–460 of 527 posts

Re: Formalizing Fermat's Last Theorem

#451

Post by xvilka »

kingstnap wrote: post #77
KaiserPister wrote: post #39

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

The AI labs have out considerable effort in trying to find and patch lean exploits. They explicitly set agents and have them try to prove false. > Daniel used OpenAI internal models to discover new soundness issues in the official Lean kernel and runtime https://leodemoura.github.io/blog/2026-8-24-postmortem-for-t... They found several bugs and they have patched them. Lots of work going into making sure lean is sound…

Some argue that Lean breaks a few type-theoretical properties. See full discussion here:

https://github.com/rocq-prover/rocq/issues/10871

Re: Formalizing Fermat's Last Theorem

#452

Post by amelius »

FartyMcFarter wrote: post #419
amelius wrote: post #418

They should let AI work on it until the proof fits in the margin of a page.

5 minutes later, the AI concludes the best strategy is to start a universe simulation and let Fermat write the proof in a margin. Recurse.

Yeah they tried that, but the proof didn't fit.

Re: Formalizing Fermat's Last Theorem

#453

Post by ndriscoll »

kzrdude wrote: post #441
stratos123 wrote: post #71

Earlier quoted context omitted.

encode mathematical reasoning in a way that can’t be fooled. I would be a bit careful asserting that in full generality, given https://github.com/James-Hanson/junk-theorems-in-lean

Some kind of linter should flag these with a warning, I think

As with many programming languages, you can use phantom types to prevent this sort of thing, and in fact, that's exactly what's happening but they make it sound extra silly when they throw away the safety wrapper. That's why some of these have weird statements like the third coordinate of . Some of these amount to, "if you have 3 apples and 5 oranges, and you just take the raw numbers and add them, you get 8," and then layer it with an extra level of obfuscation, like "if you have the second prime number apples, and the third prime number oranges, and take the raw numbers and add them, you get the first prime number to the power of the second prime number."

Re: Formalizing Fermat's Last Theorem

#454

Post by auggierose »

jeanmichelselli wrote: post #420

I'm a mathematician and I'm not sure one should believe those results right now.. An automatic formalization requires a system of logic rules to be applied, which is not something LLMs are great at (remember the Apple paper a while ago?). I'm very curious to see how the community will react after the initial hype.. so far, it's being quite disappointing..

Kevin Buzzard is a mathematician as well, and he thinks it's ok. I am a mathematician, too, and I know it is ok. What I find fascinating is how little mathematicians still know about this. But I am used to that attitude towards interactive theorem proving for quite some time. The difference now: if you don't adapt, you are obsolete and done for as a mathematician.

Re: Formalizing Fermat's Last Theorem

#455

Post by auggierose »

vitriol83 wrote: post #438

i find this and other efforts from anthropic somewhat antisocial. technically they have achieved their goal, but in a way which does not benefit mathematics or humanity. Kevin Buzzards headline goal was to formalise FLT, but i’m sure the real aim was to create a formalised library of mathematics which is comprehensible to humans. By solving these famous problems by brute force, they are disincentivising the important…

Maybe society has the wrong values. Maybe society needs to rethink incentives. Maybe society is somewhat antisocial.

Re: Formalizing Fermat's Last Theorem

#456

Post by andriy_koval »

Smaug123 wrote: post #403
andriy_koval wrote: post #291

Earlier quoted context omitted.

coming back to your argument about peano being obtained from zfc, you obviously can't prove that it happened using purely zfc, and not some logical framework embedded into those proof assistants. I said I am not expert, I am indeed not expert in zfc and godel theorems, but I am an expert (phd) in actual formalization theory. Formal theory is very simple concept: its alphabet, set of formulas on top of this alphabet,…

Eh? Any first course in set theory will present ZFC as a one-sorted theory with ten axioms (/schemas) in first order logic (inheriting an equality symbol, forall, implies etc) with one binary predicate (namely set membership), or will present a theory that is equiconsistent with a usual ZFC presentation. Honestly I’m not sure how you simultaneously claim to be a PhD in formalisation and also not be aware of the exist…

> Honestly I’m not sure how you simultaneously claim to be a PhD in formalisation and also not be aware of the existence of Isabelle/ZF, for example.

I am aware, also I am not sure why you wrote all of this. Your unknown to me "first course" claims to be some authority of formalization purity?

Re: Formalizing Fermat's Last Theorem

#457

Post by vitriol83 »

auggierose wrote: post #455
vitriol83 wrote: post #438

i find this and other efforts from anthropic somewhat antisocial. technically they have achieved their goal, but in a way which does not benefit mathematics or humanity. Kevin Buzzards headline goal was to formalise FLT, but i’m sure the real aim was to create a formalised library of mathematics which is comprehensible to humans. By solving these famous problems by brute force, they are disincentivising the important…

Maybe society has the wrong values. Maybe society needs to rethink incentives. Maybe society is somewhat antisocial.

yes society has let the trillion dollar company down

Re: Formalizing Fermat's Last Theorem

#458

Post by andriy_koval »

Smaug123 wrote: post #404
andriy_koval wrote: post #332

Earlier quoted context omitted.

zfc doesn't have functions, so you are building something new on top of it. Also, I am not sure successor function is enough for PA.

It simply does have functions. According to ZFC, a function is a set whose members are pairs, such that no two different pairs have the same first element. I mean this quite seriously: have you considered reading any first course in set theory?

> According to ZFC, a function is a set whose members are pairs, such that no two different pairs have the same first element.

Can you cite where did you get this?

Re: Formalizing Fermat's Last Theorem

#459

Post by andriy_koval »

IsTom wrote: post #406
andriy_koval wrote: post #259

Earlier quoted context omitted.

> interpreted its hard to me to tell what this means formally(as I said I am not expert). There is no "interpret" operator in zfc. I believe what it says if you add some robinson axioms + some logical rules on top of zfc, you can carry your results.

It's the same way you don't need to have GCD in stdlib to say that you can compute GCD in C++. You can make your own using parts given. You don't need to add any axioms, you just build some sets to represent numbers and make operations that act the same way as arithmetic, define some equality relations. Then you derive rules of arithmetic for your handcrafted arithmetic using ZF axioms and you're good. You get axioms…

> you just build some sets to represent numbers and make operations that act the same way as arithmetic

which is already "just" some non trivial problem(there is no "operations" in set theory), and we are discussing if it is achievable.

Re: Formalizing Fermat's Last Theorem

#460

Post by btilly »

chpatrick wrote: post #308
btilly wrote: post #302

Earlier quoted context omitted.

Amazon didn't make a profit because they were reinvesting money into starting new lines of business. Basically there was a choice between taking the money, and growing. They chose growth.

As opposed to...?

As opposed to building a bigger bank account, or paying dividends.
Post reply on HN