Show HN: TheoremSmith: Mass-Producing Hard Proof Problems to Train LLMs

TheoremSmith is a pipeline for generating difficult Lean proof tasks to train language models in formal verification. The case for this work is that proofs are unusually easy to check mechanically, making them useful reinforcement-learning tasks, while better proof-writing could support both mathematical research and software correctness. The system starts from open-source Lean projects, maps their theorems and dependencies, and creates tasks by removing selected proofs while preserving the statements agents must prove. It then builds longer tasks by adding new theorems that depend on earlier results, aiming to train models to work across extended chains of reasoning rather than isolated exercises.

To guard against faulty tasks and reward hacking, the pipeline checks that original proofs pass and blank solutions fail, runs models on the tasks, and tests deliberate cheating attempts. Lean Comparator compiles solutions in a sandbox, checks that the submitted statements match the original challenge, validates proofs with Lean’s kernel, and rejects extra axioms. The system produced hundreds of tasks with horizons exceeding 30 minutes for leading models, but there is no evidence yet that training on them transfers to real-world proof work. Other concerns include math-heavy source projects, possible exposure to their proofs during model training, and imperfect automated checks. Future directions include measuring transfer, adapting the method to software-verification tools, and creating tasks for collaborative agent swarms.