{"total":134,"rows":[{"id":"2306.15626","title":"LeanDojo: Theorem Proving with Retrieval-Augmented Language Models","created":"2023-06-27","cited_by_count":427,"area":"rag"},{"id":"2109.00110","title":"MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics","created":"2021-08-31","cited_by_count":391,"area":null},{"id":"2310.10631","title":"Llemma: An Open Language Model For Mathematics","created":"2023-10-16","cited_by_count":388,"area":"lr"},{"id":"2301.13867","title":"Mathematical Capabilities of ChatGPT","created":"2023-01-31","cited_by_count":268,"area":null},{"id":"2205.11491","title":"HyperTree Proof Search for Neural Theorem Proving","created":"2022-05-23","cited_by_count":197,"area":null},{"id":"2408.08152","title":"DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search","created":"2024-08-15","cited_by_count":197,"area":"lr"},{"id":"2302.12433","title":"ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics","created":"2023-02-24","cited_by_count":192,"area":null},{"id":"2407.11214","title":"PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition","created":"2024-07-15","cited_by_count":165,"area":null},{"id":"2102.06203","title":"Proof Artifact Co-training for Theorem Proving with Language Models","created":"2021-02-11","cited_by_count":132,"area":"offlinerl"},{"id":"2212.10535","title":"A Survey of Deep Learning for Mathematical Reasoning","created":"2022-12-20","cited_by_count":124,"area":"lr"},{"id":"2406.03847","title":"Lean Workbook: A large-scale Lean problem set formalized from natural language math problems","created":"2024-06-06","cited_by_count":122,"area":null},{"id":"2402.06332","title":"InternLM-Math: Open Math Large Language Models Toward Verifiable Reasoning","created":"2024-02-09","cited_by_count":119,"area":"lr"},{"id":"2310.00656","title":"LEGO-Prover: Neural Theorem Proving with Growing Libraries","created":"2023-10-01","cited_by_count":109,"area":null},{"id":"2304.11062","title":"Scaling Transformer to 1M tokens and beyond with RMT","created":"2023-04-19","cited_by_count":98,"area":null},{"id":"2310.04353","title":"An In-Context Learning Agent for Formal Theorem-Proving","created":"2023-10-06","cited_by_count":82,"area":"agents"},{"id":"2412.16075","title":"Formal Mathematical Reasoning: A New Frontier in AI","created":"2024-12-20","cited_by_count":81,"area":"lr"},{"id":"2502.00212","title":"STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving","created":"2025-01-31","cited_by_count":79,"area":"lr"},{"id":"2407.10040","title":"Lean-STaR: Learning to Interleave Thinking and Proving","created":"2024-07-14","cited_by_count":68,"area":"lr"},{"id":"2404.12534","title":"Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean","created":"2024-04-18","cited_by_count":58,"area":null},{"id":"2311.14125","title":"Scalable AI Safety via Doubly-Efficient Debate","created":"2023-11-23","cited_by_count":57,"area":null},{"id":"2309.04295","title":"FIMO: A Challenge Formal Dataset for Automated Theorem Proving","created":"2023-09-08","cited_by_count":55,"area":null},{"id":"2101.06223","title":"LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning","created":"2021-01-15","cited_by_count":46,"area":null},{"id":"2408.03350","title":"miniCTX: Neural Theorem Proving with (Long-)Contexts","created":"2024-08-05","cited_by_count":37,"area":null},{"id":"2410.15700","title":"InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Search","created":"2024-10-21","cited_by_count":34,"area":null},{"id":"2505.23135","title":"VERINA: Benchmarking Verifiable Code Generation","created":"2025-05-29","cited_by_count":34,"area":null},{"id":"2310.18457","title":"LLMSTEP: LLM proofstep suggestions in Lean","created":"2023-10-27","cited_by_count":32,"area":null},{"id":"2406.07222","title":"Reliable Evaluation and Benchmarks for Statement Autoformalization","created":"2024-06-11","cited_by_count":32,"area":null},{"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":"2505.13938","title":"CLEVER: A Curated Benchmark for Formally Verified Code Generation","created":"2025-05-20","cited_by_count":29,"area":null},{"id":"2407.17227","title":"LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover","created":"2024-07-24","cited_by_count":25,"area":"lr"},{"id":"2310.10180","title":"TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models","created":"2023-10-16","cited_by_count":24,"area":"lr"},{"id":"2406.14408","title":"FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving","created":"2024-06-20","cited_by_count":22,"area":null},{"id":"2403.04571","title":"Machine learning and information theory concepts towards an AI Mathematician","created":"2024-03-07","cited_by_count":20,"area":"lr"},{"id":"2405.01787","title":"Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming","created":"2024-05-03","cited_by_count":20,"area":null},{"id":"2406.11915","title":"miniCodeProps: a Minimal Benchmark for Proving Code Properties","created":"2024-06-16","cited_by_count":18,"area":null},{"id":"2501.16207","title":"From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs","created":"2025-01-27","cited_by_count":18,"area":"lr"},{"id":"2602.24273","title":"A Minimal Agent for Automated Theorem Proving","created":"2026-02-27","cited_by_count":18,"area":"agents"},{"id":"2506.04592","title":"Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification","created":"2025-06-05","cited_by_count":17,"area":"lr"},{"id":"2602.17016","title":"M2F: Automated Formalization of Mathematical Literature at Scale","created":"2026-02-19","cited_by_count":15,"area":null},{"id":"2407.11373","title":"Reliable Reasoning Beyond Natural Language","created":"2024-07-16","cited_by_count":14,"area":"lr"},{"id":"2606.03303","title":"LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks","created":"2026-06-02","cited_by_count":12,"area":"lr"},{"id":"2603.19329","title":"Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification","created":"2026-03-18","cited_by_count":11,"area":null},{"id":"2304.00994","title":"Machine-Learned Premise Selection for Lean","created":"2023-03-17","cited_by_count":10,"area":null},{"id":"2310.07957","title":"A New Approach Towards Autoformalization","created":"2023-10-12","cited_by_count":10,"area":null},{"id":"2410.04753","title":"ImProver: Agent-Based Automated Proof Optimization","created":"2024-10-07","cited_by_count":10,"area":"agents"},{"id":"2502.17925","title":"LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction","created":"2025-02-25","cited_by_count":10,"area":"lr"},{"id":"2509.22246","title":"ASSESS: A Semantic and Structural Evaluation Framework for Statement Similarity","created":"2025-09-26","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":"2510.10815","title":"DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems","created":"2025-10-12","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.03071","title":"Automatic Textbook Formalization","created":"2026-04-03","cited_by_count":8,"area":null},{"id":"2504.19110","title":"APE-Bench: Evaluating Automated Proof Engineering for Formal Math Libraries","created":"2025-04-27","cited_by_count":7,"area":null},{"id":"2511.03618","title":"Towards Formalizing Reinforcement Learning Theory: A Robbins-Siegmund Approach","created":"2025-11-05","cited_by_count":7,"area":"deeprl"},{"id":"2506.07477","title":"Premise Selection for a Lean Hammer","created":"2025-06-09","cited_by_count":6,"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":"2603.19514","title":"Learning to Disprove: Formal Counterexample Generation with Large Language Models","created":"2026-03-19","cited_by_count":5,"area":"lr"},{"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.14000","title":"Formalizing Numerical Analysis: An Agent Pipeline and Quality Audit Beyond Kernel Acceptance","created":"2026-06-12","cited_by_count":5,"area":"agents"},{"id":"2608.28433","title":"Prove2Me: An Open Collaborative Platform for Scaling Math Formalization","created":"2026-08-28","cited_by_count":5,"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":"2605.14061","title":"MathAtlas: A Benchmark for Autoformalization in the Wild","created":"2026-05-13","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":"2606.31134","title":"Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics","created":"2026-06-30","cited_by_count":4,"area":"lr"},{"id":"2607.04655","title":"FormalRx: Rectify and eXamine Semantic Failures in Autoformalization","created":"2026-07-06","cited_by_count":4,"area":"lr"},{"id":"2608.29270","title":"SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization","created":"2026-08-29","cited_by_count":4,"area":null},{"id":"2503.19605","title":"Lean Formalization of Generalization Error Bound by Rademacher Complexity and Dudley's Entropy Integral","created":"2025-03-25","cited_by_count":3,"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":"2605.30333","title":"COMPOSE: Composing Future Theorems from Citations and Formal Structure","created":"2026-05-28","cited_by_count":3,"area":null},{"id":"2606.23959","title":"Does My Embedding Reflect That $A = B$? Evaluating Mathematical Equivalence in Embedding Models","created":"2026-06-22","cited_by_count":3,"area":null},{"id":"2607.28699","title":"WitCert: Sound Runtime Risk Observability and Gating for KV-Cache Quantization","created":"2026-07-30","cited_by_count":3,"area":"inference"},{"id":"2402.04689","title":"Stein Boltzmann Sampling: A Variational Approach for Global Optimization","created":"2024-02-07","cited_by_count":2,"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":"2512.07766","title":"Formalized Hopfield Networks and Boltzmann Machines","created":"2025-12-08","cited_by_count":2,"area":null},{"id":"2512.10187","title":"MINIF2F-DAFNY: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification","created":"2025-12-11","cited_by_count":2,"area":"lr"},{"id":"2604.16584","title":"Certified Program Synthesis with a Multi-Modal Verifier","created":"2026-04-17","cited_by_count":2,"area":null},{"id":"2605.27246","title":"Many Logics, One Methodology: A Plea for Logical Pluralism in Formalised Reasoning (preprint)","created":"2026-05-26","cited_by_count":2,"area":null},{"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":"2607.09632","title":"Lean-QIT: Towards a Formal Infrastructure for Quantum Information Theory","created":"2026-07-10","cited_by_count":2,"area":null},{"id":"2608.13522","title":"Vero: Can AI Agents Build Formally Verified Software Repositories?","created":"2026-08-13","cited_by_count":2,"area":null},{"id":"2608.15432","title":"Does the Proof Prove It That Way? Faithful Formalization of Elements Proofs","created":"2026-08-15","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":"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":"2505.18492","title":"Formally Solving Answer-Construction Problems in Lean","created":"2025-05-24","cited_by_count":1,"area":"lr"},{"id":"2505.23557","title":"Learning Parametric Distributions from Samples and Preferences","created":"2025-05-29","cited_by_count":1,"area":"alignment"},{"id":"2510.23637","title":"Combining Textual and Structural Information for Premise Selection in Lean","created":"2025-10-24","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":"2602.20770","title":"Pipeline for Verifying LLM-Generated Mathematical Solutions","created":"2026-02-24","cited_by_count":1,"area":"lr"},{"id":"2603.24465","title":"MechMath: Sorrifier-Driven Formal Decomposition Workflow for Automated Theorem Proving","created":"2026-03-25","cited_by_count":1,"area":"agents"},{"id":"2605.19063","title":"Mapping Uncharted Symmetries: Machine Discovery in Combinatorics","created":"2026-05-18","cited_by_count":1,"area":null},{"id":"2605.22257","title":"What are the Right Symmetries for Formal Theorem Proving?","created":"2026-05-21","cited_by_count":1,"area":null},{"id":"2606.00329","title":"Benchmarking Recursive-Collapse Warning Claims Under Matched False-Positive Control","created":"2026-05-29","cited_by_count":1,"area":null},{"id":"2606.10799","title":"Evaluating Research-Level Math Proofs via Strict Step-Level Verification","created":"2026-06-09","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":"2606.20642","title":"Hypothesis-Disciplined Multi-Agent Automated Formalization of Asymptotic Statistical Theory","created":"2026-06-03","cited_by_count":1,"area":null},{"id":"2607.19407","title":"ITPEval: Benchmarking Formal Translation Across Interactive Theorem Provers","created":"2026-07-07","cited_by_count":1,"area":null},{"id":"2607.22511","title":"CausalSmith: A Formally Grounded, Self-Improving Agentic Framework for Automated Research in Causal Inference","created":"2026-07-24","cited_by_count":1,"area":"agents"},{"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":"2402.16878","title":"EvoGPT-f: An Evolutionary GPT Framework for Benchmarking Formal Math Languages","created":"2024-02-12","cited_by_count":0,"area":null},{"id":"2506.07066","title":"From Axioms to Algorithms: Mechanized Proofs of the vNM Utility Theorem","created":"2025-06-08","cited_by_count":0,"area":null}],"next_cursor":"100"}