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

181–190 of 526 posts

Re: Formalizing Fermat's Last Theorem

#181

Post by kccqzy »

m_w_ wrote: post #7

> Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems. Pretty insane. I suppose it lends further credence to the idea that anything that can be shown to be correct can be done by a model.

The next step, if Anthropic is interested, is definitely performing refactoring to cut down on the size of the proof. It’s clear to everyone including Anthropic that this proof isn’t as concise as it could have been. When it’s concise enough to be accepted into Mathlib is when victory truly is upon us.

Re: Formalizing Fermat's Last Theorem

#183

Post by CaptWorld »

dakolli wrote: post #126
yesitcan wrote: post #49

Earlier quoted context omitted.

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

Please tell me how AI is going to make regular people's lives better. You optimisitic types keep saying "just wait, its going to cure diseases" without any outlook on how thats going to happen. You're actually just repeating marketing jargon from AI companies who want people to think they're going to possibly live longer if you let them build more datacenters, so they can make another 30%. Its all about money, thats…

Can't you see the pathway where the individuals who are experts in their fields utilise AI to make breakthroughs like these mathematicians finding breakthroughs in mere 4-5 years since the advent of LLMs. In other areas, The bottleneck seems to be physical experimentation which researchers are increasingly utilising for new ideas and pathways like how anthropic is concentrating on. It's all about money/status/pride/ envy but are these endeavours solving problems or not. That's why even utilize innovations from bad humans like DBS etc. that's why we tolerate capitalism and markets as well whereas socialism utilises these same sins and makes even worse human atrocities.

Re: Formalizing Fermat's Last Theorem

#184

Post by CaptWorld »

bobmarleybiceps wrote: post #112
babelfish wrote: post #57

Earlier quoted context omitted.

A human definitely didn't, but one of the benefits of formal verification is that even if the work done to achieve something is slop-y or excessively verbose, solvers like Lean guarantee that the initial proposition (assuming it was written correctly and in this case was definitely reviewed by humans) is definitively True. This is true across other domains of formal verification outside of math as well

guaranteed, up to lean itself having bugs that are exploited by the LLM :shrug:

Do you have proof of this bug or something? Is this just envy against computers now ?

Re: Formalizing Fermat's Last Theorem

#185

Post by jjtheblunt »

>. Claude produced the first end-to-end, computer-checked proof of FLT. Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems.

I'm just old enough to remember Paul Erdo"s and his notion of 'The Book', which he defined to be a book the "Supreme Fascist" (God) had which held the most elegant proofs of mathematical theorems.

https://en.wikipedia.org/wiki/Paul_Erdős#Personal_life

It would be interesting to see how Erdo"s would name such a huge proof by Claude using Lean.

Re: Formalizing Fermat's Last Theorem

#187

Post by dataking »

tinfoilhatter wrote: post #107
nutjob2 wrote: post #101

Earlier quoted context omitted.

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.

> the most obvious being an ever-increasing population

https://en.wikipedia.org/wiki/Thomas_Robert_Malthus

Re: Formalizing Fermat's Last Theorem

#189

Post by tintor »

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 of the kids in history died before age 5.

Child mortality is very low now compared to the past, thanks to the modern medicine and technology.

I am glad humanity "played God", and reduced this unnecessary child suffering.

Re: Formalizing Fermat's Last Theorem

#190

Post by threethirtytwo »

>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. My guess is that it is unlikely that Anthropic are going to do this; they will feel that their job is done with the formalization (and they did not formalize the modern proof anyway).

What is even the point? Have claude do it.

I'm not trying to be snarky here. I'm being serious. What is the point? This is an important question that needs to be answered. If something is definitively better, why not have that something take over?

I know people talk about the importance of human endeavor or the "joy" of doing something. But I don't care for those answers because it's weak. The question is deeper than this. AI is better than us, what is the logical point other than attempting to monopolize human effort even though it is inferior.

Post reply on HN