Provides great context on this accomplishment and what it means but also doesn't mean.
Gives you an idea of the scale...
I've tried the various intros to Lean multiple times (even before Lean 4 came out) and something about the way Lean proofs are written does not align with how I think about proofs. My very brief attempts at Isabelle / RCoq feel more natural.
I think it's a pity that the future of proofs is Lean. I'd love for someone to come up with a more digestable proof language!
Lean is not for humans.
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.
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 aging.
The future is both beautiful and terrifying.
status: "self-assessed"
Fable, please translate to HOL-light. Make no mistakes. You are doing great!
^ this section should have been in the first few paragraphs imho. Explaining why this is relevant shouldn't be so far down.
Not sure why anyone is excited about this tech.
I hope soon enough we will have one of the big ones proved by AI!
Can not we do it by code?
kdavis•34m ago
[1] https://github.com/ImperialCollegeLondon/FLT
arjie•18m ago
> We shared the resulting proof with Kevin Buzzard, who said:
> > This extraordinary autoformalization achievement, which Anthropic researchers say only took 11 days, proves Fermat’s Last Theorem with no assumptions other than the axioms of mathematics. Along the way we see autoformalization of algebra, harmonic analysis, geometry and number theory, and we learn that AI autoformalization artefacts are now robust enough to be built upon; the proof is multi-layered.