formalising is a more rigourous task than formalizing thoughbeit

>>17089355
what 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

>>17089360
I 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 representations
gee, perhaps this is why Anthropic demonstrated that AI can formalize about 30k theorems in 13 million lines of Lean code?

>>17089794
gee, 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 code

more 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”