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

241–250 of 526 posts

Re: Formalizing Fermat's Last Theorem

#241

Post by mikmoila »

educasean wrote: post #199
mikmoila wrote: post #196

"The effort succeeded when we switched to using Prove2Me, an open collaborative platform for formalizing mathematics designed by Tianyi Peng and his collaborators at Columbia University." So in the end, it required tooling crafted by humans.

By this standard, no computer has ever accomplished anything, because humans built the computer. AI bubble about to burst any second now.

Humans built the tool which enabled the result. AI used the tooling for eliminating the dead ends. Yes, I can appreciate the practical value of all this, but IMHO it is not a kind of breakthrough result the article gives impression of.

Re: Formalizing Fermat's Last Theorem

#242

Post by kzrdude »

EGreg wrote: post #188

So Fermat’s Last Theorem has been proven a long time ago? By Andrew Wiles right? Is this like Appel and Haken >>> Seymour and Robin Thomas proof of 4CT?

FLT was proven in 1995 by Andrew Wiles (with help of Richard Taylor).

This is not even a new proof, or at least they don't claim that it is. It's the formalization (in Lean) of an existing proof. That means, they are 'porting' the proof to a theorem proving programming language.

Re: Formalizing Fermat's Last Theorem

#243

Post by CaptWorld »

lukewarm707 wrote: post #232
CaptWorld wrote: post #176

Earlier quoted context omitted.

So oppressed that they are one of the main reasons for positive gdp growth in the USA, tax revenues, mathematical/scientific innovations etc. They're doing all this but still can't imagine a positive vision for the world but be a doomer. What a sad state the world is in, the humans are more prosperous, healthier than ever but looks like the seven deadly sins might never go away.

you say ai increases gdp growth, tax revenues and scientific innovations. then you say that ai is good. that is not formally valid. in between those two you are smuggling the assumption that gdp growth, tax revenues and scientific innovations are good. a) those metrics are poisoned, per Goodheart's law. b) they are not good and human welfare will get worse as gdp, tax revenues and innovations grow. i leave b for the…

Which metrics are poisoned? Can you provide your arguments for why Good heart's law applies here and how and which metrics are bad measures? For b, can the writer at least provide their own thoughts or are they gonna leave it as exercise for some others to fill in?

Re: Formalizing Fermat's Last Theorem

#244

Post by [deleted] »

chi_features wrote: post #114

There's a wonderful documentary by BBC Horizon with Andrew Wiles from 1996 – highly recommend! I saw it in the 90's and it's a documentary for everyone. It captures the effort, struggle, highs and lows of a 7 year effort working on Fermat's Last Theorem.

[deleted]

Re: Formalizing Fermat's Last Theorem

#245

Post by IsTom »

andriy_koval wrote: post #226
deepsun wrote: post #207

Earlier quoted context omitted.

There is, or rather are, fully recognized axiomatic foundations. You are free to choose one you like. Of the most popular ones is ZFC or ZF, but there are others (some lead to the same results some not). The main criteria for popularity is how useful it is. You can even make your own axiomatic where 2+2=5, but it would be useless. You probably heard about Goedel Incompleteness -- the proof that the the axiomatic itse…

> Goedel Incompleteness -- the proof that the the axiomatic itself cannot be proven, like using ZFC to prove ZFC, but that's another topic. Godel theorems are for systems with basic arithmetic, zfc doesn't include arithmetic, thus are not object of Godel theorems.

> Moreover, Robinson arithmetic can be interpreted in general set theory, a small fragment of ZFC.

https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_t...

Re: Formalizing Fermat's Last Theorem

#246

Post by AmazingEveryDay »

martinpw wrote: post #231
chi_features wrote: post #114

There's a wonderful documentary by BBC Horizon with Andrew Wiles from 1996 – highly recommend! I saw it in the 90's and it's a documentary for everyone. It captures the effort, struggle, highs and lows of a 7 year effort working on Fermat's Last Theorem.

Looks like it is available here: https://www.dailymotion.com/video/x3wrbsb

Also: https://archive.org/details/BBCHorizonCollection512Episodes/...

Re: Formalizing Fermat's Last Theorem

#247

Post by kzrdude »

yesitcan wrote: post #56
sweetheart wrote: post #32

Earlier quoted context omitted.

Lean _is_ code. FLT cannot be proven by exhaustion because it's domain is an infinite set: the natural numbers above 2.

If they’re asking that kind of question, do you think this answer will help them understand anything?

Yes

Re: Formalizing Fermat's Last Theorem

#248

Post by andriy_koval »

Almondsetat wrote: post #240
andriy_koval wrote: post #237

Earlier quoted context omitted.

support your point with explanation or be ignored :-)

Godel proved that any system expressive enough to produce an arithmetic is incomplete. He initially proved it for the peano axioms but then it got generalized. ZFC can produce an arithmetic. Also, before being arrogant and demanding explanations, you should give them first for your claims

> expressive enough to produce

you understand that "expressive enough to produce" are not obvious elements of zfc, that's some average consumer napkin math and not strict formalization.

Re: Formalizing Fermat's Last Theorem

#249

Post by ndriscoll »

stratos123 wrote: post #71
hyperhello wrote: post #53

Earlier quoted context omitted.

The point of writing Lean code is that Lean checks it accordingly. Lean is a domain specific language to encode mathematical reasoning in a way that can’t be fooled. Note to other users: don’t downvote this kind of comment, answer it.

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

This has nothing to do with Lean, e.g.

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

Re: Formalizing Fermat's Last Theorem

#250

Post by UltraSane »

BeetleB wrote: post #27
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.

"I was given £1M to run my project over 5 years; Anthropic took only 11 days but I do wonder if they spent more money…" Gives you an idea of the scale...

I burned $70 on fable 5.1 Max in about 2 hours. I suggest never using fable 5.1 on higher than High reasoning unless someone else is paying for it.
Post reply on HN