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

311–320 of 524 posts

Re: Formalizing Fermat's Last Theorem

#311

Post by sashank_1509 »

Legend2440 wrote: post #260
skobes wrote: post #228

Earlier quoted context omitted.

Maybe I'm misunderstanding something about how all this works, but can we have any confidence that 13 million lines of AI-generated Lean code are... correct? How have we not merely substituted one verification problem for another?

The point of Lean is that it can be mechanically verified by a proof checker.

Not always, there can be bugs in lean. Recently some guy with claimed to disprove Collatz conjecture, only to turn out that there was a bug in lean. I actually have no idea, how anyone can be sure this 13 M lines is meaningful

Re: Formalizing Fermat's Last Theorem

#312

Post by jibal »

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.

That is wildly wrong.

Re: Formalizing Fermat's Last Theorem

#313

Post by willmarch »

Jtarii wrote: post #86
ben_w wrote: post #55

Earlier quoted context omitted.

> It is truly saddening to think that machines will deprive us of this wonder and experience. It won't deprive us. Recent video I've watched from Brandon Sanderson, IMO also applies to all the things we love and not just art: https://youtu.be/mb3uK-_QkOo?si=SG1uvGUbN6SOYI_J

If the Riemann hypothesis is solved primarily by a AI system it will not be as awe inspiring as if a human solved it. That is just how it is.

Why?

Re: Formalizing Fermat's Last Theorem

#314

Post by skipants »

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…

Funnily enough, this is more readable to me than most Clayde jargon.

Re: Formalizing Fermat's Last Theorem

#315

Post by jibal »

andriy_koval wrote: post #261
Almondsetat wrote: post #252

Earlier quoted context omitted.

why should they be obvious? they are derived and have been thoroughly proven.

looks like we are in disagreement

That increases the likelihood that they are right.

> support your point with explanation or be ignored :-)

Anyone who says "Godel theorems are for systems with basic arithmetic, zfc doesn't include arithmetic, thus are not object of Godel theorems" and isn't joking warrants a permanent ignore.

https://math.stackexchange.com/questions/1366560/why-does-g%...

https://math.stackexchange.com/questions/1090437/how-to-prov...

Re: Formalizing Fermat's Last Theorem

#316

Post by traes »

margorczynski wrote: post #274
jensgk wrote: post #89

Earlier quoted context omitted.

What would it cost to make a team of mathematicians do the same?

Buzzard was given 1kk GBP and 5 years and his goal I think wasn't the full thing like Anthropic did. So much more cash and orders of magnitude more time. The proof is about 5x the whole Mathlib library which was developed over many years by dozens of people.

It's true that his goal was not the full thing, but it was also not merely a Lean verified proof. From the blog post linked in the toptext:

> The work certainly achieves some of the aims of the EPSRC project, and indeed it goes much further in terms of what is formalized (I only promised the EPSRC that I would reduce FLT to the 1980s; this repo proves the whole thing). But I also promised several other things to EPSRC: firstly, that I would be making pull requests to Lean’s mathematics library, adding fundamental objects from modern number theory; this is ongoing. And secondly, and perhaps most importantly, that I would be creating a dynamic document enabling humans to explore the modern proof.

Re: Formalizing Fermat's Last Theorem

#317

Post by logicprog »

3192987 wrote: post #87
davmre wrote: post #74

> a team of agents completed the proof in a little under two weeks, consuming about six billion output tokens from a general-purpose internal research model roughly comparable to Claude Fable 5.1. At $50/M output tokens, this would have cost on the order of $300k (plus a bit for input/prefill tokens) at API rates.

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 about it as a novel thing, because it is. You don't get to claim being "right all along" from this

Re: Formalizing Fermat's Last Theorem

#318

Post by logicprog »

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.

There's nothing about prove2me that couldn't have been coded just like any other huge coding project frontier models have proven themselves extremely good at doing. It just happened to have been made by humans.

Re: Formalizing Fermat's Last Theorem

#319

Post by traes »

chpatrick wrote: post #47
drivebyhooting wrote: post #34

LLMs are pretty good at slogging through. When will they come up with brilliant breakthroughs like Andrew Wiles?

About two month ago: https://en.wikipedia.org/wiki/Jacobian_conjecture

We have absolutely no idea if this was a brilliant breakthrough or not. They haven't released any explanation of how it was found. A problem being old and prestigious does not mean its solution is automatically a brilliant breakthrough.

Re: Formalizing Fermat's Last Theorem

#320

Post by traes »

bjourne wrote: post #36
jrflo wrote: post #17

Holy shit, this has to be one of the most difficult proofs to formalize due to it's length and complexity right?

Yep. There may be only 25-50 people alive today in the whole world who can credibly claim to understand Wiles' proof. Now we add an LLM to that list. Absolutely mind-blowing stuff.

25-50 seems like a pretty lowball estimate, I guess depending on your definition of "understand."
Post reply on HN