Autoformalization is the step between a human-readable proof and a machine-checkable one. An AI writes the formal version, often millions of lines long, and a proof assistant verifies it.
In September 2026 Anthropic reported that Claude agents formalised Fermat’s Last Theorem in Lean in 11 days, about 13 million lines. The risk it introduces is misformalization: the formal statement may differ subtly from the question people meant to ask, so a passing check proves the wrong thing. The usual safeguard is to compare the statement against one humans have already reviewed and keep it short enough to read.