Self-Supervised Theorem Discovery in a Formal Axiomatic System

The field of AI-driven mathematical reasoning has seen rapid growth, especially with large language models like GPT and Gemini achieving notable benchmark performance. However, these models often rely on extensive human-curated data, including theorem libraries and natural language descriptions, which limits their autonomy. Formal proof systems and proof assistants, such as Lean and Coq, have been developed to ensure correctness but still depend on human knowledge bases. Recent research explores the possibility of autonomous theorem discovery directly from axioms and inference rules, aiming to eliminate reliance on external data. This shift addresses fundamental questions about AI's capacity for self-guided mathematical exploration and the potential for fully automated proof generation, verification, and discovery, which could revolutionize mathematical research and formal verification.

The core challenge is whether an AI agent can independently discover meaningful theorems solely from primitive axioms and inference rules, without any human-curated theorem libraries or natural language input. Traditional methods depend heavily on pre-existing knowledge, limiting the scope of autonomous discovery. The key bottlenecks include the enormous search space, the complexity of proof search, and the difficulty of filtering valuable theorems from trivial or redundant results. Achieving efficient, scalable, and meaningful theorem discovery in a purely formal setting remains an open problem, crucial for advancing AI's role in mathematical innovation and automated reasoning.

This work introduces several key innovations: 1) a stack-machine formalization of propositional proof search, transforming proofs into sequential actions; 2) a self-supervised goal-conditioned policy learning framework that guides proof attempts based on discovered theorems; 3) a filtering mechanism based on generality and reprovability to select high-value theorems; 4) iterative expansion of the action space by incorporating discovered theorems as lemmas, enabling continuous growth of the theorem library. These innovations collectively allow the system to autonomously explore, filter, and reuse theorems, significantly reducing dependence on human knowledge and enhancing proof search efficiency.

• �� Formalize propositional proof search as a stack-machine decision process, with actions including axioms and inference rule applications. • Develop a goal-conditioned policy πθ that predicts the next action based on current proof state and target theorem. • Use self-discovered theorems as goals during training, updating the policy via supervised learning from proof prefixes. • Extract high-quality theorems based on generality (filtering out specialized ones) and reprovability (success rate estimation). • Expand the action space by adding theorem actions corresponding to selected theorems, enabling reuse as lemmas. • Conduct multi-generation proof searches, iteratively growing the theorem library and refining the policy. • Validate the approach through experiments on propositional logic, measuring theorem discovery, proof success, and transferability to LLMs.

The experiments involve running the proof search algorithm in the Hilbert propositional logic system over six generations. The initial action space includes three axioms and Modus Ponens. Each generation involves proof attempts, theorem extraction, filtering, and action space expansion. The performance is evaluated on 30 human-written benchmark problems, measuring proof success rate and theorem coverage. The discovered theorems are also tested as prompt lemmas to assess their transferability to LLM proof tasks. Hyperparameters include the number of proof attempts per generation, filtering thresholds, and theorem selection criteria. Ablation studies analyze the impact of filtering strategies and action space expansion on performance.

The results show a steady increase in the number of discovered theorems, reaching 38 after six generations. The theorem set covers 30% of benchmark problems, with proof success rates of about 30%. When used as prompt lemmas, the extracted theorems improve LLM proof success rates from around 10% to over 20%, demonstrating their external utility. The filtering mechanism effectively removes redundant theorems, ensuring high-quality knowledge accumulation. The approach outperforms baseline methods that lack theorem reuse, confirming the importance of iterative expansion and self-supervision in autonomous theorem discovery.

This framework can be applied to automated theorem proving, formal verification, and mathematical discovery systems. It enables AI agents to autonomously generate and verify mathematical results, reducing reliance on human-curated data. The approach can be integrated into proof assistants to enhance their autonomous reasoning capabilities. Long-term, it may facilitate the development of self-evolving AI systems capable of independently exploring complex mathematical domains, accelerating discovery and verification processes in academia and industry.

The current implementation is limited to propositional logic, and scaling to richer systems like first-order logic presents computational challenges. The proof search process is resource-intensive, especially as the theorem library grows. The mathematical significance of the discovered theorems remains to be validated beyond formal correctness, requiring further interpretability studies. Additionally, the approach's effectiveness in more complex mathematical domains needs exploration, along with strategies to improve scalability and efficiency.