NanoProof: Open and Efficient Automated Theorem Proving in Lean 4
cs.LG, cs.AI
Submitted: 2026-10-08
Updated: 2026-10-08
Code: https://github.com/kripner/nanoproof
Sources
- Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4
- The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale
- Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving
- Stop Regressing: Training Value Functions via Classification for Scalable Deep RL
- The Formal Proof of the Kepler Conjecture: a critical retrospective
- Proof Artifact Co-training for Theorem Proving with Language Models
- LeanReasoner: Boosting Complex Logical Reasoning with Lean
- LeanTree: Accelerating White-Box Proof Search with Factorized States in Lean 4
- Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction
- Nemotron-CC-Math: A 133 Billion-Token-Scale High Quality Math Pretraining Dataset
- Generative Language Modeling for Automated Theorem Proving
- DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition
- Formalization of physics index notation in Lean 4
- PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition
- Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning
- Holophrasm: a neural Automated Theorem Prover for higher-order logic
- InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Search
- LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover
- DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data
- Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Provers
Related papers
- Polynomial-Augmented Neural Networks (PANNs) with Weak Orthogonality Constraints for Enhanced Function and PDE Approximation
- AIRL-S: Unifying Reinforcement Learning and Search-Based Test-Time Scaling via Adversarial Inverse Reinforcement Learning
- Transformers as Bayesian In-Context Experimenters: Smoothness-Adaptive Efficient ATE Estimation
- Convergence issues in Relational Concept Analysis based on AOC-posets
- Beliefs Beyond Posteriors: The Predictive Cost of ELBO Binding
- Understanding Diffusion Models via Ratio-Based Function Approximation with SignReLU Networks