{"total":133,"rows":[{"id":"2504.21801","title":"DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition","created":"2025-04-30","cited_by_count":287,"area":"lr"},{"id":"2504.11354","title":"Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning","created":"2025-04-15","cited_by_count":180,"area":"lr"},{"id":"2508.03613","title":"Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction","created":"2025-08-05","cited_by_count":154,"area":"synth"},{"id":"2507.15061","title":"WebShaper: Agentically Data Synthesizing via Information-Seeking Formalization","created":"2025-07-20","cited_by_count":121,"area":null},{"id":"2507.23726","title":"Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving","created":"2025-07-31","cited_by_count":101,"area":"lr"},{"id":"2510.02387","title":"CWM: An Open-Weights LLM for Research on Code Generation with World Models","created":"2025-09-30","cited_by_count":93,"area":"wm"},{"id":"2506.02355","title":"Rewarding the Unlikely: Lifting GRPO Beyond Distribution Sharpening","created":"2025-06-03","cited_by_count":80,"area":"lr"},{"id":"2509.22819","title":"Hilbert: Recursively Building Formal Proofs with Informal Reasoning","created":"2025-09-26","cited_by_count":60,"area":"lr"},{"id":"2510.01346","title":"Aristotle: IMO-level Automated Theorem Proving","created":"2025-10-01","cited_by_count":58,"area":null},{"id":"2505.02735","title":"FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models","created":"2025-05-05","cited_by_count":48,"area":"lr"},{"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":"2507.15225","title":"Solving Formal Math Problems by Decomposition and Iterative Reflection","created":"2025-07-21","cited_by_count":35,"area":"lr"},{"id":"2505.03171","title":"CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics","created":"2025-05-06","cited_by_count":31,"area":"lr"},{"id":"2506.19923","title":"Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs","created":"2025-06-24","cited_by_count":31,"area":"agents"},{"id":"2510.12787","title":"Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics","created":"2025-10-14","cited_by_count":31,"area":"lr"},{"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":"2505.13938","title":"CLEVER: A Curated Benchmark for Formally Verified Code Generation","created":"2025-05-20","cited_by_count":29,"area":null},{"id":"2509.06493","title":"Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Provers","created":"2025-09-08","cited_by_count":28,"area":"lr"},{"id":"2504.06122","title":"Leanabell-Prover: Posttraining Scaling in Formal Reasoning","created":"2025-04-08","cited_by_count":27,"area":"lr"},{"id":"2507.08649","title":"Leanabell-Prover-V2: Verifier-integrated Reasoning for Formal Theorem Proving via Reinforcement Learning","created":"2025-07-11","cited_by_count":27,"area":"lr"},{"id":"2602.05665","title":"Graph-based Agent Memory: Taxonomy, Techniques, and Applications","created":"2026-02-05","cited_by_count":25,"area":"agents"},{"id":"2503.03205","title":"MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving","created":"2025-03-05","cited_by_count":24,"area":"lr"},{"id":"2505.23486","title":"Autoformalization in the Era of Large Language Models: A Survey","created":"2025-05-29","cited_by_count":21,"area":null},{"id":"2506.07927","title":"Solving Inequality Proofs with Large Language Models","created":"2025-06-09","cited_by_count":21,"area":"lr"},{"id":"2602.06176","title":"Large Language Model Reasoning Failures","created":"2026-02-05","cited_by_count":21,"area":"lr"},{"id":"2510.24592","title":"ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization","created":"2025-10-28","cited_by_count":20,"area":"lr"},{"id":"2505.20613","title":"REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning","created":"2025-05-27","cited_by_count":18,"area":"lr"},{"id":"2506.07047","title":"Mathesis: Towards Formal Theorem Proving from Natural Languages","created":"2025-06-08","cited_by_count":18,"area":null},{"id":"2510.15681","title":"ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings","created":"2025-10-17","cited_by_count":18,"area":"rag"},{"id":"2602.24273","title":"A Minimal Agent for Automated Theorem Proving","created":"2026-02-27","cited_by_count":18,"area":"agents"},{"id":"2502.13834","title":"Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning","created":"2025-02-19","cited_by_count":17,"area":"lr"},{"id":"2506.11487","title":"Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models","created":"2025-06-13","cited_by_count":17,"area":"lr"},{"id":"2605.08678","title":"MLS-Bench: A Holistic and Rigorous Assessment of AI Systems on Building Better AI","created":"2026-05-09","cited_by_count":17,"area":null},{"id":"2507.06181","title":"CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization","created":"2025-07-08","cited_by_count":16,"area":"lr"},{"id":"2508.04440","title":"StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion","created":"2025-08-06","cited_by_count":16,"area":"lr"},{"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":"2506.06034","title":"MATP-BENCH: Can MLLM Be a Good Automated Theorem Prover for Multimodal Problems?","created":"2025-06-06","cited_by_count":13,"area":"mllm"},{"id":"2507.13966","title":"Bottom-up Domain-specific Superintelligence: A Reliable Knowledge Graph is What We Need","created":"2025-07-18","cited_by_count":13,"area":"lr"},{"id":"2507.20199","title":"StepFun-Prover Preview: Let's Think and Verify Step by Step","created":"2025-07-27","cited_by_count":13,"area":"lr"},{"id":"2507.02726","title":"Bourbaki: Self-Generated and Goal-Conditioned MDPs for Theorem Proving","created":"2025-07-03","cited_by_count":12,"area":"synth"},{"id":"2509.17677","title":"EngiBench: A Benchmark for Evaluating Large Language Models on Engineering Problem Solving","created":"2025-09-22","cited_by_count":12,"area":"lr"},{"id":"2505.23703","title":"Let's Reason Formally: Natural-Formal Hybrid Reasoning Enhances LLM's Math Capability","created":"2025-05-29","cited_by_count":11,"area":"lr"},{"id":"2511.08522","title":"AlphaResearch: Accelerating New Algorithm Discovery with Language Models","created":"2025-11-11","cited_by_count":11,"area":"agents"},{"id":"2505.10962","title":"MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation","created":"2025-05-16","cited_by_count":10,"area":null},{"id":"2604.20209","title":"Scaling Self-Play with Self-Guidance","created":"2026-04-22","cited_by_count":10,"area":"synth"},{"id":"2605.29955","title":"Formalizing Mathematics at Scale","created":"2026-05-28","cited_by_count":10,"area":null},{"id":"2602.16793","title":"Escaping the Cognitive Well: Efficient Competition Math with Off-the-Shelf Models","created":"2026-02-18","cited_by_count":9,"area":"lr"},{"id":"2606.06468","title":"Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement","created":"2026-06-04","cited_by_count":9,"area":"agents"},{"id":"2608.05179","title":"Autonomous Research Agents: A Survey of AI Scientists and the Verification Gap","created":"2026-06-29","cited_by_count":9,"area":"agents"},{"id":"2505.12680","title":"Ineq-Comp: Benchmarking Human-Intuitive Compositional Reasoning in Automated Theorem Proving on Inequalities","created":"2025-05-19","cited_by_count":8,"area":"lr"},{"id":"2506.17104","title":"Towards Advanced Mathematical Reasoning for LLMs via First-Order Logic Theorem Proving","created":"2025-06-20","cited_by_count":8,"area":"lr"},{"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":"2603.02668","title":"SorryDB: Can AI Provers Complete Real-World Lean Theorems?","created":"2026-03-03","cited_by_count":8,"area":null},{"id":"2507.06804","title":"Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving","created":"2025-07-07","cited_by_count":7,"area":"lr"},{"id":"2602.02990","title":"Learning to Repair Lean Proofs from Compiler Feedback","created":"2026-02-03","cited_by_count":7,"area":"agents"},{"id":"2605.17283","title":"OProver: A Unified Framework for Agentic Formal Theorem Proving","created":"2026-05-17","cited_by_count":7,"area":"agents"},{"id":"2606.20068","title":"Process-Verified Reinforcement Learning for Theorem Proving via Lean","created":"2026-06-18","cited_by_count":7,"area":"lr"},{"id":"2506.07477","title":"Premise Selection for a Lean Hammer","created":"2025-06-09","cited_by_count":6,"area":null},{"id":"2506.10903","title":"Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoning","created":"2025-06-12","cited_by_count":6,"area":"lr"},{"id":"2506.23908","title":"Beyond Statistical Learning: Exact Learning Is Essential for General Intelligence","created":"2025-06-30","cited_by_count":6,"area":"lr"},{"id":"2510.11769","title":"GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving","created":"2025-10-13","cited_by_count":6,"area":"lr"},{"id":"2603.12744","title":"TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib?","created":"2026-03-13","cited_by_count":6,"area":null},{"id":"2503.03238","title":"FANS -- Formal Answer Selection for Natural Language Math Reasoning Using Lean4","created":"2025-03-05","cited_by_count":5,"area":"lr"},{"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":"2510.26094","title":"Lean4Physics: Comprehensive Reasoning Framework for College-level Physics in Lean4","created":"2025-10-30","cited_by_count":5,"area":null},{"id":"2601.21210","title":"Uncovering Hidden Correctness in LLM Causal Reasoning via Symbolic Verification","created":"2026-01-29","cited_by_count":5,"area":"lr"},{"id":"2603.19514","title":"Learning to Disprove: Formal Counterexample Generation with Large Language Models","created":"2026-03-19","cited_by_count":5,"area":"lr"},{"id":"2604.26311","title":"DreamProver: Evolving Transferable Lemma Libraries via a Wake-Sleep Theorem-Proving Agent","created":"2026-04-29","cited_by_count":5,"area":"agents"},{"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":"2602.02561","title":"MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics","created":"2026-01-30","cited_by_count":4,"area":"lr"},{"id":"2603.18325","title":"Learning to Reason with Curriculum I: Provable Benefits of Autocurriculum","created":"2026-03-18","cited_by_count":4,"area":"lr"},{"id":"2605.20531","title":"Pseudo-Formalization for Automatic Proof Verification","created":"2026-05-19","cited_by_count":4,"area":"lr"},{"id":"2606.12594","title":"Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation","created":"2026-06-10","cited_by_count":4,"area":"lr"},{"id":"2606.26525","title":"Theory-Scale Auto-Formalization of Logics for Computer Science","created":"2026-06-25","cited_by_count":4,"area":null},{"id":"2606.31134","title":"Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics","created":"2026-06-30","cited_by_count":4,"area":"lr"},{"id":"2502.12275","title":"Integrating Expert Knowledge into Logical Programs via LLMs","created":"2025-02-17","cited_by_count":3,"area":"lr"},{"id":"2507.14335","title":"ProofCompass: Enhancing Specialized Provers with LLM Guidance","created":"2025-07-18","cited_by_count":3,"area":"lr"},{"id":"2508.15878","title":"Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs","created":"2025-08-21","cited_by_count":3,"area":"lr"},{"id":"2510.05016","title":"Large Language Models Achieve Gold Medal Performance at the International Olympiad on Astronomy & Astrophysics (IOAA)","created":"2025-10-06","cited_by_count":3,"area":null},{"id":"2512.00997","title":"IndiMathBench: Autoformalizing Mathematical Reasoning Problems with a Human Touch","created":"2025-11-30","cited_by_count":3,"area":"lr"},{"id":"2512.10317","title":"Translating Informal Proofs into Formal Proofs Using a Chain of States","created":"2025-12-11","cited_by_count":3,"area":null},{"id":"2606.04883","title":"Optimizing the Cost-Quality Tradeoff of Agentic Theorem Provers in Lean","created":"2026-06-03","cited_by_count":3,"area":"agents"},{"id":"2607.13292","title":"Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases","created":"2026-07-14","cited_by_count":3,"area":null},{"id":"2502.11901","title":"Building A Proof-Oriented Programmer That Is 64% Better Than GPT-4o Under Data Scarcity","created":"2025-02-17","cited_by_count":2,"area":"lr"},{"id":"2507.02541","title":"Clarifying Before Reasoning: A Coq Prover with Structural Context","created":"2025-07-03","cited_by_count":2,"area":"lr"},{"id":"2509.14274","title":"Discovering New Theorems via LLMs with In-Context Proof Learning in Lean","created":"2025-09-16","cited_by_count":2,"area":null},{"id":"2601.22365","title":"Towards Solving the Gilbert-Pollak Conjecture via Large Language Models","created":"2026-01-29","cited_by_count":2,"area":null},{"id":"2603.24914","title":"Shaping the Future of Mathematics in the Age of AI","created":"2026-03-26","cited_by_count":2,"area":null},{"id":"2605.10141","title":"FormalRewardBench: A Benchmark for Formal Theorem Proving Reward Models","created":"2026-05-11","cited_by_count":2,"area":"alignment"},{"id":"2606.14688","title":"Flood and Harvest: The Provable Necessity of Trivia for Generating Valuable Mathematics via the Lens of Language Generation in the Limit","created":"2026-06-12","cited_by_count":2,"area":null},{"id":"2606.19399","title":"VERITAS: Verifier-Guided Proof Search for Zero-Shot Formal Theorem Proving","created":"2026-06-17","cited_by_count":2,"area":null},{"id":"2608.20153","title":"FormalTCS: Benchmarking End-to-End Frontier Formal Theoretical Computer Science Research of Large Language Models","created":"2026-08-20","cited_by_count":2,"area":null},{"id":"2505.12031","title":"LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation","created":"2025-05-17","cited_by_count":1,"area":"synth"},{"id":"2509.12603","title":"EconProver: Towards More Economical Test-Time Scaling for Automated Theorem Proving","created":"2025-09-16","cited_by_count":1,"area":"lr"},{"id":"2510.12350","title":"O-Forge: An LLM + Computer Algebra Framework for Asymptotic Analysis","created":"2025-10-14","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":"2601.06795","title":"GDEPO: Group Dual-dynamic and Equal-right Advantage Policy Optimization with Enhanced Training Data Utilization for Sample-Constrained Reinforcement Learning","created":"2026-01-11","cited_by_count":1,"area":"lr"},{"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":"2603.24465","title":"MechMath: Sorrifier-Driven Formal Decomposition Workflow for Automated Theorem Proving","created":"2026-03-25","cited_by_count":1,"area":"agents"}],"next_cursor":"100"}