{"total":192,"rows":[{"id":"2303.18223","title":"A Survey of Large Language Models","created":"2023-03-31","cited_by_count":2576,"area":null},{"id":"2307.05782","title":"Large Language Models","created":"2023-07-11","cited_by_count":780,"area":null},{"id":"2306.15626","title":"LeanDojo: Theorem Proving with Retrieval-Augmented Language Models","created":"2023-06-27","cited_by_count":427,"area":"rag"},{"id":"2310.10631","title":"Llemma: An Open Language Model For Mathematics","created":"2023-10-16","cited_by_count":388,"area":"lr"},{"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":"2509.02547","title":"The Landscape of Agentic Reinforcement Learning for LLMs: A Survey","created":"2025-09-02","cited_by_count":205,"area":"agents"},{"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":"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":"2310.15164","title":"LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers","created":"2023-10-23","cited_by_count":168,"area":"lr"},{"id":"2310.06786","title":"OpenWebMath: An Open Dataset of High-Quality Mathematical Web Text","created":"2023-10-10","cited_by_count":155,"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":"2605.00674","title":"Beyond Benchmarks: MathArena as an Evaluation Platform for Mathematics with LLMs","created":"2026-05-01","cited_by_count":137,"area":null},{"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":"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":"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":"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":"2503.21380","title":"Challenging the Boundaries of Reasoning: An Olympiad-Level Math Benchmark for Large Language Models","created":"2025-03-27","cited_by_count":70,"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":"2312.17120","title":"MathPile: A Billion-Token-Scale Pretraining Corpus for Math","created":"2023-12-28","cited_by_count":67,"area":null},{"id":"2407.03203","title":"TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts","created":"2024-07-03","cited_by_count":59,"area":"lr"},{"id":"2410.10878","title":"Herald: A Natural Language Annotated Lean 4 Dataset","created":"2024-10-09","cited_by_count":59,"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":"2404.09939","title":"A Survey on Deep Learning for Theorem Proving","created":"2024-04-15","cited_by_count":57,"area":null},{"id":"2403.18120","title":"Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization","created":"2024-03-26","cited_by_count":55,"area":"lr"},{"id":"2406.18321","title":"MathOdyssey: Benchmarking Mathematical Problem-Solving Skills in Large Language Models Using Odyssey Math Data","created":"2024-06-26","cited_by_count":52,"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":"2406.01940","title":"Process-Driven Autoformalization in Lean 4","created":"2024-06-04","cited_by_count":45,"area":"lr"},{"id":"2311.03755","title":"Multilingual Mathematical Autoformalization","created":"2023-11-07","cited_by_count":39,"area":null},{"id":"2508.15096","title":"Nemotron-CC-Math: A 133 Billion-Token-Scale High Quality Math Pretraining Dataset","created":"2025-08-20","cited_by_count":38,"area":"lr"},{"id":"2305.16366","title":"Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving","created":"2023-05-25","cited_by_count":37,"area":"diffusion"},{"id":"2408.03350","title":"miniCTX: Neural Theorem Proving with (Long-)Contexts","created":"2024-08-05","cited_by_count":37,"area":null},{"id":"2502.15815","title":"Theoretical Physics Benchmark (TPBench) -- a Dataset and Study of AI Reasoning Capabilities in Theoretical Physics","created":"2025-02-19","cited_by_count":34,"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":"2504.05605","title":"ShadowCoT: Cognitive Hijacking for Stealthy Reasoning Backdoors in LLMs","created":"2025-04-08","cited_by_count":30,"area":"lr"},{"id":"2402.07625","title":"Autonomous Data Selection with Zero-shot Generative Classifiers for Mathematical Texts","created":"2024-02-12","cited_by_count":27,"area":null},{"id":"2405.17216","title":"Autoformalizing Euclidean Geometry","created":"2024-05-27","cited_by_count":27,"area":null},{"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":"2309.15806","title":"Lyra: Orchestrating Dual Correction in Automated Theorem Proving","created":"2023-09-27","cited_by_count":25,"area":null},{"id":"2312.07622","title":"Mathematical Language Models: A Survey","created":"2023-12-12","cited_by_count":24,"area":null},{"id":"2410.10135","title":"FormalAlign: Automated Alignment Evaluation for Autoformalization","created":"2024-10-14","cited_by_count":24,"area":null},{"id":"2412.03205","title":"U-MATH: A University-Level Benchmark for Evaluating Mathematical Skills in LLMs","created":"2024-12-04","cited_by_count":24,"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":"2502.12065","title":"Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitions","created":"2025-02-17","cited_by_count":22,"area":null},{"id":"2410.04194","title":"Consistent Autoformalization for Constructing Mathematical Libraries","created":"2024-10-05","cited_by_count":21,"area":null},{"id":"2510.04520","title":"Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graph","created":"2025-10-06","cited_by_count":21,"area":"agents"},{"id":"2506.17114","title":"Mathematical Proof as a Litmus Test: Revealing Failure Modes of Advanced Large Reasoning Models","created":"2025-06-20","cited_by_count":20,"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":"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":"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":"2507.09662","title":"Towards Concise and Adaptive Thinking in Large Reasoning Models: A Survey","created":"2025-07-13","cited_by_count":18,"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":"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":"2410.12881","title":"MIND: Math Informed syNthetic Dialogues for Pretraining LLMs","created":"2024-10-15","cited_by_count":14,"area":"lr"},{"id":"2502.10454","title":"One Example Shown, Many Concepts Known! Counterexample-Driven Conceptual Reasoning in Mathematical LLMs","created":"2025-02-12","cited_by_count":14,"area":"lr"},{"id":"2505.24869","title":"SiLVR: A Simple Language-based Video Reasoning Framework","created":"2025-05-30","cited_by_count":14,"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.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":"2601.20055","title":"VERGE: Formal Refinement and Guidance Engine for Verifiable LLM Reasoning","created":"2026-01-27","cited_by_count":12,"area":"lr"},{"id":"2412.15184","title":"Data for Mathematical Copilots: Better Ways of Presenting Proofs for Machine Learning","created":"2024-12-19","cited_by_count":11,"area":null},{"id":"2502.06217","title":"Examining False Positives under Inference Scaling for Mathematical Reasoning","created":"2025-02-10","cited_by_count":11,"area":"lr"},{"id":"2502.14333","title":"A Survey on Feedback-based Multi-step Reasoning for Large Language Models on Mathematics","created":"2025-02-20","cited_by_count":11,"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":"2306.08997","title":"Exploring the MIT Mathematics and EECS Curriculum Using Large Language Models","created":"2023-06-15","cited_by_count":10,"area":null},{"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":"2509.22246","title":"ASSESS: A Semantic and Structural Evaluation Framework for Statement Similarity","created":"2025-09-26","cited_by_count":10,"area":null},{"id":"2511.06209","title":"ReProbe: Efficient Test-Time Scaling of Multi-Step Reasoning by Probing Internal States of Large Language Models","created":"2025-11-09","cited_by_count":10,"area":"lr"},{"id":"2605.29955","title":"Formalizing Mathematics at Scale","created":"2026-05-28","cited_by_count":10,"area":null},{"id":"2606.31002","title":"Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization","created":"2026-06-30","cited_by_count":10,"area":null},{"id":"2408.15332","title":"What makes math problems hard for reinforcement learning: a case study","created":"2024-08-27","cited_by_count":9,"area":"deeprl"},{"id":"2307.10573","title":"Invalid Logic, Equivalent Gains: The Bizarreness of Reasoning in Language Model Prompting","created":"2023-07-20","cited_by_count":8,"area":"lr"},{"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":"2604.06802","title":"Riemann-Bench: A Benchmark for Moonshot Mathematics","created":"2026-04-08","cited_by_count":8,"area":null},{"id":"2604.25031","title":"Faithful Autoformalization via Roundtrip Verification and Repair","created":"2026-04-27","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":"2512.10534","title":"Achieving Olympiad-Level Geometry Large Language Model Agent via Complexity Boosting Reinforcement Learning","created":"2025-12-11","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":"2406.06140","title":"Can I understand what I create? Self-Knowledge Evaluation of Large Language Models","created":"2024-06-10","cited_by_count":6,"area":null},{"id":"2411.18104","title":"Training and Evaluating Language Models with Template-based Data Generation","created":"2024-11-27","cited_by_count":6,"area":null},{"id":"2505.13406","title":"AutoMathKG: The automated mathematical knowledge graph based on LLM and vector database","created":"2025-05-19","cited_by_count":6,"area":null},{"id":"2505.15740","title":"HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement","created":"2025-05-21","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":"2510.08988","title":"MASA: LLM-Driven Multi-Agent Systems for Autoformalization","created":"2025-10-10","cited_by_count":6,"area":"agents"},{"id":"2510.11769","title":"GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving","created":"2025-10-13","cited_by_count":6,"area":"lr"},{"id":"2606.16541","title":"The Faithfulness Gap: Certifying Semantic Equivalence Between Natural-Language and Formal Mathematical Statements","created":"2026-06-15","cited_by_count":6,"area":null},{"id":"2505.20869","title":"Step-Wise Formal Verification for LLM-Based Mathematical Problem Solving","created":"2025-05-27","cited_by_count":5,"area":"lr"},{"id":"2508.06931","title":"Automated Formalization via Conceptual Retrieval-Augmented LLMs","created":"2025-08-09","cited_by_count":5,"area":"rag"},{"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.01400","title":"EternalMath: A Living Benchmark of Frontier Mathematics that Evolves with Human Discovery","created":"2026-01-04","cited_by_count":4,"area":"lr"},{"id":"2602.02561","title":"MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics","created":"2026-01-30","cited_by_count":4,"area":"lr"},{"id":"2604.23002","title":"FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean","created":"2026-04-24","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":"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}],"next_cursor":"100"}