I wrote a similar DAG-based verifier as a skill a few months ago: https://github.com/sethlei/Warrant . The thing mine has that I didn't see in their's is a verification of the composition rules.
Mine also does more than just math.
Formalizing Fermat's Last Theorem
341–350 of 523 posts
Re: Formalizing Fermat's Last Theorem
#342Earlier quoted context omitted.
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.
There is, or rather are, fully recognized axiomatic foundations. You are free to choose one you like. Of the most popular ones is ZFC or ZF, but there are others (some lead to the same results some not). The main criteria for popularity is how useful it is. You can even make your own axiomatic where 2+2=5, but it would be useless. You probably heard about Goedel Incompleteness -- the proof that the the axiomatic itse…
Lean is based on Type Theory not ZFC.
Re: Formalizing Fermat's Last Theorem
#343I saw the 1996 FLT documentary in high school calculus class. For me, it forever cemented that archetype of modern math researcher at the top of my mental “smart” totem pole.
It also convinced me I had no interest in that path. Setting aside the grinding work of producing a proof that can only be reached by existing years in the abstract and hyper niche isolation of the problem space (not to mention that you might never discover it or that it DNE), the anguish of the output being a paper or presentation or some other artifact of human symbology (_words_, really) that could at any moment be refuted by a single observation of a single mistake—-that sounded like hell to me.
An equivalent high schooler today probably sees things differently, in light of this news and the undeniable implications of LLMs on mathematics. Sturdy autoformalization tooling should with time completely dispel the aforementioned anguish, once our confidence in converting a human proof to Lean/etc. reaches that of a compiler translating Java application language to bytecode. Errata may always exist, but in practice these new methods will do wonders for rigor and peace of mind.
(I’m far less confident re novel discoveries. There’s too much chance of derivative findings based on something part of the training looking like genius but really just tiptoeing on the shoulders of humans, whereas autoformalization is absolutely convincing to me as transformative, particularly to check correctness of AI outputted proofs as mentioned in the post.)
Re: Formalizing Fermat's Last Theorem
#344> 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.
Maybe we need "de Moura complexity": the shortest Lean proof of a theorem.
Re: Formalizing Fermat's Last Theorem
#345I'd feel so much more excited if this was done in Metamath. Tiny checker kernel, no complicated dependent types, way less to go wrong.
Not mm0?
Re: Formalizing Fermat's Last Theorem
#346Earlier quoted context omitted.
I did an undergrad in math with a little research in number theory and recognized parts — eg, I myself worked through the proof for odd regular primes and that 37 is irregular, breaking the general case. Wiles-Taylor-Wiles was the original proof by Andrew Wiles, and its corrections. Galois representations is about vectors over Galois extensions, which are essentially adding roots to regular numbers (rationals, intege…
About the Langlands program, Nunberphile has an excellent episode with Edward Frenkel explaining what it's about: https://youtu.be/4dyytPboqvE .
Frenkel does a nice job explaining the Langlands program in general. But Buzzard's complaint about Langlands, I believe, refers specifically to the proof of a version of the Geometric Langlands Conjecture by Gaitsgory et al. The proo f is of order thousand pages of mathematical text and builds off of thousands of pages of higher-categorical algebraic geometry by Lurie & others. It's a ripe target for formalization because it's terrifically complicated, not well understood or thoroughly digested yet, and relatively important. A formal proof would be reassuring to mathematicians, whereas Fermat's Last Theorem is relatively unique in that so many mathematicians have examined the proof that it's not very likely to be wrong.
Re: Formalizing Fermat's Last Theorem
#347Earlier quoted context omitted.
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?
Feel very grateful I was never taught this... Would have missed out on quite a lot of good bodies of text in my life I think! Pushing through any initial friction or ignorance I might have as a reader, having the patience and charity to bear with an author until you get it, was instead what I was always taught. Giving such a blanket "responsibility" to the author at all is just such a bummer! I say let them do whatev…
> Feel very grateful I was never taught this...
Never heard of Abstract section? First semester on a college or last year on high school.
Re: Formalizing Fermat's Last Theorem
#348Earlier quoted context omitted.
Isn't it the cost we care about, rather than the speed? All we know know is that a frontier AI lab was able to do it in 11 days, we have no idea how much compute they threw at it.
They said 6 billion tokens, which isn't as much as I thought it might be.
Am I doing my napkin math correct? The post says it's using a model comparable to Fable 5.1, which is $50 per million output tokens. So this is ~$300K? Surely an over-estimate due to caching.
Re: Formalizing Fermat's Last Theorem
#349I think Anthropic might the frontier lab hiring contractors through data vendors to formalize mathematical textbooks for them at a rate of 170-200 dollars per hour. This was mainly through Alignerr which has the worst reputation for not paying their contractors. They have been hiring since February as far as I can recall. This is in addition to all the internal people they might have working on this. If they have been formalizing all this work for the past 9 months before having Claude use all this data needed to formalize FLT, then it wouldn't be Claude formalizing FLT in just 11 days. Same with the upcoming results they will claim Claude came up with, but in fact they have been hiring frontier researchers working on very niche topics through Micro1. It's all a marketing ploy before their IPO.
Re: Formalizing Fermat's Last Theorem
#350So I don't know Lean or Mathematics to any degree to really be able to say this with any level of confidence, but speaking from a pure software engineering backgrouand, how do we know that 13 MILLION lines of Lean code are bug-free? It seems to me that for a mathematical proof, bug-free would be an absolute requirement. Maybe the structure of Lean imposes that, I don't know, but that seems highly unlikely to me. That just feels like a LOT of code to be comletely error-free... What am I missing here?