Typechecked and Still Wrong
TL;DR for operators The useful lesson from this paper is not “AI can formalize mathematics better.” That is the shiny wrapper. The operational lesson is nastier and more important: an AI-generated formal artifact can pass syntactic checks, be provable, and still fail to represent the original human intent. The type checker is not a mind reader. It is a very disciplined bureaucrat. ...