Update
Meta and NYU’s h1 system beats elaborate theorem-proving workflows at lower cost
Researchers at Meta and New York University have developed a simplified AI system called h1 for proving mathematical theorems. h1 matched or outperformed carefully engineered Lean proof workflows but did so at a lower cost. The system scored 670 out of 672 on the PutnamBench benchmark using GPT-5.5 and resolved eight open problems in the FormalConjectures collection, including variants of Erdős problems. h1 spent $121 per successful proof, compared to $317 for AlphaProof Nexus.