A new AI harness doesn't just write formal math proofs - it checks whether the formal version secretly changed what the original theorem claimed.
FYAN is a human-AI harness for turning math proofs into Lean, a language that checks proofs line by line. Instead of handling one theorem at a time, it runs a full pipeline: write a formal specification, plan the proof, review the logic, build the Lean proof, and validate the result, with people able to step in at any stage. Its key addition is a "semantic audit": an AI model lays out evidence of where the formal statement matches, omits, or shifts scope from the original wording, and a separate deterministic checker turns that evidence into a reproducible verdict. Using the same model, DeepSeek-V4.1-Flash, at every stage, FYAN proved 86 of 143 theorems from a benchmark called FormalTCS under a strict Lean check, versus 69 for a generic AI agent doing the same job, and raised a natural-language proof-quality score from 0.501 to 0.851.
The real failure mode in AI-assisted formalization isn't proofs that fail to compile - it's proofs that compile perfectly while quietly proving something easier or different than the original claim. On a test built to catch exactly that, called ConsistencyCheck, FYAN's semantic audit flagged 77.7% of inconsistent statements verified against the source, versus 63.6% for a model simply asked to judge the statements directly, and it pointed to the specific hypothesis, conclusion, or scope where the drift happened rather than issuing a vague thumbs-down.
As a side effect, the project also produced ODENumLib, a 9,355-line Lean library for the numerical analysis of ordinary differential equations - a useful resource on its own, and a reminder that the hard part of "AI does math" is no longer getting a proof to compile, it's trusting that it proved what you actually asked.