Formalizing Fermat's Last Theorem • Hacker News Board

Re: Formalizing Fermat's Last Theorem

#331

Post by SoMomentary » Sat, Sep 05, 2026, 1:03 AM UTC

beepbooptheory wrote: post #299

salomonk_mur wrote: post #132

Earlier quoted context omitted.

For any body of text (or in general, any exposition of any kind), the responsibility to explain the value of the article is very much in the author's side. Explaining the value of what you are showing should always go towards the start. Else, why would anyone bother with the rest?

Feel very grateful I was never taught this... Would have missed out on quite a lot of good bodies of text in my life I think! Pushing through any initial friction or ignorance I might have as a reader, having the patience and charity to bear with an author until you get it, was instead what I was always taught. Giving such a blanket "responsibility" to the author at all is just such a bummer! I say let them do whatev…

Unfortunately I don't see this particular view paying off in the age of AI, as many prove they have nothing at all to say but say it anyways. Which isn't to say people shouldn't write if they enjoy writing, but I for one will stay a discerning reader.

Re: Formalizing Fermat's Last Theorem

#332

Post by andriy_koval » Sat, Sep 05, 2026, 1:04 AM UTC

drdeca wrote: post #325

andriy_koval wrote: post #226

Earlier quoted context omitted.

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

ZFC has greater consistency strength than PA. If we take ZFC (or some other set theory) as our meta theory, we can easily see that the axiom of infinity (of ZFC) gives a set of natural numbers (using the von Neumann encoding), which, when equipped with the successor function, is a model of the natural numbers.

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.

Re: Formalizing Fermat's Last Theorem

#333

Post by andriy_koval » Sat, Sep 05, 2026, 1:05 AM UTC

drdeca wrote: post #328

andriy_koval wrote: post #208

Earlier quoted context omitted.

do we know if claude's formalization is built on top of zfc and not zfc+extra? zfc itself is not sufficient, you need some layers of extra concepts formalization to fit specific problem domain(e.g. zfc doesn't define even basic arithmetics), which also could have potential issues.

Within a given inference system, one can define concepts. This doesn’t add any axioms. It is, in essence, just a way to abbreviate things.

ok, you now added some unknown inference system in addition to zfc

Re: Formalizing Fermat's Last Theorem

#334

Post by SoMomentary » Sat, Sep 05, 2026, 1:05 AM UTC

doctoboggan wrote: post #218

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.

They said 6 billion tokens, which isn't as much as I thought it might be.

Re: Formalizing Fermat's Last Theorem

#335

Post by throw567643u8 » Sat, Sep 05, 2026, 1:16 AM UTC

13 million lines of code, a lot of which is new to Mathlib. So it hasn't built on what is already there but synthesised a bunch of new stuff.

LLM generated Lean code in the past has been known to exploit bugs in the Lean kernel, it would be foolish to rule this out happening again.

Re: Formalizing Fermat's Last Theorem

#336

Post by 9763268964 » Sat, Sep 05, 2026, 1:20 AM UTC

tinfoilhatter wrote: post #75

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…

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.

[dead]

Re: Formalizing Fermat's Last Theorem

#337

Post by throw567643u8 » Sat, Sep 05, 2026, 1:26 AM UTC

I'd feel so much more excited if this was done in Metamath. Tiny checker kernel, no complicated dependent types, way less to go wrong.

Re: Formalizing Fermat's Last Theorem

#338

Post by fyredge » Sat, Sep 05, 2026, 1:27 AM UTC

CaptWorld wrote: post #194

oblio wrote: post #172

Earlier quoted context omitted.

Or we could invest in a ton of other non AI related research we're underinvesting in.

Like? I feel breakthroughs that can be found via AI might help us more in the long term where even previously non AI fields can be helped by AI. So you have specific non AI research in mind that we're underinvesting in? Because the USA is already spending crazy anyway for healthcare and I don't feel like funding is the issue but better incentives, reforms etc

Like funding education. Let's build up human intelligence instead, they seem to have made great breakthroughs in every single field!

The US doesn't pay too much to healthcare, they pay too much to health insurance. Too much for too little value

Re: Formalizing Fermat's Last Theorem

#339

Post by hackandthink » Sat, Sep 05, 2026, 1:28 AM UTC

UltraSane wrote: post #300

glimshe wrote: post #205

"The proof is not the modern proof which I have been formalizing myself following ideas of Khare, Taylor etc, but the Darmon–Diamond–Taylor exposition from 1995 of the Wiles–Taylor–Wiles argument, via the Langlands–Tunnell theorem and Ribet’s level-lowering theorem. Anthropic’s repository develops Fontaine theory (to study flat deformations of Galois representations) and develops enough of Mazur’s work on the Eisenst…

advanced math like this takes 10 years to learn all the tower of things it is based on.

if you are a fast learner

Re: Formalizing Fermat's Last Theorem

#340

Post by mathisfun123 » Sat, Sep 05, 2026, 1:28 AM UTC

glimshe wrote: post #205

"The proof is not the modern proof which I have been formalizing myself following ideas of Khare, Taylor etc, but the Darmon–Diamond–Taylor exposition from 1995 of the Wiles–Taylor–Wiles argument, via the Langlands–Tunnell theorem and Ribet’s level-lowering theorem. Anthropic’s repository develops Fontaine theory (to study flat deformations of Galois representations) and develops enough of Mazur’s work on the Eisenst…

This question gets asked every single time a serious mathematical result gets posted.