{"total":48,"rows":[{"id":"2509.22819","title":"Hilbert: Recursively Building Formal Proofs with Informal Reasoning","created":"2025-09-26","cited_by_count":60,"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":"2605.22763","title":"Advancing Mathematics Research with AI-Driven Formal Proof Search","created":"2026-05-21","cited_by_count":23,"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":"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":"2510.04474","title":"DRPO: Efficient Reasoning via Decoupled Reward Policy Optimization","created":"2025-10-06","cited_by_count":16,"area":"lr"},{"id":"2601.03715","title":"R$^3$L: Reflect-then-Retry Reinforcement Learning with Language-Guided Exploration, Pivotal Credit, and Positive Amplification","created":"2026-01-07","cited_by_count":12,"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":"2511.18760","title":"HERMES: Towards Efficient and Verifiable Mathematical Reasoning in LLMs","created":"2025-11-24","cited_by_count":11,"area":"lr"},{"id":"2602.16793","title":"Escaping the Cognitive Well: Efficient Competition Math with Off-the-Shelf Models","created":"2026-02-18","cited_by_count":9,"area":"lr"},{"id":"2508.14644","title":"LeanGeo: Formalizing Competitional Geometry problems in Lean","created":"2025-08-20","cited_by_count":7,"area":"lr"},{"id":"2605.02909","title":"Delay, Plateau, or Collapse: Evaluating the Impact of Systematic Verification Error on RLVR","created":"2026-04-06","cited_by_count":7,"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":"2510.19842","title":"DAG-Math: Graph-of-Thought Guided Mathematical Reasoning in LLMs","created":"2025-10-19","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.10916","title":"FaithformBench: Benchmarking Faithfulness of Mathematical Chain-of-Thought Autoformalisation","created":"2026-08-11","cited_by_count":5,"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":"2605.20531","title":"Pseudo-Formalization for Automatic Proof Verification","created":"2026-05-19","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":"2605.28365","title":"Risk-Controlled Lean-as-Judge for Natural-Language Mathematical Reasoning","created":"2026-05-27","cited_by_count":3,"area":"lr"},{"id":"2511.05705","title":"Long Grounded Thoughts: Synthesizing Visual Problems and Reasoning Chains at Scale","created":"2025-11-07","cited_by_count":2,"area":"lr"},{"id":"2604.00790","title":"RefineRL: Advancing Competitive Programming with Self-Refinement Reinforcement Learning","created":"2026-04-01","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":"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":"2603.22363","title":"Early Discoveries of Algorithmist I: Promise of Provable Algorithm Synthesis at Scale","created":"2026-03-23","cited_by_count":1,"area":"lr"},{"id":"2604.01302","title":"Scaling Reasoning Tokens via RL and Parallel Thinking: Evidence From Competitive Programming","created":"2026-04-01","cited_by_count":1,"area":"lr"},{"id":"2604.19558","title":"On Reasoning-Centric LLM-based Automated Theorem Proving","created":"2026-04-21","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.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":"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":"2607.17352","title":"Self-Modifying Lean Proof Agents with Verifier-Grounded Benchmark Coevolution","created":"2026-07-19","cited_by_count":1,"area":"lr"},{"id":"2604.18050","title":"The Topological Dual of a Dataset: A Logic-to-Topology Encoding for AlphaGeometry-Style Data","created":"2026-04-20","cited_by_count":0,"area":"lr"},{"id":"2605.00677","title":"Evaluating the Architectural Reasoning Capabilities of LLM Provers via the Obfuscated Natural Number Game","created":"2026-05-01","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":"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.19315","title":"Diffusion-Proof: Recipe for Formal Theorem Proving Beyond Auto-Regressive Generation","created":"2026-06-17","cited_by_count":0,"area":"lr"},{"id":"2607.21856","title":"LeAct: Learning to Reason from Expert Actions","created":"2026-07-23","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":"2610.13996","title":"Splicing Hints into Reasoning Traces: Learning from Demonstrator Failures","created":"2026-09-26","cited_by_count":0,"area":"lr"}],"next_cursor":null}