{"total":79,"rows":[{"id":"2503.09567","title":"Towards Reasoning Era: A Survey of Long Chain-of-Thought for Reasoning Large Language Models","created":"2025-03-12","cited_by_count":384,"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":"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":"2507.23726","title":"Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving","created":"2025-07-31","cited_by_count":101,"area":"lr"},{"id":"2503.09501","title":"ReMA: Learning to Meta-think for LLMs with Multi-Agent Reinforcement Learning","created":"2025-03-12","cited_by_count":79,"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":"2506.01716","title":"Self-Challenging Language Model Agents","created":"2025-06-02","cited_by_count":59,"area":"agents"},{"id":"2505.23614","title":"Inference-time Scaling of Diffusion Models through Classical Search","created":"2025-05-29","cited_by_count":49,"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":"2505.05758","title":"APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning","created":"2025-05-09","cited_by_count":35,"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":"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.06122","title":"Leanabell-Prover: Posttraining Scaling in Formal Reasoning","created":"2025-04-08","cited_by_count":27,"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":"2602.06176","title":"Large Language Model Reasoning Failures","created":"2026-02-05","cited_by_count":21,"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.15681","title":"ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings","created":"2025-10-17","cited_by_count":18,"area":"rag"},{"id":"2602.24273","title":"A Minimal Agent for Automated Theorem Proving","created":"2026-02-27","cited_by_count":18,"area":"agents"},{"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":"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":"2507.02726","title":"Bourbaki: Self-Generated and Goal-Conditioned MDPs for Theorem Proving","created":"2025-07-03","cited_by_count":12,"area":"synth"},{"id":"2602.09464","title":"AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms","created":"2026-02-10","cited_by_count":12,"area":null},{"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":"2508.21107","title":"Learning to Generate Unit Test via Adversarial Reinforcement Learning","created":"2025-08-28","cited_by_count":11,"area":"lr"},{"id":"2504.02181","title":"A Survey of Scaling in Large Language Model Reasoning","created":"2025-04-02","cited_by_count":10,"area":"lr"},{"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.24193","title":"AceSearcher: Bootstrapping Reasoning and Search for LLMs via Reinforced Self-Play","created":"2025-09-29","cited_by_count":10,"area":"lr"},{"id":"2604.20209","title":"Scaling Self-Play with Self-Guidance","created":"2026-04-22","cited_by_count":10,"area":"synth"},{"id":"2511.13027","title":"Scaling Generative Verifiers For Natural Language Mathematical Proof Verification And Selection","created":"2025-11-17","cited_by_count":9,"area":null},{"id":"2608.05179","title":"Autonomous Research Agents: A Survey of AI Scientists and the Verification Gap","created":"2026-06-29","cited_by_count":9,"area":"agents"},{"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.06499","title":"SPARQ: Synthetic Problem Generation for Reasoning via Quality-Diversity Algorithms","created":"2025-06-06","cited_by_count":7,"area":"lr"},{"id":"2510.00732","title":"EvolProver: Advancing Automated Theorem Proving by Evolving Formalized Problems via Symmetry and Difficulty","created":"2025-10-01","cited_by_count":7,"area":null},{"id":"2603.21065","title":"LongCat-Flash-Prover: Advancing Native Formal Reasoning via Agentic Tool-Integrated Reinforcement Learning","created":"2026-03-22","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":"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":"2603.12744","title":"TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib?","created":"2026-03-13","cited_by_count":6,"area":null},{"id":"2510.20342","title":"Teaching Language Models to Reason with Tools","created":"2025-10-23","cited_by_count":5,"area":"lr"},{"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":"2603.19514","title":"Learning to Disprove: Formal Counterexample Generation with Large Language Models","created":"2026-03-19","cited_by_count":5,"area":"lr"},{"id":"2604.26311","title":"DreamProver: Evolving Transferable Lemma Libraries via a Wake-Sleep Theorem-Proving Agent","created":"2026-04-29","cited_by_count":5,"area":"agents"},{"id":"2603.15957","title":"GASP: Guided Asymmetric Self-Play For Coding LLMs","created":"2026-03-16","cited_by_count":4,"area":"synth"},{"id":"2605.23109","title":"Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems","created":"2026-05-22","cited_by_count":4,"area":null},{"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":"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":"2601.15737","title":"PhysProver: Advancing Automatic Theorem Proving for Physics","created":"2026-01-22","cited_by_count":3,"area":null},{"id":"2603.24202","title":"A Deep Dive into Scaling RL for Code Generation with Synthetic Data and Curricula","created":"2026-03-25","cited_by_count":3,"area":"synth"},{"id":"2605.30333","title":"COMPOSE: Composing Future Theorems from Citations and Formal Structure","created":"2026-05-28","cited_by_count":3,"area":null},{"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":"2509.14274","title":"Discovering New Theorems via LLMs with In-Context Proof Learning in Lean","created":"2025-09-16","cited_by_count":2,"area":null},{"id":"2511.14778","title":"Learning Interestingness in Automated Mathematical Theory Formation","created":"2025-11-05","cited_by_count":2,"area":null},{"id":"2603.03524","title":"Test-Time Meta-Adaptation with Self-Synthesis","created":"2026-03-03","cited_by_count":2,"area":null},{"id":"2608.16977","title":"The Problem Is the Problem: Towards Scalable Mathematical Discovery","created":"2026-08-17","cited_by_count":2,"area":null},{"id":"2504.19188","title":"Hierarchical Attention Generates Better Proofs","created":"2025-04-27","cited_by_count":1,"area":null},{"id":"2505.03818","title":"Program Semantic Inequivalence Game with Large Language Models","created":"2025-05-02","cited_by_count":1,"area":null},{"id":"2505.12031","title":"LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation","created":"2025-05-17","cited_by_count":1,"area":"synth"},{"id":"2511.13043","title":"Spark-Prover-X1: Formal Theorem Proving Through Diverse Data Training","created":"2025-11-17","cited_by_count":1,"area":null},{"id":"2606.01861","title":"A Theoretical Framework for Self-Play Theorem Proving Algorithms","created":"2026-06-01","cited_by_count":1,"area":"synth"},{"id":"2606.26454","title":"Data-driven Machine Learning Cannot Reach Symbolic-level Logical Reasoning -- The Limit of the Scaling Law","created":"2026-06-24","cited_by_count":1,"area":"lr"},{"id":"2607.04631","title":"Formal Disco: Scalable Open-Ended Generation of Formally Verified Programs","created":"2026-07-06","cited_by_count":1,"area":null},{"id":"2607.07779","title":"From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier","created":"2026-07-08","cited_by_count":1,"area":null},{"id":"2607.16372","title":"AoA: Theorem Proving Agent over Abstract Syntax Tree of Redesigned Language","created":"2026-07-17","cited_by_count":1,"area":"agents"},{"id":"2607.27709","title":"MECA: A Mechanism-Centered Agent for Constructing Well-Specified and Valuable Mathematical Conjectures","created":"2026-07-30","cited_by_count":1,"area":null},{"id":"2608.28639","title":"Reward-Oracle MCTS for Formal Theorem Proving: Sample-Efficient Search and the Need for Kernel-Level Proof Auditing","created":"2026-08-11","cited_by_count":1,"area":null},{"id":"2609.25438","title":"PermuFormer: Multi-Task Pretraining for Permutation Representation in Algebraic Combinatorics","created":"2026-09-21","cited_by_count":1,"area":null},{"id":"2609.30063","title":"Self-Play Pretraining with Zero Data","created":"2026-09-24","cited_by_count":1,"area":"synth"},{"id":"2609.37633","title":"RLTL;DR: Self-improvement by Internalizing Self-generated Feedback","created":"2026-09-29","cited_by_count":1,"area":null},{"id":"2602.17831","title":"The Token Games: Evaluating Language Model Reasoning with Puzzle Duels","created":"2026-02-19","cited_by_count":0,"area":"lr"},{"id":"2604.27644","title":"ANCORA: Learning to Question via Manifold-Anchored Self-Play for Verifiable Reasoning","created":"2026-04-30","cited_by_count":0,"area":null},{"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.17278","title":"A2RBench: An Automatic Paradigm for Formally Verifiable Abstract Reasoning Benchmark Generation","created":"2026-05-17","cited_by_count":0,"area":"lr"},{"id":"2606.17581","title":"Visored: A Controlled-Natural-Language Prover for LLM-Generated Mathematics","created":"2026-06-16","cited_by_count":0,"area":null},{"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":"2606.28747","title":"Self-Supervised Theorem Discovery in a Formal Axiomatic System","created":"2026-06-27","cited_by_count":0,"area":"lr"},{"id":"2609.32228","title":"CompassPlay: Rewarding the Proposer for Where It Moves the Solver","created":"2026-09-26","cited_by_count":0,"area":null},{"id":"2609.32264","title":"LANTERN: Illuminating Hidden Mathematical Knowledge in Language Models","created":"2026-09-26","cited_by_count":0,"area":null},{"id":"2609.34460","title":"When Does Structured Knowledge Help Neural Theorem Proving?","created":"2026-09-28","cited_by_count":0,"area":null},{"id":"2609.37356","title":"Teaching LLMs to Generate Challenging MILP Instances via Solver Feedback","created":"2026-09-29","cited_by_count":0,"area":null}],"next_cursor":null}