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

511–520 of 526 posts

Re: Formalizing Fermat's Last Theorem

#511

Post by auggierose »

vitriol83 wrote: post #470
auggierose wrote: post #462

Earlier quoted context omitted.

You can say that American society made OpenAI and Anthropic possible. No other current society would have. Suddenly, formalisation of math is becoming cheap. That's not a problem, that's the goal, and it is here much earlier than expected. That's not antisocial. That is scientific progress. (I swear, did not use an LLM for this)

You're stating it's not a problem- but I'm giving you a reason why it is. This is serendipitously mirrored by a recent post from Terence Tao on Mastodon ( https://mathstodon.xyz/@tao/117207856734787448 ) In most cases in pure mathematics, the problems are posed not because we desperately want the solution to these problems in and of themselves, but because we have seen from past experience that human-directed efforts…

Yes. But that is a problem for pure mathematics, not for society. I think that pure mathematics is over. At the same time, applied mathematics will probably subsume most of pure mathematics. Fermat's theorem now is applied mathematics! It will be used to improve implementations of proof assistants for a long time.

Re: Formalizing Fermat's Last Theorem

#512

Post by dang »

jonesn11 wrote: post #508
dang wrote: post #123

Earlier quoted context omitted.

Thanks! I've added that link to the toptext. I'd really like to make it the top link (and relegate https://www.anthropic.com/research/formalizing-fermats-last-... to the toptext) since HN has been tracking the work of https://news.ycombinator.com/user?id=kevinbuzzard for a long time and we're big fans. But I guess that would be overkill.

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

Hey! If you know more than others (which I'm guessing you do), that's great - but in that case can you please share some of what you know, so the rest of us can learn? If you only post a putdown, it just makes the thread mean and the rest of us don't get to learn anything.

https://hn.algolia.com/?dateRange=all&page=0&prefix=true&sor...

Re: Formalizing Fermat's Last Theorem

#513

Post by jasomill »

andriy_koval wrote: post #466
Smaug123 wrote: post #463

Earlier quoted context omitted.

As I have said a few times now, you should read any first course in set theory. I’m quoting my third-year notes from Cambridge there, but essentially every intro to set theory will say the same. (I’m sure someone will find a single counterexample that does it somehow differently.)

Your third year notes from Cambridge has very low authority to me

Formally, a function f is a relation between sets A and B such that, for all x in A and u,v in B, f(x) = u and f(x) = v implies u = v.

It's just a definition. Authority is, as the parent suggests, any introduction to set theory.

Re: Formalizing Fermat's Last Theorem

#514

Post by andriy_koval »

jasomill wrote: post #513
andriy_koval wrote: post #466

Earlier quoted context omitted.

Your third year notes from Cambridge has very low authority to me

Formally, a function f is a relation between sets A and B such that, for all x in A and u , v in B , f ( x ) = u and f ( x ) = v implies u = v . It's just a definition. Authority is, as the parent suggests, any introduction to set theory.

> Formally, a function f is a relation

discussion was if zfc has functions at all, not sure why you put relation here.

Re: Formalizing Fermat's Last Theorem

#515

Post by 2muchcoffeeman »

aurareturn wrote: post #493
2muchcoffeeman wrote: post #253

Earlier quoted context omitted.

The token price seems like a poor measure. Building the LLM that could do this work in 11 days cost multi billions. The economics probably only make sense if LLMs prove to be a benefit to almost everyone in a way we can all accept. Otherwise this cost a lot more than we’d otherwise pay. It was incredibly fast though. But we all know: cost, speed, quality. Pick two.

Human mathematicians also have to eat right, trained, etc.

ChatGPT has raised over 120 billion USD in funding.

For argument let’s just say we paid all the mathematicians 200k in salary from graduation till retirement. Say 40 years. That’s about 8 million. Let’s round that up to USD 10 million. We can see the future and pay to raise all the baby mathematicians.

For 100 billion that’s 10000 mathematician lifetimes. For 1 AI company _so far_.

There’s no value for money in AI yet.

Re: Formalizing Fermat's Last Theorem

#516

Post by throw567643u8 »

throw-qqqqq wrote: post #461
throw567643u8 wrote: post #411

Earlier quoted context omitted.

So would you also say no chance of a stack overflow or any type of surreptitious storage overflow anywhere in the runtime do you think?

I would say it’s very unlikely to be the case here at least. Of course some bugs in Lean may exist (I don’t have deep insight into Lean’s implementation and there have been bugs before), but I find it unlikely to be systematical or in a format that could affect the proof. As I understand it, Lean is implemented in Lean and emits/compiles to C. In that C code, I’d be very surprised if any buffer overflows or stack ove…

No I don't have any reason to believe you are mistaken other than general suspicion.

Re: Formalizing Fermat's Last Theorem

#517

Post by aurareturn »

2muchcoffeeman wrote: post #515
aurareturn wrote: post #493

Earlier quoted context omitted.

Human mathematicians also have to eat right, trained, etc.

ChatGPT has raised over 120 billion USD in funding. For argument let’s just say we paid all the mathematicians 200k in salary from graduation till retirement. Say 40 years. That’s about 8 million. Let’s round that up to USD 10 million. We can see the future and pay to raise all the baby mathematicians. For 100 billion that’s 10000 mathematician lifetimes. For 1 AI company _so far_. There’s no value for money in AI ye…

Well, it's taken 4 billion years for life to evolve into humans to be able to do math. That's a lot of resources, right?

Likewise, LLMs also needed the same amount of evolution.

My point is that it's silly to make these comparisons on resources. A single SOTA trained LLM isn't just doing advanced math research. It's used by hundreds of millions or even billions daily for various tasks. It's just a tool humans invented.

Re: Formalizing Fermat's Last Theorem

#518

Post by vitriol83 »

auggierose wrote: post #511
vitriol83 wrote: post #470

Earlier quoted context omitted.

You're stating it's not a problem- but I'm giving you a reason why it is. This is serendipitously mirrored by a recent post from Terence Tao on Mastodon ( https://mathstodon.xyz/@tao/117207856734787448 ) In most cases in pure mathematics, the problems are posed not because we desperately want the solution to these problems in and of themselves, but because we have seen from past experience that human-directed efforts…

Yes. But that is a problem for pure mathematics, not for society. I think that pure mathematics is over. At the same time, applied mathematics will probably subsume most of pure mathematics. Fermat's theorem now is applied mathematics! It will be used to improve implementations of proof assistants for a long time.

facepalm yet pure mathematics has been instrumental in all scientific progress in modern human history including LLMs, very short sighted view

Re: Formalizing Fermat's Last Theorem

#519

Post by qbit42 »

tsimionescu wrote: post #504
qbit42 wrote: post #417

Earlier quoted context omitted.

You just have to trust the statement and the lean compiler, not the proof. The compiler certainly still has remaining bugs, but I have never seen a bug leading to a false proof in good faith, only via obscure meta programming tricks. The nice thing is that the multiple versions of the compiler are constantly being stress tested. Still, there is plenty of work that could be done to make the compiler more trustworthy /…

This being 13M lines of entirely agent-generated code, we can't be certain it's written in good faith and doesn't actually exploit some weird metaprogramming trick. The agents' goal was to write a proof that Lean prints "correct" on, not to check that the proof of the FLT was valid (which they wouldn't be able to do anyway).

It's not impossible, but I also know of no instances of an AI being told to prove something in Lean and exploiting such tricks. Surely Anthropic also had some agents looking for issues with the generated proofs. Personally, I am also comfortable trusting Kevin Buzzard, who was leading the human team aiming to formalize FLT and discussed this a bit on his blog.

Finally, the good thing about Lean is that if anyone ever finds a new compiler bug (which, by the way, are being searched for extensively using AI), you can correct the bug and recompile any old proofs of which you are suspicious. Any tricks in a false proof must be exploiting a bug in the Lean compiler, so as we increase trust in the compiler over time we also increase trust in every previously compiled proof.

I agree it's not a 100% guarantee, but in this case the human proof is well-understood and written about by many experts, so I think Claude had plenty of material to work with. Even if the task was enormous, I don't think any of the individual steps are out of the scope of what we have seen from current AI tools.

Re: Formalizing Fermat's Last Theorem

#520

Post by Brian_K_White »

aurareturn wrote: post #517
2muchcoffeeman wrote: post #515

Earlier quoted context omitted.

ChatGPT has raised over 120 billion USD in funding. For argument let’s just say we paid all the mathematicians 200k in salary from graduation till retirement. Say 40 years. That’s about 8 million. Let’s round that up to USD 10 million. We can see the future and pay to raise all the baby mathematicians. For 100 billion that’s 10000 mathematician lifetimes. For 1 AI company _so far_. There’s no value for money in AI ye…

Well, it's taken 4 billion years for life to evolve into humans to be able to do math. That's a lot of resources, right? Likewise, LLMs also needed the same amount of evolution. My point is that it's silly to make these comparisons on resources. A single SOTA trained LLM isn't just doing advanced math research. It's used by hundreds of millions or even billions daily for various tasks. It's just a tool humans invente…

It's just a wildly inefficient tool whos inefficiency is obscured so no one realizes how bad it is and everyone thinks the good part is the only part.
Post reply on HN