{"total":72,"rows":[{"id":"2502.07640","title":"Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving","created":"2025-02-11","cited_by_count":133,"area":null},{"id":"2510.01346","title":"Aristotle: IMO-level Automated Theorem Proving","created":"2025-10-01","cited_by_count":58,"area":null},{"id":"2512.17260","title":"Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience","created":"2025-12-19","cited_by_count":44,"area":null},{"id":"2506.21621","title":"The Open Proof Corpus: A Large-Scale Study of LLM-Generated Mathematical Proofs","created":"2025-06-23","cited_by_count":30,"area":null},{"id":"2511.02872","title":"FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levels","created":"2025-11-04","cited_by_count":27,"area":null},{"id":"2502.05567","title":"ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data","created":"2025-02-08","cited_by_count":23,"area":null},{"id":"2509.22908","title":"A benchmark for vericoding: formally verified program synthesis","created":"2025-09-26","cited_by_count":20,"area":null},{"id":"2506.07047","title":"Mathesis: Towards Formal Theorem Proving from Natural Languages","created":"2025-06-08","cited_by_count":18,"area":null},{"id":"2511.03108","title":"miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forward","created":"2025-11-05","cited_by_count":14,"area":null},{"id":"2509.26076","title":"IMProofBench: Benchmarking AI on Research-Level Mathematical Proof Generation","created":"2025-09-30","cited_by_count":13,"area":null},{"id":"2507.07399","title":"Generalized Tree Edit Distance (GTED): A Faithful Evaluation Metric for Statement Autoformalization","created":"2025-07-10","cited_by_count":12,"area":null},{"id":"2602.24173","title":"LemmaBench: A Live, Research-Level Benchmark to Evaluate LLM Capabilities in Mathematics","created":"2026-02-27","cited_by_count":10,"area":null},{"id":"2605.13171","title":"Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics","created":"2026-05-13","cited_by_count":10,"area":null},{"id":"2605.29955","title":"Formalizing Mathematics at Scale","created":"2026-05-28","cited_by_count":10,"area":null},{"id":"2510.10815","title":"DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems","created":"2025-10-12","cited_by_count":8,"area":null},{"id":"2510.15940","title":"Lean Finder: Semantic Search for Mathlib That Understands User Intents","created":"2025-10-08","cited_by_count":8,"area":null},{"id":"2602.18307","title":"VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Lean","created":"2026-02-20","cited_by_count":8,"area":null},{"id":"2603.02668","title":"SorryDB: Can AI Provers Complete Real-World Lean Theorems?","created":"2026-03-03","cited_by_count":8,"area":null},{"id":"2604.06802","title":"Riemann-Bench: A Benchmark for Moonshot Mathematics","created":"2026-04-08","cited_by_count":8,"area":null},{"id":"2510.06857","title":"Autoformalizer with Tool Feedback","created":"2025-10-08","cited_by_count":7,"area":null},{"id":"2603.12744","title":"TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib?","created":"2026-03-13","cited_by_count":6,"area":null},{"id":"2510.02335","title":"FormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theory","created":"2025-09-26","cited_by_count":5,"area":null},{"id":"2603.26996","title":"FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?","created":"2026-03-27","cited_by_count":5,"area":null},{"id":"2606.25363","title":"TheoremGraph: Bridging Formal and Informal Mathematics","created":"2026-06-24","cited_by_count":5,"area":null},{"id":"2502.15507","title":"Steering LLMs for Formal Theorem Proving","created":"2025-02-21","cited_by_count":4,"area":null},{"id":"2512.24796","title":"LeanCat: A Benchmark Suite for Formal Category Theory in Lean (Part I: 1-Categories)","created":"2025-12-31","cited_by_count":4,"area":null},{"id":"2601.18944","title":"Neural Theorem Proving for Verification Conditions: A Real-World Benchmark","created":"2026-01-26","cited_by_count":4,"area":null},{"id":"2604.06107","title":"Artificial Intelligence and the Structure of Mathematics","created":"2026-04-07","cited_by_count":4,"area":null},{"id":"2606.26525","title":"Theory-Scale Auto-Formalization of Logics for Computer Science","created":"2026-06-25","cited_by_count":4,"area":null},{"id":"2507.14722","title":"LeanTree: Accelerating White-Box Proof Search with Factorized States in Lean 4","created":"2025-07-19","cited_by_count":3,"area":null},{"id":"2507.21130","title":"INTEGRALBENCH: Benchmarking LLMs with Definite Integral Problems","created":"2025-07-22","cited_by_count":3,"area":null},{"id":"2601.15737","title":"PhysProver: Advancing Automatic Theorem Proving for Physics","created":"2026-01-22","cited_by_count":3,"area":null},{"id":"2605.10379","title":"Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness","created":"2026-05-11","cited_by_count":3,"area":null},{"id":"2505.04528","title":"Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving","created":"2025-05-07","cited_by_count":2,"area":null},{"id":"2509.24827","title":"Putnam-like dataset summary: LLMs as mathematical competition contestants","created":"2025-09-29","cited_by_count":2,"area":null},{"id":"2512.18256","title":"MSC-180: A Benchmark for Automated Formal Theorem Proving from Mathematical Subject Classification","created":"2025-12-20","cited_by_count":2,"area":null},{"id":"2606.03743","title":"Proof-Refactor: Refactoring Generated Formal Proofs into Modular Artifacts","created":"2026-06-02","cited_by_count":2,"area":null},{"id":"2502.04671","title":"ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving","created":"2025-02-07","cited_by_count":1,"area":null},{"id":"2507.04719","title":"Advocate for Complete Benchmarks for Formal Reasoning with Formal/Informal Statements and Formal/Informal Proofs","created":"2025-07-07","cited_by_count":1,"area":null},{"id":"2508.17200","title":"Large Language Model-Based Automatic Formulation for Stochastic Optimization Models","created":"2025-08-24","cited_by_count":1,"area":null},{"id":"2511.13043","title":"Spark-Prover-X1: Formal Theorem Proving Through Diverse Data Training","created":"2025-11-17","cited_by_count":1,"area":null},{"id":"2512.14252","title":"G\\\"odel's Poetry","created":"2025-12-16","cited_by_count":1,"area":null},{"id":"2601.15714","title":"Even GPT-5.2 Can't Count to Five: The Case for Zero-Error Horizons in Trustworthy LLMs","created":"2026-01-22","cited_by_count":1,"area":null},{"id":"2604.23698","title":"Benchmarking Testing in Automated Theorem Proving","created":"2026-04-26","cited_by_count":1,"area":null},{"id":"2606.09450","title":"TheoremBench: Evaluating LLMs on Theorem Proving in Formal Mathematics","created":"2026-06-08","cited_by_count":1,"area":null},{"id":"2606.13782","title":"MA-ProofBench: A Two-Tiered Evaluation of LLMs for Theorem Proving in Mathematical Analysis","created":"2026-06-11","cited_by_count":1,"area":null},{"id":"2607.07779","title":"From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier","created":"2026-07-08","cited_by_count":1,"area":null},{"id":"2608.28639","title":"Reward-Oracle MCTS for Formal Theorem Proving: Sample-Efficient Search and the Need for Kernel-Level Proof Auditing","created":"2026-08-11","cited_by_count":1,"area":null},{"id":"2609.05157","title":"AxQM: A Textbook-Scale Benchmark for Formal Proof Synthesis in a Library of Finite-Dimensional Quantum Mechanics","created":"2026-09-04","cited_by_count":1,"area":null},{"id":"2507.23776","title":"Cascaded Information Disclosure for Generalized Evaluation of Problem Solving Capabilities","created":"2025-07-31","cited_by_count":0,"area":null},{"id":"2510.11944","title":"TopoAlign: A Framework for Aligning Code to Math via Topological Decomposition","created":"2025-10-13","cited_by_count":0,"area":null},{"id":"2601.23048","title":"From Abstract to Contextual: What LLMs Still Cannot Do in Mathematics","created":"2026-01-30","cited_by_count":0,"area":null},{"id":"2605.14040","title":"Physics-R1: An Audited Olympiad Corpus and Released Verifiers for Visual Physics Reasoning","created":"2026-05-13","cited_by_count":0,"area":null},{"id":"2605.28512","title":"On Compositional Learning Behaviours in Formal Mathematics","created":"2026-05-27","cited_by_count":0,"area":null},{"id":"2606.01008","title":"FVSpec: Real-World Property-Based Tests as Lean Challenges","created":"2026-05-31","cited_by_count":0,"area":null},{"id":"2606.02588","title":"Lean-GAP: A Dataset of Formalized Graduate Algebra Problems","created":"2026-05-20","cited_by_count":0,"area":null},{"id":"2606.15258","title":"Mask-Proof: An LLM-based Automated Data Curation Pipeline on Mathematical Proofs","created":"2026-06-13","cited_by_count":0,"area":null},{"id":"2608.12762","title":"PROVE-RT: Generating Mechanized Theorem Prover Scripts for Real-Time Systems using LLMs","created":"2026-08-13","cited_by_count":0,"area":null},{"id":"2608.15979","title":"ALPS: Measuring Valid Creativity in Large Language Models with Mathematical Construction","created":"2026-08-17","cited_by_count":0,"area":null},{"id":"2608.18084","title":"Compiler-Guided Adaptive Proof Search with Cross-Model Synergy on Context-Dependent Theorem Proving","created":"2026-06-04","cited_by_count":0,"area":null},{"id":"2608.26334","title":"ProofEvolve: Neuro-Symbolic Evolution for Formal Automated Theorem Proving","created":"2026-08-26","cited_by_count":0,"area":null},{"id":"2609.09264","title":"StochBench: A Domain-Specific Benchmark for Stochastic Processes in Lean","created":"2026-09-08","cited_by_count":0,"area":null},{"id":"2609.10712","title":"An Open Recipe for IMO Gold: Training Nemotron for Olympiad Mathematics","created":"2026-09-09","cited_by_count":0,"area":null},{"id":"2609.34460","title":"When Does Structured Knowledge Help Neural Theorem Proving?","created":"2026-09-28","cited_by_count":0,"area":null},{"id":"2609.35606","title":"TCSAlgBench: Benchmarking Automated Proving for Research-Level Theoretical Computer Science","created":"2026-09-28","cited_by_count":0,"area":null},{"id":"2609.38384","title":"LeanPolish: Verified Supervision for Lean Proof Compression","created":"2026-09-29","cited_by_count":0,"area":null},{"id":"2609.39544","title":"Growing an Agent/Prover Interface: Evolutionary Tool Design for Cost-Efficient Theorem Proving in Rocq and Lean","created":"2026-09-30","cited_by_count":0,"area":null},{"id":"2610.11605","title":"NanoProof: Open and Efficient Automated Theorem Proving in Lean 4","created":"2026-10-08","cited_by_count":0,"area":null},{"id":"2610.13461","title":"SqueezeBench: Saturation-Resilient Evaluation of Mathematical Capability","created":"2026-10-09","cited_by_count":0,"area":null},{"id":"2610.17358","title":"claimcheck: Measuring and Improving Specification Faithfulness","created":"2026-10-12","cited_by_count":0,"area":null},{"id":"2610.17697","title":"LeanPRM: Lean-Grounded Process Supervision for Natural Language Proof Verification","created":"2026-10-13","cited_by_count":0,"area":null},{"id":"2610.18301","title":"A dataset of formalised theorem statements from the Annals of Mathematics","created":"2026-10-13","cited_by_count":0,"area":null}],"next_cursor":null}