AI Discovers Thousands of Theorems From Scratch, Boosting LLM Proofs
A new algorithm starts only with axioms and inference rules, then alternates proof search and theorem extraction to build its own library. In experiments it generated tens of thousands of novel theorems and solved benchmark problems, and feeding these lemmas into large language models improved their proof performance. This shows AI can create useful mathematical knowledge without human‑written resources.