{"total":45,"rows":[{"id":"2505.23281","title":"MathArena: Evaluating LLMs on Uncontaminated Math Competitions","created":"2025-05-29","cited_by_count":297,"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":"2507.23726","title":"Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving","created":"2025-07-31","cited_by_count":101,"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":"2506.02355","title":"Rewarding the Unlikely: Lifting GRPO Beyond Distribution Sharpening","created":"2025-06-03","cited_by_count":80,"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.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":"2506.08446","title":"A Survey on Large Language Models for Mathematical Reasoning","created":"2025-06-10","cited_by_count":52,"area":"lr"},{"id":"2412.20735","title":"HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving","created":"2024-12-30","cited_by_count":33,"area":"lr"},{"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":"2501.11110","title":"Chain-of-Reasoning: Towards Unified Mathematical Reasoning in Large Language Models via a Multi-Paradigm Perspective","created":"2025-01-19","cited_by_count":29,"area":"lr"},{"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":"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":"2506.07927","title":"Solving Inequality Proofs with Large Language Models","created":"2025-06-09","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":"2510.13888","title":"Reliable Fine-Grained Evaluation of Natural Language Math Proofs","created":"2025-10-14","cited_by_count":18,"area":"lr"},{"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.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":"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":"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":"2606.20068","title":"Process-Verified Reinforcement Learning for Theorem Proving via Lean","created":"2026-06-18","cited_by_count":7,"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":"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":"2603.19514","title":"Learning to Disprove: Formal Counterexample Generation with Large Language Models","created":"2026-03-19","cited_by_count":5,"area":"lr"},{"id":"2507.11275","title":"FMC: Formalization of Natural Language Mathematical Competition Problems","created":"2025-07-15","cited_by_count":4,"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":"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":"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":"2505.00001","title":"Rosetta-PL: Propositional Logic as a Benchmark for Large Language Model Reasoning","created":"2025-03-25","cited_by_count":2,"area":"lr"},{"id":"2506.01531","title":"STORM-BORN: A Challenging Mathematical Derivations Dataset Curated via a Human-in-the-Loop Multi-Agent Framework","created":"2025-06-02","cited_by_count":2,"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":"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":"2605.30914","title":"Automating Formal Verification with Reinforcement Learning and Recursive Inference","created":"2026-05-29","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":"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":"2605.11905","title":"Rethinking Supervision Granularity: Segment-Level Learning for LLM-Based Theorem Proving","created":"2026-05-12","cited_by_count":0,"area":"lr"},{"id":"2606.05030","title":"Imbuing Large Language Models with Bidirectional Logic for Robust Chain Repair","created":"2026-06-03","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"}],"next_cursor":null}