{"total":79,"rows":[{"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":"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":"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":"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":"2403.18120","title":"Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization","created":"2024-03-26","cited_by_count":55,"area":"lr"},{"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":"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":"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":"2504.05605","title":"ShadowCoT: Cognitive Hijacking for Stealthy Reasoning Backdoors in LLMs","created":"2025-04-08","cited_by_count":30,"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":"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":"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":"2601.20055","title":"VERGE: Formal Refinement and Guidance Engine for Verifiable LLM Reasoning","created":"2026-01-27","cited_by_count":12,"area":"lr"},{"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":"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":"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":"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.11769","title":"GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving","created":"2025-10-13","cited_by_count":6,"area":"lr"},{"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":"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":"2607.04655","title":"FormalRx: Rectify and eXamine Semantic Failures in Autoformalization","created":"2026-07-06","cited_by_count":4,"area":"lr"},{"id":"2404.18130","title":"Logic Agent: Enhancing Validity with Logic Rule Invocation","created":"2024-04-28","cited_by_count":3,"area":"lr"},{"id":"2504.04945","title":"A Llama walks into the 'Bar': Efficient Supervised Fine-Tuning for Legal Reasoning in the Multi-state Bar Exam","created":"2025-04-07","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":"2512.00997","title":"IndiMathBench: Autoformalizing Mathematical Reasoning Problems with a Human Touch","created":"2025-11-30","cited_by_count":3,"area":"lr"},{"id":"2605.28365","title":"Risk-Controlled Lean-as-Judge for Natural-Language Mathematical Reasoning","created":"2026-05-27","cited_by_count":3,"area":"lr"},{"id":"2409.11074","title":"RoMath: A Mathematical Reasoning Benchmark in Romanian","created":"2024-09-17","cited_by_count":2,"area":"lr"},{"id":"2410.08437","title":"Autonomous Evaluation of LLMs for Truth Maintenance and Reasoning Tasks","created":"2024-10-11","cited_by_count":2,"area":"lr"},{"id":"2503.11657","title":"Scaling Natural-Language Graph-Based Test Time Compute for Automated Theorem Proving","created":"2025-02-04","cited_by_count":2,"area":"lr"},{"id":"2510.07697","title":"Rethinking Reasoning: A Survey on Reasoning-based Backdoors in LLMs","created":"2025-10-09","cited_by_count":2,"area":"lr"},{"id":"2510.11986","title":"Conjecturing: An Overlooked Step in Formal Mathematical Reasoning","created":"2025-10-13","cited_by_count":2,"area":"lr"},{"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":"2402.03667","title":"Large Language Models as an Indirect Reasoner: Contrapositive and Contradiction for Automated Reasoning","created":"2024-02-06","cited_by_count":1,"area":"lr"},{"id":"2504.20771","title":"Computational Reasoning of Large Language Models","created":"2025-04-29","cited_by_count":1,"area":"lr"},{"id":"2505.18492","title":"Formally Solving Answer-Construction Problems in Lean","created":"2025-05-24","cited_by_count":1,"area":"lr"},{"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":"2605.07147","title":"MathlibPR: Pull Request Merge-Readiness Benchmark for Formal Mathematical Libraries","created":"2026-05-08","cited_by_count":1,"area":"lr"},{"id":"2605.09292","title":"Beyond Accuracy: Evaluating Strategy Diversity in LLM Mathematical Reasoning","created":"2026-05-10","cited_by_count":1,"area":"lr"},{"id":"2605.19723","title":"Mathematical Reasoning in Large Language Models: Benchmarks, Architectures, Evaluation, and Open Challenges","created":"2026-05-19","cited_by_count":1,"area":"lr"},{"id":"2605.30914","title":"Automating Formal Verification with Reinforcement Learning and Recursive Inference","created":"2026-05-29","cited_by_count":1,"area":"lr"},{"id":"2606.02113","title":"A Primer in Post-Training Reasoning Data: What We Know About How It Works","created":"2026-06-01","cited_by_count":1,"area":"lr"},{"id":"2606.08728","title":"Artificial Intelligence for Mathematical Reasoning: An Integrated Survey of Language Models, Neuro-symbolic Systems, and Verified Discovery","created":"2026-06-07","cited_by_count":1,"area":"lr"},{"id":"2606.28841","title":"LAMP: Lean-based Agentic framework with MCP and Proof Repair","created":"2026-06-27","cited_by_count":1,"area":"lr"},{"id":"2510.12997","title":"Max It or Miss It: Benchmarking LLM On Solving Extremal Problems","created":"2025-10-14","cited_by_count":0,"area":"lr"},{"id":"2601.13392","title":"Beyond Memorization: Testing LLM Reasoning on Unseen Theory of Computation Tasks","created":"2026-01-19","cited_by_count":0,"area":"lr"},{"id":"2604.02709","title":"Evaluating the Formal Reasoning Capabilities of Large Language Models through Chomsky Hierarchy","created":"2026-04-03","cited_by_count":0,"area":"lr"},{"id":"2604.06401","title":"ProofSketcher: Hybrid LLM + Lightweight Proof Checker for Reliable Math/Logic Reasoning","created":"2026-04-07","cited_by_count":0,"area":"lr"},{"id":"2604.18587","title":"Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs","created":"2026-03-13","cited_by_count":0,"area":"lr"},{"id":"2605.09012","title":"Re$^2$Math: Benchmarking Theorem Retrieval in Research-Level Mathematics","created":"2026-05-09","cited_by_count":0,"area":"lr"},{"id":"2605.17255","title":"CAM-Bench: A Benchmark for Computational and Applied Mathematics in Lean","created":"2026-05-17","cited_by_count":0,"area":"lr"},{"id":"2606.06526","title":"CrowdMath: A Dataset of Crowdsourced Mathematical Research Discussions","created":"2026-06-02","cited_by_count":0,"area":"lr"},{"id":"2606.19315","title":"Diffusion-Proof: Recipe for Formal Theorem Proving Beyond Auto-Regressive Generation","created":"2026-06-17","cited_by_count":0,"area":"lr"},{"id":"2608.25449","title":"MathAdv: What Theorem Provers Know, Reason, Formalize, and Generalize","created":"2026-08-26","cited_by_count":0,"area":"lr"},{"id":"2608.26950","title":"From Atomic to Agentic: Towards Interpretable Evaluation of LLMs' Agentic Mathematical Capabilities","created":"2026-08-27","cited_by_count":0,"area":"lr"}],"next_cursor":null}