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

431–440 of 531 posts

Re: Formalizing Fermat's Last Theorem

#431

Post by Smaug123 »

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

The LLM is not the thing applying the logical rules. That is instead the deterministic system Lean 4. (Also that Apple paper was garbage even when it was written, assuming you’re referring to The Illusion of Thinking, and LLMs have got much better since.)

Re: Formalizing Fermat's Last Theorem

#432

Post by robotpepi »

lepton wrote: post #414
raincole wrote: post #357

Earlier quoted context omitted.

The answer is we don't really know [0]: > In 2026, AIs designed to spot bugs in software were directed at Lean, and found several loopholes which were then fixed. Perhaps related to this effort, a purported disproof of the Collatz conjecture was announced as verified in Lean. However, this proof was soon determined to rely on a bug in Lean, and once the bug was fixed the proof was found invalid However it's a bit dif…

What are the chances that a small C program uncovers a bug in the C compiler, maybe in its type checker? What are the chances that a very large C program uncovers a bug in the C compiler?

you're missing the point...

Re: Formalizing Fermat's Last Theorem

#433

Post by robotpepi »

not-so-darkstar wrote: post #429
thevivekpandey wrote: post #352

Earlier quoted context omitted.

In lean, a theorem is specified by a type (in their highly complex "dependent type system") and proof is specified by a code that produces a term of that type. If the compiler certifies that the code indeed produces a term of that type, then the proof is correct. So, only need to trust: (1) That theorem statement is correctly encoded (FLT has a very short 1 liner description really) (2) Lean compiler is correct

What if the mathematical objects are not encoded "correctly"? For example, everyone knows that the natural numbers and simple data structures like lists or trees can be encoded with inductive types, but what about the new objects introduced by the proof?

that's something a human needs to do, and it's non trivial, but it's a simple task compared to checking the correctness of the proof. in any case, most of the language is probably already defined in Lean and checked independently by many people.

Re: Formalizing Fermat's Last Theorem

#434

Post by Smaug123 »

kccqzy wrote: post #181
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.

The next step, if Anthropic is interested, is definitely performing refactoring to cut down on the size of the proof. It’s clear to everyone including Anthropic that this proof isn’t as concise as it could have been. When it’s concise enough to be accepted into Mathlib is when victory truly is upon us.

You don’t necessarily want concision for that. You want “the right abstractions”, with an API that admits nice general work building on top of it. That might mean doing things in more generality than you wanted to. For example, for a long time (and possibly even now, I’m not up to date) there was very little graph theory in mathlib because there wasn’t consensus about what “the right definition” of a graph was, to permit all the possible consumers to get what they need from the API.

Re: Formalizing Fermat's Last Theorem

#435

Post by euroderf »

chvid wrote: post #370
alok-g wrote: post #321

Earlier quoted context omitted.

If AI manages to prove, or disprove, I wonder what would Clay Foundation do for the prize.

Who cares about some billionaire paying another billionaire a million dollars? WHat matters is our understanding of maths, and whether this sort of thing makes us smarter or stupider.

Proving Riemann sure would clean up a lot of contingent/dependent number theory.

Re: Formalizing Fermat's Last Theorem

#436

Post by bananaflag »

bigyabai wrote: post #264
tintor wrote: post #189

Earlier quoted context omitted.

Most of the kids in history died before age 5. Child mortality is very low now compared to the past, thanks to the modern medicine and technology. I am glad humanity "played God", and reduced this unnecessary child suffering.

They didn't die of senescence.

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

Re: Formalizing Fermat's Last Theorem

#437

Post by not-so-darkstar »

robotpepi wrote: post #433
not-so-darkstar wrote: post #429

Earlier quoted context omitted.

What if the mathematical objects are not encoded "correctly"? For example, everyone knows that the natural numbers and simple data structures like lists or trees can be encoded with inductive types, but what about the new objects introduced by the proof?

that's something a human needs to do, and it's non trivial, but it's a simple task compared to checking the correctness of the proof. in any case, most of the language is probably already defined in Lean and checked independently by many people.

I think the other commenters are right, as long as the statement of FLT is correct and no funny stuff is used (admitting theorems without proof or defining new axioms) then it doesn't matter what you used in the proof.

Re: Formalizing Fermat's Last Theorem

#438

Post by vitriol83 »

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 work of making it digestible for everyone else, and so in my view this work in particular has negative societal value.

Re: Formalizing Fermat's Last Theorem

#439

Post by lukewarm707 »

CaptWorld wrote: post #388
lukewarm707 wrote: post #306

Earlier quoted context omitted.

a) classic goodhart is using gdp as a measure of prosperity. the government sets a prosperity target. to increase prosperity the government makes workers increase gdp by working 16 hours per day. gdp increases. prosperity is up! the metric is now poisoned. b) how and why could human welfare get worse in a growing economy, really the list is long. one example, unsustainable industries grow but do not create surplus. t…

A) that's a bad model to think. You are of the mind that working more hours is the only way to measure gdp whereas increase in productivity with tools like AI, machinery, tech etc can act as a multiplier. So this way you are conflating bad ways to increase gdp with good ways like AI. That's how US is powerhouse as they are basically a technological hub of the world. B) ha? More fish means couple of things.. they're a…

come on. you asked for a fuller justification and then disparage me for writing a screed and ted talk. those are my thoughts about it.

nonetheless thank you for sharing a rejoinder.

Re: Formalizing Fermat's Last Theorem

#440

Post by 123aHgf »

logicprog wrote: post #317
3192987 wrote: post #87

Earlier quoted context omitted.

And human salaries for those who worked on the prover harness etc. which isn't just standard Fable. It also uses Prove2Me, which uses a graph like previous automated theorem provers. A fact that LLM hawks have categorically denied here before, with opposition naturally flagged. Now they have it in writing.

> A fact that LLM hawks have categorically denied here before, with opposition naturally flagged. Yeah, because before now there's been literally zero proof of an automated theorem prover scaffold around the LLMs being used, and big counterexamples and such being found, with raw chat logs available, where no such thing was used. > Now they have it in writing. Yeah, because now it's actually being done . They talk abo…

Wrong. AlphaProof is much older, used Lean and a tree search for tactics just like ACL2.

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.

Post reply on HN