Machine learning methods discover a new noncrossing-partition statistic interpreting q,t-Narayana polynomials and yield a combinatorial proof of their symmetry.
hub Canonical reference
Aristotle: IMO-level Automated Theorem Proving
Canonical reference. 75% of citing Pith papers cite this work as background.
44
Pith papers citing it
1
external citations · Pith
Background
75% of classified citations
abstract
We introduce Aristotle, an AI system that combines formal verification with informal reasoning, achieving gold-medal-equivalent performance on the 2025 International Mathematical Olympiad problems. Aristotle integrates three main components: a Lean proof search system, an informal reasoning system that generates and formalizes lemmas, and a dedicated geometry solver. Our system demonstrates state-of-the-art performance with favorable scaling properties for automated theorem proving.
hub tools
citation-role summary
background 6
method 2
citation-polarity summary
representative citing papers
Lean-QEC delivers the first end-to-end Lean 4 formalization of stabilizer-code theory with verified distance certificates for large qLDPC codes in the Bivariate Bicycle family.
Any subset of the natural numbers that contains 1 can be realized as a product intersection set for any family of at least two subsets of a semigroup, and the paper gives the full classification for both arbitrary and decreasing families.
A deterministic O(n^6) algorithm for bipartite exact matching is obtained by proving the Affine-Slice Nonvanishing Theorem for all braces via induction on McCuaig's decomposition, with Lean 4 formalization.
AXLE is a multi-tenant cloud platform providing Lean 4 metaprogramming utilities with per-request isolation, multi-version support, and public access via SDK and API, having processed over 500 million requests.
Proves n_k > exp((log² k)/(20 log log k)) for large k, confirming Erdős conjecture on consecutive integers free of primes in (k,2k).
LeanMarathon uses four contract-scoped agents on an evolving blueprint coordinated by a two-stage orchestrator to formalize seven theorems from Erdős problems in Lean, proving 258 lemmas with no sorry across three runs.
A multi-agent framework called AutoformBot autoformalized 26 textbooks spanning analysis, algebra, topology, combinatorics and probability into a verified Lean 4 library of 45k declarations, demonstrating scalable formalization of graduate math.
Proof-state snapshotting in Lean 4 delivers 5.6-50x wall-time speedups (average 14x) on 48 miniF2F-v2 problems by reusing elaborated states and avoiding repeated import loading and theorem-body elaboration.
An LLM-based agent with Lean verification autonomously solved multiple open Erdős problems and OEIS conjectures in the first large-scale test.
CAM-Bench is a new Lean 4 theorem-proving benchmark of 1,000 problems in computational and applied mathematics, built from textbook exercises using a dependency-recovery pipeline to reconstruct local context.
Formal Conjectures is a Lean 4 benchmark containing 2615 formalized problems with 1029 open conjectures, designed to evaluate automated mathematical reasoning and proof discovery.
LeanSearch v2 recovers 46.1% of ground-truth premise groups for research-level Lean 4 theorems within 10 candidates and raises fixed-loop proof success to 20%.
An interactive AI workbench for mathematicians achieves 48% on FrontierMath Tier 4 and helped solve open problems in early tests.
Self-improvement of a decoder-only transformer yields plans averaging 30% shorter than a source symbolic planner, over 80% optimal where known, with sub-exponential latency scaling.
g(n) ≪_ε n^{ρ+ε} with ρ = (13 - √69)/10 < 0.47 for multiplicative Sidon sets that intersect every interval of length L up to n.
A SAT-plus-LLM method discovers infinite families of doubly saturated Ramsey-good graphs, answering Grinstead and Roberts' 1982 question.
A domain-independent analogy engine transfers Lean tactic patterns from probability to representation theory, producing four new machine-verified proofs.
LeetProof achieves higher rates of fully certified program synthesis from natural language by using a multi-modal verifier in Lean to validate specifications via randomized testing and delegate proofs to AI tools, outperforming single-mode baselines on benchmarks while uncovering defects in prior参考.
Rethlas+Archon automatically construct and Lean-verify a counterexample showing weak quasi-completeness does not imply quasi-completeness for Noetherian local rings.
Multi-agent AI system formalizes entire 500-page graduate algebraic combinatorics textbook into Lean, creating 130K lines of code in one week at human-expert cost.
SageMath-augmented ReAct agents raise solve rates by +9.7 pp on average on a curated 133-problem RealMath subset, with GPT-5.5 reaching 75.2%.
LLM formal provers must shift from competition solvers to research agents that handle open-ended, under-specified frontier mathematics under machine-checked rigor.
Theoria rewrites solutions into auditable typed state transitions with justifications, certifying 105 of 185 HLE problems at 91.4% precision and outperforming holistic judges on adversarial poisoned proofs by catching hidden premises.
citing papers explorer
-
Mapping Uncharted Symmetries: Machine Discovery in Combinatorics
Machine learning methods discover a new noncrossing-partition statistic interpreting q,t-Narayana polynomials and yield a combinatorial proof of their symmetry.
-
End-to-End Formalization of Quantum Error Correction
Lean-QEC delivers the first end-to-end Lean 4 formalization of stabilizer-code theory with verified distance certificates for large qLDPC codes in the Bivariate Bicycle family.
-
Global Product Intersection Sets in Semigroups
Any subset of the natural numbers that contains 1 can be realized as a product intersection set for any family of at least two subsets of a semigroup, and the paper gives the full classification for both arbitrary and decreasing families.
-
Bipartite Exact Matching in P
A deterministic O(n^6) algorithm for bipartite exact matching is obtained by proving the Affine-Slice Nonvanishing Theorem for all braces via induction on McCuaig's decomposition, with Lean 4 formalization.
-
AXLE: A Cloud Infrastructure for Lean 4 Theorem Proving Utilities
AXLE is a multi-tenant cloud platform providing Lean 4 metaprogramming utilities with per-request isolation, multi-version support, and public access via SDK and API, having processed over 500 million requests.
-
Consecutive integers free of certain prime factors
Proves n_k > exp((log² k)/(20 log log k)) for large k, confirming Erdős conjecture on consecutive integers free of primes in (k,2k).
-
LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization
LeanMarathon uses four contract-scoped agents on an evolving blueprint coordinated by a two-stage orchestrator to formalize seven theorems from Erdős problems in Lean, proving 258 lemmas with no sorry across three runs.
-
Formalizing Mathematics at Scale
A multi-agent framework called AutoformBot autoformalized 26 textbooks spanning analysis, algebra, topology, combinatorics and probability into a verified Lean 4 library of 45k declarations, demonstrating scalable formalization of graduate math.
-
Keep the Proof State Live: Snapshotting for Efficient Tactic Search in Lean 4
Proof-state snapshotting in Lean 4 delivers 5.6-50x wall-time speedups (average 14x) on 48 miniF2F-v2 problems by reusing elaborated states and avoiding repeated import loading and theorem-body elaboration.
-
Advancing Mathematics Research with AI-Driven Formal Proof Search
An LLM-based agent with Lean verification autonomously solved multiple open Erdős problems and OEIS conjectures in the first large-scale test.
-
CAM-Bench: A Benchmark for Computational and Applied Mathematics in Lean
CAM-Bench is a new Lean 4 theorem-proving benchmark of 1,000 problems in computational and applied mathematics, built from textbook exercises using a dependency-recovery pipeline to reconstruct local context.
-
Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics
Formal Conjectures is a Lean 4 benchmark containing 2615 formalized problems with 1029 open conjectures, designed to evaluate automated mathematical reasoning and proof discovery.
-
LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving
LeanSearch v2 recovers 46.1% of ground-truth premise groups for research-level Lean 4 theorems within 10 candidates and raises fixed-loop proof success to 20%.
-
AI co-mathematician: Accelerating mathematicians with agentic AI
An interactive AI workbench for mathematicians achieves 48% on FrontierMath Tier 4 and helped solve open problems in early tests.
-
Self-Improvement for Fast, High-Quality Plan Generation
Self-improvement of a decoder-only transformer yields plans averaging 30% shorter than a source symbolic planner, over 80% optimal where known, with sub-exponential latency scaling.
-
Gaps in Multiplicative Sidon Sets
g(n) ≪_ε n^{ρ+ε} with ρ = (13 - √69)/10 < 0.47 for multiplicative Sidon sets that intersect every interval of length L up to n.
-
Doubly Saturated Ramsey Graphs: A Case Study in Computer-Assisted Mathematical Discovery
A SAT-plus-LLM method discovers infinite families of doubly saturated Ramsey-good graphs, answering Grinstead and Roberts' 1982 question.
-
Yanasse: Finding New Proofs from Deep Vision's Analogies, Part 1
A domain-independent analogy engine transfers Lean tactic patterns from probability to representation theory, producing four new machine-verified proofs.
-
Certified Program Synthesis with a Multi-Modal Verifier
LeetProof achieves higher rates of fully certified program synthesis from natural language by using a multi-modal verifier in Lean to validate specifications via randomized testing and delegate proofs to AI tools, outperforming single-mode baselines on benchmarks while uncovering defects in prior参考.
-
Automated Conjecture Resolution with Formal Verification
Rethlas+Archon automatically construct and Lean-verify a counterexample showing weak quasi-completeness does not imply quasi-completeness for Noetherian local rings.
-
Automatic Textbook Formalization
Multi-agent AI system formalizes entire 500-page graduate algebraic combinatorics textbook into Lean, creating 130K lines of code in one week at human-expert cost.
-
Evaluating SageMath-Augmented LLM Agents for Computational and Experimental Mathematics
SageMath-augmented ReAct agents raise solve rates by +9.7 pp on average on a curated 133-problem RealMath subset, with GPT-5.5 reaching 75.2%.
-
From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier
LLM formal provers must shift from competition solvers to research agents that handle open-ended, under-specified frontier mathematics under machine-checked rigor.
-
Theoria: Rewrite-Acceptability Verification over Informal Reasoning States
Theoria rewrites solutions into auditable typed state transitions with justifications, certifying 105 of 185 HLE problems at 91.4% precision and outperforming holistic judges on adversarial poisoned proofs by catching hidden premises.
-
Gaps in Multiplicative Sidon Sets II
Multiplicative Sidon sets in [1,n] exist with maximal gap ≪_ε n^{10/33 + ε}.
-
Automating Formal Verification with Agent-Guided Tree Search
Agent-directed tree search improves LLM performance on Lean formal verification tasks, with context-based orchestration solving more intermediate specs at lower token cost than baseline agents.
-
Lean-GAP: A Dataset of Formalized Graduate Algebra Problems
Lean-GAP is a dataset of 430 graduate algebra problems formalized in Lean 4 from Dummit and Foote, with a described pipeline for autoformalization and verification plus analysis of challenges.
-
Teaching LLMs Program Semantics via Symbolic Execution Traces
Training Qwen3-8B on symbolic execution traces from Soteria improves violation detection in C programs by over 17 points, transfers across five property types, and shows superadditive gains with chain-of-thought.
-
The Network Structure of Mathlib
Network analysis of Mathlib reveals 50.9% coupling between human taxonomies and logical dependencies, median 1.6% import usage by developers, and centrality driven by infrastructure rather than mathematical content.
-
PROMISE: Proof Automation as Structural Imitation of Human Reasoning
PROMISE reframes automated proof generation as stateful search over structural embeddings of proof states, outperforming prior LLM-based systems by up to 26 points on the seL4 benchmark.
-
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.
-
Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics
Ax-Prover is a tool-using multi-agent LLM system that matches state-of-the-art provers on public math benchmarks and outperforms them on new abstract-algebra and quantum-theory benchmarks while also assisting an expert with a cryptography proof.
-
Artificial Intelligence for Mathematical Reasoning: An Integrated Survey of Language Models, Neuro-symbolic Systems, and Verified Discovery
AI for mathematics is best described as a supervision ladder — final answers, programs, process rewards, proof-assistant kernels — culminating in verified-discovery workflows.
-
Automating Formal Verification with Reinforcement Learning and Recursive Inference
RLVR training raises verified Dafny pass rates from 9.7% to 31.1% on a filtered benchmark while a Lean proof scaffold lifts success from 46.2% to 69.2% on a pilot set and solves 7 of 42 prior unsolved tasks.
-
Using Aristotle API for AI-Assisted Theorem Proving in Lean 4: A Formalisation Case Study of the Grasshopper Problem
Case study formalizes an AI-generated proof attempt for the Grasshopper problem in Lean 4, verifying four helper lemmas on maximality and adjacent swaps but leaving the main theorem unresolved due to missing global counting argument.
-
Beyond Benchmarks: MathArena as an Evaluation Platform for Mathematics with LLMs
MathArena is broadened into a maintained platform with new benchmarks for proofs, research questions, and formal verification, where GPT-5.5 scores 98% on 2026 USAMO and 74% on research-level tasks.
-
The cardinality of a set containing the pairwise sums of a fixed number of integers
Any subset A of {1,...,2n} with |A| at least n+1 or n+3 must contain the pairwise sums of three or four distinct integers respectively (both optimal), while |A| at least n plus 120 million guarantees it for five integers.
-
Astrolabe: A Content-Addressable Hypergraph for Semantic Knowledge Management
Astrolabe is a content-addressable hypergraph for semantic knowledge management using hash-identified entries, arbitrary-width ordered references, and plugin-extensible records.
-
Agentic Proving for Program Verification
Agentic Claude reaches 98.8% valid specs, 87.5% implementation certification, and 98.1% end-to-end success on CLEVER, revealing a mismatch between benchmark difficulty and current prover performance.
-
Toward Evaluation Frameworks for Multi-Agent Scientific AI Systems
This paper discusses challenges in evaluating multi-agent scientific AI systems and proposes strategies like contamination-resistant tasks and multi-turn testing, demonstrated via a novel research ideas dataset and quantum science interviews.
-
AI for Mathematics: Progress, Challenges, and Prospects
AI for math combines task-specific architectures and general foundation models to support research and advance AI reasoning capabilities.
- Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics
- Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search
- Deep Vision: A Formal Proof of Wolstenholmes Theorem in Lean 4