{"total":67,"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":"2507.23726","title":"Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving","created":"2025-07-31","cited_by_count":101,"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":"2509.22819","title":"Hilbert: Recursively Building Formal Proofs with Informal Reasoning","created":"2025-09-26","cited_by_count":60,"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":"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":"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":"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":"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.16395","title":"OJBench: A Competition Level Code Benchmark For Large Language Models","created":"2025-06-19","cited_by_count":26,"area":"lr"},{"id":"2605.22763","title":"Advancing Mathematics Research with AI-Driven Formal Proof Search","created":"2026-05-21","cited_by_count":23,"area":"lr"},{"id":"2509.18883","title":"Introducing LongCat-Flash-Thinking: A Technical Report","created":"2025-09-23","cited_by_count":22,"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":"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":"2506.04894","title":"ICPC-Eval: Probing the Frontiers of LLM Reasoning with Competitive Programming Contests","created":"2025-06-05","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":"2606.03303","title":"LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks","created":"2026-06-02","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.18760","title":"HERMES: Towards Efficient and Verifiable Mathematical Reasoning in LLMs","created":"2025-11-24","cited_by_count":11,"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":"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":"2508.14644","title":"LeanGeo: Formalizing Competitional Geometry problems in Lean","created":"2025-08-20","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":"2506.04821","title":"LogicPuzzleRL: Cultivating Robust Mathematical Reasoning in LLMs via Reinforcement Learning","created":"2025-06-05","cited_by_count":5,"area":"lr"},{"id":"2510.19842","title":"DAG-Math: Graph-of-Thought Guided Mathematical Reasoning in LLMs","created":"2025-10-19","cited_by_count":5,"area":"lr"},{"id":"2601.22642","title":"Pushing the Boundaries of Natural Reasoning: Interleaved Bonus from Formal-Logic Verification","created":"2026-01-30","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":"2608.31075","title":"Scaling Large Reasoning Models beyond Human Supervision: A Path toward Superintelligence","created":"2026-08-31","cited_by_count":5,"area":"lr"},{"id":"2508.00459","title":"Thinking Machines: Mathematical Reasoning in the Age of LLMs","created":"2025-08-01","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.12594","title":"Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation","created":"2026-06-10","cited_by_count":4,"area":"lr"},{"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":"2506.18421","title":"TReB: A Comprehensive Benchmark for Evaluating Table Reasoning Capabilities of Large Language Models","created":"2025-06-23","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":"2512.00997","title":"IndiMathBench: Autoformalizing Mathematical Reasoning Problems with a Human Touch","created":"2025-11-30","cited_by_count":3,"area":"lr"},{"id":"2512.05962","title":"Whatever Remains Must Be True: Filtering Drives Reasoning in LLMs, Shaping Diversity","created":"2025-12-05","cited_by_count":3,"area":"lr"},{"id":"2603.29500","title":"Learning to Generate Formally Verifiable Step-by-Step Logic Reasoning via Structured Formal Intermediaries","created":"2026-03-31","cited_by_count":3,"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":"2510.07486","title":"AsyncSpade: Efficient Test-Time Scaling with Asynchronous Sparse Decoding","created":"2025-10-08","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":"2512.20760","title":"Generalization of RLVR Using Causal Reasoning as a Testbed","created":"2025-12-23","cited_by_count":2,"area":"lr"},{"id":"2607.11307","title":"Efficient Test-Time Optimization for Multi-Agent Proof Autoformalization","created":"2026-07-13","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":"2602.20770","title":"Pipeline for Verifying LLM-Generated Mathematical Solutions","created":"2026-02-24","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.15445","title":"From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates","created":"2026-05-14","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.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":"2607.14178","title":"ReasFlow: Assisting Reasoning-Centric Scientific Discovery in Applied Mathematics via a Knowledge-Based Multi-Agent System","created":"2026-07-15","cited_by_count":1,"area":"lr"},{"id":"2509.20208","title":"Play by the Type Rules: Inferring Constraints for LLM Functions in Declarative Programs","created":"2025-09-24","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.13515","title":"SFT-GRPO Data Overlap as a Post-Training Hyperparameter for Autoformalization","created":"2026-04-15","cited_by_count":0,"area":"lr"},{"id":"2604.17010","title":"Improving LLM Code Reasoning via Semantic Equivalence Self-Play with Formal Verification","created":"2026-04-18","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.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.15972","title":"Formalize Once, Edit the Rest: Efficient Lean-Based Answer Selection for Math Reasoning","created":"2026-06-14","cited_by_count":0,"area":"lr"},{"id":"2606.16154","title":"A Gradient Perspective on RLVR Stability and Winner Advantage Policy Optimization","created":"2026-06-15","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":"2609.30192","title":"SAGE: Mitigating Long-Horizon Reasoning Biases via Topological Guidance","created":"2026-09-24","cited_by_count":0,"area":"lr"}],"next_cursor":null}