Charles Huang introduces TheoremSmith for mass-producing hard proof problems to train LLMs
Charles Huang introduces TheoremSmith, a pipeline for generating synthetic formal verification environments. The tool reliably creates multi-hour, frontier-difficulty tasks and can scale throughput effectively. Math research has recently seen AI-assisted breakthroughs, with 10,000 agents deriving a possible solution to the Navier–Stokes problem and a formalization of Fermat’s Last Theorem in September. Software outages have increased 50% in the past two years, and AI code generation has played a large part in this. Industry QA and testing standards cannot keep up with the rise of agentic coding. Formal verification allows mathematically proving the correctness of a program, significantly reducing the number of bugs in code. The economics of formal methods have flipped with AI, now costing about $0.10 per line of code, making them viable for mainstream use. TheoremSmith addresses two halves of formal verification: defining a specification and proving said specification. The tool generates mathematical statements that can be verified more easily than natural language translation. Limitations include the difficulty of making specifications faithful to original intent and the challenge of verifying whether a spec matches user intent. Future work aims to improve the pipeline's ability to generate verifiable domains and scale synthesis.
About TheoremSmith: Software Engineering @ University of Waterloo. More at charleshuang.me.
