Self-Supervised Theorem Discovery in a Formal Axiomatic System

• URL: http://arxiv.org/abs/2606.28747v1
• Date: Sat, 27 Jun 2026 05:55:18 GMT
• Title: Self-Supervised Theorem Discovery in a Formal Axiomatic System
• Abstract summary: We study whether an agent can autonomously discover useful theorems without such human priors.<n>We propose a self-supervised theorem-discovery algorithm that alternates between proof search and useful-theorem extraction.<n>Our results provide evidence that useful theorems can emerge from proof search without relying on human-provided theorem libraries.
• Score: 44.603295025494674
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Recent artificial intelligence (AI) systems have shown remarkable progress in mathematical reasoning. Many existing approaches, including large language models (LLMs), draw on human prior knowledge in the form of mathematical text, code, or theorem libraries. Although these approaches are highly effective in practice, it remains an open question whether an agent can autonomously discover useful theorems without such human priors. We study this question in a formal axiomatic system by developing an agent that starts from axioms and inference rules alone and gradually grows a library of useful theorems. Concretely, we propose a self-supervised theorem-discovery algorithm that alternates between proof search and useful-theorem extraction, building a theorem library whose entries are reused as lemmas for subsequent proof search. Experiments show that the agent discovers tens of thousands of theorems and finds proofs for human-written benchmark problems, suggesting that its discoveries include theorems meaningful from a human mathematical perspective. Furthermore, the discovered theorems improve LLM proof performance when provided as prompt lemmas, indicating that they can serve as external knowledge for LLM reasoning. Our results provide evidence that useful theorems can emerge from proof search without relying on human-provided theorem libraries. More broadly, they suggest a path toward self-evolving AI systems for mathematics whose discoveries remain formally verifiable.

Related papers

• MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Research [62.221184989046826]
  MathCoPilot is a human-in-the-loop system that embodies a new human--AI symbiotic paradigm for mathematical research.<n>MathCoPilot unifies three core capabilities: an interactive proof blueprint that decomposes a proof into navigable steps the human can directly inspect, direct, and refine; automated proving skill orchestration with adaptive knowledge base search and Lean-integrated iterative verification; and topic-driven paper retrieval and automated formalization into a verified Lean knowledge base.
  arXiv  Detail & Related papers  (2026-07-16T05:22:40Z)
• From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier [109.93387172162984]
  We argue that the next leap in AI4Math systems requires a decisive shift from predefined problem-solvers to research agents.<n>We provide a systematic review of the field, covering datasets, auto-formalization, and proof synthesis.
  arXiv  Detail & Related papers  (2026-07-08T17:46:36Z)
• Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics [20.90238876313568]
  Large Language Models (LLMs) produce subtle errors that evade human detection.<n>Recent trends indicate that general-purpose LLMs now outperform smaller models explicitly fine-tuned for Lean.<n>We introduce an agentic autoformalization framework powered by general coding LLMs.
  arXiv  Detail & Related papers  (2026-06-30T05:05:03Z)
• A Theoretical Framework for Self-Play Theorem Proving Algorithms [7.702779307300836]
  We provide a theoretical framework for understanding the self-improvement capabilities of self-play algorithms for theorem proving.<n>We show that if the underlying graph of theorems is well-connected, then a prover-conjecturer system, where the conjecturing algorithm is based on a reversible random walk, is sufficient to grow the set of proved theorems exponentially.
  arXiv  Detail & Related papers  (2026-06-01T08:12:47Z)
• Discovering New Theorems via LLMs with In-Context Proof Learning in Lean [6.097030695272925]
  We propose Conjecturing-Proving Loop pipeline for automatically generating mathematical conjectures and proving them in Lean 4 format.<n>A feature of our approach is that we generate and prove further conjectures with context including previously generated theorems and their proofs.<n>At least one of these theorems could not be proved by the LLM without in-context learning, even in natural language.
  arXiv  Detail & Related papers  (2025-09-16T06:48:11Z)
• DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning [67.93945726549289]
  DeepTheorem is a comprehensive informal theorem-proving framework exploiting natural language to enhance mathematical reasoning.<n>DeepTheorem includes a large-scale benchmark dataset consisting of 121K high-quality IMO-level informal theorems and proofs.<n>We devise a novel reinforcement learning strategy (RL-Zero) explicitly tailored to informal theorem proving, leveraging the verified theorem variants to incentivize robust mathematical inference.
  arXiv  Detail & Related papers  (2025-05-29T17:59:39Z)
• LeanAgent: Lifelong Learning for Formal Theorem Proving [85.39415834798385]
  We present LeanAgent, a novel lifelong learning framework for formal theorem proving.<n>LeanAgent continuously generalizes to and improves on ever-expanding mathematical knowledge.<n>It generates formal proofs for 155 theorems across 23 diverse Lean repositories.
  arXiv  Detail & Related papers  (2024-10-08T17:11:24Z)
• ATG: Benchmarking Automated Theorem Generation for Generative Language Models [83.93978859348313]
  Humans can develop new theorems to explore broader and more complex mathematical results. Current generative language models (LMs) have achieved significant improvement in automatically proving theorems. This paper proposes an Automated Theorem Generation benchmark that evaluates whether an agent can automatically generate valuable (and possibly brand new) theorems.
  arXiv  Detail & Related papers  (2024-05-05T02:06:37Z)
• Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
  We learn a neural generator that automatically synthesizes theorems and proofs for the purpose of training a theorem prover. Experiments on real-world tasks demonstrate that synthetic data from our approach improves the theorem prover.
  arXiv  Detail & Related papers  (2020-02-17T16:06:02Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.