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

101–110 of 526 posts

Re: Formalizing Fermat's Last Theorem

#101

Post by nutjob2 »

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.

Most people want more life. For most people it's also the most terrifying part of "the natural human experience".

If you're happy to die, why be bothered by others' trying to live longer? You won't be around. And assuming people can finance it themselves, is it really a problem for society?

Re: Formalizing Fermat's Last Theorem

#102

Post by _aavaa_ »

sebzim4500 wrote: post #93
BeetleB wrote: post #27

Earlier quoted context omitted.

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

It sounds plausible they spent more, given the output tokens (6 billion of them) would cost $300k at API prices and presumably there will have been many more input tokens than output tokens.

Unlikely, api pricing includes a healthy profit margin (as near as we can tell from the outside) which they wouldn’t charge themselves.

Re: Formalizing Fermat's Last Theorem

#104

Post by lukewarm707 »

yesitcan wrote: post #49
dakolli wrote: post #30

Earlier quoted context omitted.

You'll get mass poverty and violence which the owners of AI will qwell with AI surveillance and weapons. AI will be used to pit us against eachother and justify wars to keep us busy. Fun times ahead. Not sure why anyone is excited about this tech.

So much doom and gloom on this site. Makes it almost not worth reading.

my messages are so gloomy because i am heartbroken, that given a technological miracle again, we could snatch tragedy from the jaws of our emancipation.

will you not see that people could be truly empowered and yet will instead be oppressed?

Re: Formalizing Fermat's Last Theorem

#105

Post by tinfoilhatter »

sebzim4500 wrote: post #98
tinfoilhatter wrote: post #75

Earlier quoted context omitted.

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.

I hope you keep these horrible thoughts to yourself if you ever walk through a paediatric hospital

Thinking that aging is a natural part of the human experience is a horrible thought? Please explain...

Re: Formalizing Fermat's Last Theorem

#106

Post by henryrobbins00 »

Back in February, I was talking with my PhD advisor about using Lean to formally verify automated optimization modeling outputs. It eventually turned into this paper [1]. It’s been truly incredible to see how much the frontier models have progressed in both autoformalization and automated theorem proving in the last six months. Back in February, it was cool to see them prove the validity of some simple cutting planes. Now it can churn out a min-cut max-flow duality formalization (not to mention FLT). Very exciting times!

I’ll also share a Python package I wrote for automated theorem proving that has been super useful in my own research [2].

[1] https://arxiv.org/abs/2608.25220

[2] https://github.com/henryrobbins/open-atp

Re: Formalizing Fermat's Last Theorem

#107

Post by tinfoilhatter »

nutjob2 wrote: post #101
tinfoilhatter wrote: post #75

Earlier quoted context omitted.

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.

Most people want more life. For most people it's also the most terrifying part of "the natural human experience". If you're happy to die, why be bothered by others' trying to live longer? You won't be around. And assuming people can finance it themselves, is it really a problem for society?

I assume you mean that dying is the most terrifying pat of the natural human experience. Also, I'm not sure why you infer that me thinking death is a natural part of life, means that I'm happy or eager to die.

There are many reasons that people living forever would be a problem for society, the most obvious being an ever-increasing population.

Re: Formalizing Fermat's Last Theorem

#108

Post by sweetheart »

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?

maybe it will be an answer that entices them to understand more :)

Re: Formalizing Fermat's Last Theorem

#109

Post by fspeech »

First I have to say this is sooner than expected, even though I never doubted that this could be done. I am grateful that they dedicated resources to accomplish this. It is clear that agents are very good at discerning and holding onto very weak signals from RL traing on long horizon tasks, so much so that in my own experience even very chaotic agent thinking can converge to meaningful solutions if there is a verifier. I have not dug through the proof yet so I don't know how readable it is to a human. But it has been a dream of mine to understand the FLT proof. I think LLMs will be a big part of making it truly accessible to humans.

Re: Formalizing Fermat's Last Theorem

#110

Post by Smaug123 »

KaiserPister wrote: post #39

13M LoC, are we sure it didn't exploit any latent issues in the lean proof system?

It is possible, although the post notes that the proof was also verified by the Comparator, which means any exploited bug has to also be present in that checker. Which is not unheard of, but is much less likely than merely an exploit in Lean 4.
Post reply on HN