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

281–290 of 523 posts

Re: Formalizing Fermat's Last Theorem

#281

Post by iterateoften »

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

How many previous attempts with other models failed or on other problems. Perhaps this is $300k out of $100M or $1B of total budget just breadth first searching theorems in math and all the failed attempts conveniently don't get mentioned.

Re: Formalizing Fermat's Last Theorem

#283

Post by Philpax »

mikmoila wrote: post #279
Philpax wrote: post #277

Earlier quoted context omitted.

We don't know what they do. We shape them, but our understanding of how they get to their result is comparatively minimal.

I think you're referring to the fact that the sheer amount of computations is something too time consuming for us to follow? But still it is not "magical" - in theory we could follow all the steps, there's no hidden information.

No, I mean we just don't know what's going on in the circuits of the model at any substantial level. We set their architecture (hyperparameters), we pump them full of data (pretraining), and we shape how they behave through examples (SFT) and reward (RL), but we can't say with any certainty what the resulting model does internally.

You can scroll through https://transformer-circuits.pub/ to see the ~extent of our current understanding.

Re: Formalizing Fermat's Last Theorem

#284

Post by sanxiyn »

QuesnayJr wrote: post #136

Holy shit. The proof of FLT is a giant detour through several different areas of mathematics, so formalizing it is a lot of work. An interesting next target would be formalizing the classification of finite simple groups. The original proof scattered over thousands of pages of journal articles, plus Aschbacher and Smith's 1300 page 2 volume monograph. It's so long it's hard to know if there are any gaps. Researchers…

New proof: The Classification of the Finite Simple Groups (American Mathematical Society Mathematical Surveys and Monographs vol. 40).

https://www.ams.org/publications/authors/books/postpub/surv-...

Number 1 (1994), Number 2 (1995), Number 3 (1997), Number 4 (1999), Number 5 (2002), Number 6 (2004), Number 7 (2018), Number 8 (2018), Number 9 (2021), Number 10 (2023). 10 volumes and >4000 pages so far, number 11 is in progress, and end is in sight, probably two more volumes or so.

https://www.ams.org/journals/notices/201806/rnoti-p646.pdf

People were curious what is going on during 2004-2018. A progress report was published in 2018 right before publication of number 7 and 8. In a sense it was the peak, number 8 completes the proof of so-called "generic case". The rest is "special case". It doesn't mean things get easier, but in some specific sense number 8 completed proof for almost all groups.

Now new proof's end is in sight, people are planning new new proof.

Re: Formalizing Fermat's Last Theorem

#285

Post by Azantys »

threethirtytwo wrote: post #190

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

The whole point was for the formalization to be clean enough so it could be reused in other parts of mathematics as I understand it. 13M lines of AI slop which have never been checked do not sound like what the original goal for such a formalization was. Also Claude didnt prove anything it just translated an already existing proof by Wiles into Lean, so it didn't actually contribute anything other than "Guys we did this thing, look how great our model is!". We never questioned that a printer can print faster than a human can write, but we dont let printers write novels.

Re: Formalizing Fermat's Last Theorem

#286

Post by mikmoila »

Philpax wrote: post #283
mikmoila wrote: post #279

Earlier quoted context omitted.

I think you're referring to the fact that the sheer amount of computations is something too time consuming for us to follow? But still it is not "magical" - in theory we could follow all the steps, there's no hidden information.

No, I mean we just don't know what's going on in the circuits of the model at any substantial level. We set their architecture (hyperparameters), we pump them full of data (pretraining), and we shape how they behave through examples (SFT) and reward (RL), but we can't say with any certainty what the resulting model does internally. You can scroll through https://transformer-circuits.pub/ to see the ~extent of our cur…

Yes "at any substancial level" . But still, its all about deterministic processes and still it obeys the law that the same input gives the same output. Or do you mean that the fluctuations like computing environment might ruin the determinism?

Re: Formalizing Fermat's Last Theorem

#287

Post by Almondsetat »

andriy_koval wrote: post #272
Almondsetat wrote: post #269

Earlier quoted context omitted.

A quick google search shows different proof assistants have been used to obtain the Peano axioms from ZFC, such as Isabelle/ZF and Metamath. I think you're just wrong

you are entitled to have your opinion :-)

and you are entitled to talk about maths while rejecting maths

Re: Formalizing Fermat's Last Theorem

#289

Post by jascination »

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.

1kk? Why not say 1M?

Re: Formalizing Fermat's Last Theorem

#290

Post by johnsmith1840 »

mikmoila wrote: post #270
johnsmith1840 wrote: post #263

Earlier quoted context omitted.

A literal rock we carved patterns on and shot lightning into has accomplished something no human has. How much more magical do you want this to be? Tool or not it did something you could never have accomplished.

"you could never have accomplished"; I am not able to follow the logic here - there is no "magic" in LLMs, they're built by humans and we know what they do.

Sure? I mean the internet is just a bunch of wires and some networking code not magic but at the same completely life alteringly magical.

My logic is that you personally could never have accomplished this feat with all the non LLM tools and content in the world. These kinds of things imply these methods are stepping beyond human ability.

Sure we put walls around it and optimize but the interior of that optimization is not something we understand.

You now have access to a system that for a price could solve something you simply are unable to solve. Not something we programmed it to solve, something that has never been solved before.

Nobody gave it an example of this proof, that's magical.

Post reply on HN