REVIEW 24 cited by
ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
read the original abstract
We introduce ProofNet, a benchmark for autoformalization and formal proving of undergraduate-level mathematics. The ProofNet benchmarks consists of 371 examples, each consisting of a formal theorem statement in Lean 3, a natural language theorem statement, and a natural language proof. The problems are primarily drawn from popular undergraduate pure mathematics textbooks and cover topics such as real and complex analysis, linear algebra, abstract algebra, and topology. We intend for ProofNet to be a challenging benchmark that will drive progress in autoformalization and automatic theorem proving. We report baseline results on statement autoformalization via in-context learning. Moreover, we introduce two novel statement autoformalization methods: prompt retrieval and distilled backtranslation.
Forward citations
Cited by 24 Pith papers
-
ShannonProver: Towards Automating Formal Cryptographic Proofs
Given expert lemma decompositions, ShannonProver’s proof-state compiler and multi-agent tree search automate EasyCrypt tactic scripts for substantial fractions of real cryptographic developments including ChaCha20-Pol...
-
TLA+-Bench: An Execution-Grounded Benchmark and Dataset for Natural-Language to TLA Specification Generation
An exact model-checker oracle for NL-to-TLA+ still yields an elevenfold “correctness envelope” (18.7%–1.7%) once interface supply and vacuity screens are made explicit.
-
CausalForge: A Formally Grounded, Self-Improving Agentic Framework for Automated Research in Causal Inference
CausalForge is a Lean-grounded, self-improving agentic framework that proposes, proves, and statement-audits causal inference theorems; its runs produced nine accepted results including a new ATE minimax upper bound.
-
AoA: Theorem Proving Agent over Abstract Syntax Tree of Redesigned Language
AoA proves theorems by editing a JSON-AST proof tree for the new Minilang language, reporting 2.9–6.9x fewer tokens and 2.3–4.7x lower API cost than Amazon's Isabelle agent with equal or better pass rates.
-
FormalRx: Rectify and eXamine Semantic Failures in Autoformalization
FormalRx diagnoses Lean autoformalization failures with a 28-category SCI taxonomy and an 8B model that jointly predicts alignment, error type, location, and correction.
-
HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement
A dual-model framework that extracts proof sketches from whole-proof candidates and refines them with a tactic model and Sledgehammer, reaching 59.4 percent on miniF2F in Isabelle.
-
CircuitProver: Agentic Lean 4 Theorem Proving with Reusable Circuit Proof Library for Hardware Verification
CircuitProver is an agentic Lean 4 framework that automatically proves parameterized hardware designs correct against formalized specifications and reuses proof knowledge across tasks.
-
Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graph
A graph-of-thought agent with retrieval and a term-grounded semantic checker auto-formalizes research-level math statements in Lean, hitting 68.5% on ProofNet and 6/14 homological conjectures where baselines score 0.
-
FormaRL: Enhancing Autoformalization with no Labeled Data
A reinforcement learning framework improves autoformalization without labeled data by rewarding outputs that pass Lean syntax and LLM consistency checks.
-
LeanTree: Accelerating White-Box Proof Search with Factorized States in Lean 4
White-box proof search with factorized Lean 4 goals reaches 18.4% on MiniF2F with Llemma-7B, outperforming black-box generation at 9.6%.
-
Generalized Tree Edit Distance (GTED): A Faithful Evaluation Metric for Statement Autoformalization
GTED uses tree edit distance on operator trees of standardized Lean statements to evaluate autoformalization, ranking top on miniF2F and joint-top on ProofNet.
-
CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization
A critic model trained with reinforcement learning judges semantic correctness of Lean 4 formalizations, and using it as a filter sharply improves autoformalization accuracy.
-
Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models
An inference-only neuro-symbolic pipeline, DSP+, solves 80.7% of miniF2F and the previously unsolved imo_2019_p1, matching heavily RL-trained theorem provers without fine-tuning.
-
Mathesis: Towards Formal Theorem Proving from Natural Languages
An RL-trained autoformalizer plus a Lean prover solves 18% of Chinese Gaokao proof problems end-to-end from natural language, and 64.3% of MiniF2F at pass@32.
-
MATP-BENCH: Can MLLM Be a Good Automated Theorem Prover for Multimodal Problems?
MATP-BENCH pairs 1,056 multimodal math problems with formal theorem statements in Lean 4, Coq, and Isabelle; the strongest tested model solves only 5.68% of Lean 4 end-to-end proving tasks at pass@10.
-
Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases
Autoformalization should target complete theories—axioms, definitions, lemmas, proofs—as unified formal libraries, not isolated statements.
-
OpenProver: Agentic and Interactive Theorem Proving with Lean 4
OpenProver is an open-source Planner-Worker-Verifier ATP system with Lean 4 that raises ProofNet success rates over linear LLM rollouts and adds interactive human guidance.
-
LeanFlow: A Case Study in Workflow-Driven Lean Autoformalization
Workflow control and a cached Lean verifier improve completion and token efficiency in document-to-project autoformalization.
-
Artificial Intelligence for Mathematical Reasoning: An Integrated Survey of Language Models, Neuro-symbolic Systems, and Verified Discovery
An integrated survey organizing AI mathematical reasoning into informal, formal, discovery, and technique axes while cataloging benchmarks and assessing failure modes.
-
Integrating Rules and Semantics for LLM-Based C-to-Rust Translation
IRENE combines rule-based retrieval, structured summarization, and compiler feedback to improve LLM-based C-to-Rust translation accuracy and safety.
-
Leanabell-Prover-V2: Verifier-integrated Reasoning for Formal Theorem Proving via Reinforcement Learning
Verifier-integrated reinforcement learning with multi-turn reflection improves 7B-scale Lean 4 theorem proving by 2 to 3 points on MiniF2F at pass@128.
-
Step-Wise Formal Verification for LLM-Based Mathematical Problem Solving
MATH-VF formalizes LLM math solutions into SimpleMath and uses a tool-augmented critic to verify each reasoning step and offer corrective feedback.
-
Formally Solving Answer-Construction Problems in Lean
ECP, an enumerate-conjecture-prove framework with Lean verification, improves answer-construction accuracy on ConstructiveBench and a PutnamBench subset, but its benchmark has a 17% major-error rate and its abstract r...
-
Towards Concise and Adaptive Thinking in Large Reasoning Models: A Survey
A comprehensive review that categorizes methods for shortening and adaptively triggering chain-of-thought reasoning in large language models.
Discussion (0). Sign in to comment.