It is beyond OWAR at this point, things never imagined before are habbening.
formalising is a more rigourous task than formalizing thoughbeit
>>17089355what is even the point of trying to “formalize” Wiles’ proof? Is it to make sure it is right even moreso than the fact that it is widely accepted and celebrated for decades in the math community?Even if there are still people who doubt Wiles’ proof then I can’t imagine having some AI-generated Lean formalization helps anybody to resolve their doubts. It’s already been well-understood that AI can’t faithfully translate accepted math proofs into Lean representations, so that is already a sticking point. But beyond that, and more importantly, I don’t think anybody in math actually gains any additional understanding of proofs, or basically anything, from having some Lean code put in front of them. That’s probably infinitely worse than just going and rereading Wiles and trying to explain it like a normal human mathematician in normal human math, instead of Lean which helps nobody
>>17089360I suppose the idea is that you learn something from a bunch of humans trying to formalize it.
>>17089360>It’s already been well-understood that AI can’t faithfully translate accepted math proofs into Lean representationsgee, perhaps this is why Anthropic demonstrated that AI can formalize about 30k theorems in 13 million lines of Lean code?
>>17089794gee, how does that respond to my post at all? how do we know those 13 million lines actually are faithful translations of the human math proofs? I can guarantee you there isn’t a team of mathematicians working through 13 million lines of useless AI slop codemore likely Anthropic asked Claude “are you totally sure this is AOK?” and claude was like “yeah. trust me bro” and Dario was like “werks4me, IPO here we come”
>>17089360The idea is to turn mathematics itself into an open source library that can be built from easily. Autoformalization does nothing to aid this goal. Having set FLT as the final objective was only ever there to serve as motivation since we know that much of mathematics must be formalized in order to reach that goal.
