A self-supervised agent alternates proof search and theorem extraction in a formal system, discovers tens of thousands of theorems, solves human benchmarks, and boosts LLM proof performance when used as lemmas.
arXiv preprint arXiv:2507.02726 , year=
4 Pith papers cite this work. Polarity classification is still indexing.
4
Pith papers citing it
abstract
Reasoning remains a challenging task for large language models (LLMs), especially within the logically constrained environment of automated theorem proving (ATP), due to sparse rewards and the vast scale of proofs. These challenges are amplified in benchmarks like PutnamBench, which contains university-level problems requiring complex, multi-step reasoning. To address this, we introduce self-generated goal-conditioned MDPs (sG-MDPs), a new framework in which agents generate and pursue their subgoals based on the evolving proof state. Given this more structured generation of goals, the resulting problem becomes more amenable to search. We then apply Monte Carlo Tree Search (MCTS)-like algorithms to solve the sG-MDP, instantiating our approach in Bourbaki (7B), a modular system that can ensemble multiple 7B LLMs for subgoal generation and tactic synthesis. On PutnamBench, Bourbaki (7B) solves 26 problems, achieving new state-of-the-art results with models at this scale.
years
2026 4representative citing papers
OProver-32B achieves top Pass@32 scores on MiniF2F, ProverBench, and PutnamBench by combining continued pretraining with iterative agentic proving, retrieval, SFT on repairs, and RL on unresolved cases using a 6.86M-proof dataset.
A minimal agentic system achieves competitive performance in automated theorem proving with a simpler design and lower cost than state-of-the-art methods.
The paper introduces the 'topological dual of a dataset' — translating observable-logic sequents into covering-sieve statements on Grothendieck sites — as a new input representation for neuro-symbolic AI systems like AlphaGeometry.
citing papers explorer
-
Self-Supervised Theorem Discovery in a Formal Axiomatic System
A self-supervised agent alternates proof search and theorem extraction in a formal system, discovers tens of thousands of theorems, solves human benchmarks, and boosts LLM proof performance when used as lemmas.
-
OProver: A Unified Framework for Agentic Formal Theorem Proving
OProver-32B achieves top Pass@32 scores on MiniF2F, ProverBench, and PutnamBench by combining continued pretraining with iterative agentic proving, retrieval, SFT on repairs, and RL on unresolved cases using a 6.86M-proof dataset.
-
A Minimal Agent for Automated Theorem Proving
A minimal agentic system achieves competitive performance in automated theorem proving with a simpler design and lower cost than state-of-the-art methods.
-
The Topological Dual of a Dataset: A Logic-to-Topology Encoding for AlphaGeometry-Style Data
The paper introduces the 'topological dual of a dataset' — translating observable-logic sequents into covering-sieve statements on Grothendieck sites — as a new input representation for neuro-symbolic AI systems like AlphaGeometry.