If they provide a working lean proof, it will be so much easier to review the work.
Still, it’s an important point to make. There is still the unverifiable bridge from statement of a theorem in lean to the interpretation of what that statement means. I’ve used LLMs to attempt to formalize pdfs, and a big challenge is making sure all of the assumptions listed before the statement of the main theorem mean what I think they mean.
If they provide a working lean proof, it will be so much easier to review the work.
Still, it’s an important point to make. There is still the unverifiable bridge from statement of a theorem in lean to the interpretation of what that statement means. I’ve used LLMs to attempt to formalize pdfs, and a big challenge is making sure all of the assumptions listed before the statement of the main theorem mean what I think they mean.
Yeah my impression is verifying human proof-to-Lean code translation faithfulness is pretty resistant to automation.