Benchmark audits
1,347 statements across miniF2F, miniF2F v2 and ProofNet#, every flag verified by hand. 76 confirmed defects, all three filings public: miniF2F, v2, ProofNet#.
What we measure, and what we found
A formal statement can compile and still say the wrong thing.
Cross-system audits
Four open autoformalizers, same 488 problems, their own prompts. Failure rates ran from 21.7% to 55.5%. A compile check catches none of it.
Specification gaming
59 pairs satisfy the checker and two frontier judges yet fail human review. Three failure classes now have mechanical detectors.
Automated screens may only reject. Only a person certifies. Request a scored pilot