Earlier quoted context omitted.
About two month ago: https://en.wikipedia.org/wiki/Jacobian_conjecture
Come on, you can't compare that with Wiles's proof.
Still unsolved for 87 years.
Formalizing Fermat's Last Theorem
131–140 of 524 posts
Re: Formalizing Fermat's Last Theorem
#132>The speed with which we were able to produce this proof demonstrates that it is now possible to formalize large swaths of mathematics, which may both catch errors in the common body of mathematical proofs and reduce the burden of refereeing new work. ^ this section should have been in the first few paragraphs imho. Explaining why this is relevant shouldn't be so far down.
Forgive the authors of the article for assuming readers would complete it.
For any body of text (or in general, any exposition of any kind), the responsibility to explain the value of the article is very much in the author's side.
Explaining the value of what you are showing should always go towards the start. Else, why would anyone bother with the rest?
Re: Formalizing Fermat's Last Theorem
#133> 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.
[deleted]
Re: Formalizing Fermat's Last Theorem
#134> 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.
[deleted]
Re: Formalizing Fermat's Last Theorem
#135More (strong) evidence that agents make formal methods far more useful. The cost of creating that Lean proof has dropped dramatically.
Hopefully this helps mathematicians. It seems very clear to me that it will help software engineers apply formal methods to more of our software.
Re: Formalizing Fermat's Last Theorem
#136Holy 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 have been working on a streamlined new proof, but it's already many volumes long.
Re: Formalizing Fermat's Last Theorem
#137> 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.
There is no way Fermat could have fit that in the margin. Definitely vindicated.
While pretty much everyone is certain Fermat was mistaken in believing he had a valid proof for the theorem, this is an expanded (compared to proof presentations) version of one proof - not the shortest presentation of the shortest valid proof.
Re: Formalizing Fermat's Last Theorem
#13813M LoC, are we sure it didn't exploit any latent issues in the lean proof system?
Anthropic surely is well aware. Most likely they asked separate agents multiple times to code review the proof and look for exploits.
Re: Formalizing Fermat's Last Theorem
#139> 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.
But also achievable on a $150/mo (CAD) Max 5 subscription (I currently have 11.6B tokens in the last 30 days) according to /usage. It doesn’t break down input vs. output tokens as far as I can tell.
It's 6B output tokens, as stated by the blog post.
Re: Formalizing Fermat's Last Theorem
#14013M LoC, are we sure it didn't exploit any latent issues in the lean proof system?
Not just lean, but math foundation itself, I am not strong expert, but my understanding is that there is no fully recognized axiomatic foundation for modern math, all proposals could lead to some weird results.
ZFC is probably the biggest foundation, and only Choice is apparently controversial. The results aren't that weird, they're just different and occasionally more useful than using !Choice.