{"total":65,"rows":[{"id":"2511.10507","title":"AdvancedIF: Rubric-Based Benchmarking and Reinforcement Learning for Advancing LLM Instruction Following","created":"2025-11-13","cited_by_count":51,"area":null},{"id":"2512.17260","title":"Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience","created":"2025-12-19","cited_by_count":44,"area":null},{"id":"2511.02872","title":"FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levels","created":"2025-11-04","cited_by_count":27,"area":null},{"id":"2510.15981","title":"ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization","created":"2025-10-13","cited_by_count":21,"area":null},{"id":"2605.08678","title":"MLS-Bench: A Holistic and Rigorous Assessment of AI Systems on Building Better AI","created":"2026-05-09","cited_by_count":17,"area":null},{"id":"2509.26076","title":"IMProofBench: Benchmarking AI on Research-Level Mathematical Proof Generation","created":"2025-09-30","cited_by_count":13,"area":null},{"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":"2606.05400","title":"LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization","created":"2026-06-03","cited_by_count":12,"area":null},{"id":"2603.19329","title":"Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification","created":"2026-03-18","cited_by_count":11,"area":null},{"id":"2509.22246","title":"ASSESS: A Semantic and Structural Evaluation Framework for Statement Similarity","created":"2025-09-26","cited_by_count":10,"area":null},{"id":"2605.13171","title":"Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics","created":"2026-05-13","cited_by_count":10,"area":null},{"id":"2606.31002","title":"Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization","created":"2026-06-30","cited_by_count":10,"area":null},{"id":"2606.29493","title":"Faults in Our Formal Benchmarking: Dataset Defects and Evaluation Failures in Lean Theorem Proving","created":"2026-06-28","cited_by_count":9,"area":null},{"id":"2510.10815","title":"DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems","created":"2025-10-12","cited_by_count":8,"area":null},{"id":"2510.15940","title":"Lean Finder: Semantic Search for Mathlib That Understands User Intents","created":"2025-10-08","cited_by_count":8,"area":null},{"id":"2602.18307","title":"VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Lean","created":"2026-02-20","cited_by_count":8,"area":null},{"id":"2603.02668","title":"SorryDB: Can AI Provers Complete Real-World Lean Theorems?","created":"2026-03-03","cited_by_count":8,"area":null},{"id":"2604.03071","title":"Automatic Textbook Formalization","created":"2026-04-03","cited_by_count":8,"area":null},{"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":"2510.06857","title":"Autoformalizer with Tool Feedback","created":"2025-10-08","cited_by_count":7,"area":null},{"id":"2510.02335","title":"FormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theory","created":"2025-09-26","cited_by_count":5,"area":null},{"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":"2512.24796","title":"LeanCat: A Benchmark Suite for Formal Category Theory in Lean (Part I: 1-Categories)","created":"2025-12-31","cited_by_count":4,"area":null},{"id":"2605.14061","title":"MathAtlas: A Benchmark for Autoformalization in the Wild","created":"2026-05-13","cited_by_count":4,"area":null},{"id":"2608.29270","title":"SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization","created":"2026-08-29","cited_by_count":4,"area":null},{"id":"2601.15737","title":"PhysProver: Advancing Automatic Theorem Proving for Physics","created":"2026-01-22","cited_by_count":3,"area":null},{"id":"2605.10379","title":"Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness","created":"2026-05-11","cited_by_count":3,"area":null},{"id":"2606.05632","title":"Evaluation of LLMs for Mathematical Formalization in Lean","created":"2026-06-04","cited_by_count":3,"area":null},{"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.21056","title":"Bilevel Data Curation for LLM Fine-tuning: Offline Selection and Online Self-Refining Generation","created":"2025-11-26","cited_by_count":2,"area":null},{"id":"2512.18256","title":"MSC-180: A Benchmark for Automated Formal Theorem Proving from Mathematical Subject Classification","created":"2025-12-20","cited_by_count":2,"area":null},{"id":"2601.22365","title":"Towards Solving the Gilbert-Pollak Conjecture via Large Language Models","created":"2026-01-29","cited_by_count":2,"area":null},{"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":"2512.14252","title":"G\\\"odel's Poetry","created":"2025-12-16","cited_by_count":1,"area":null},{"id":"2601.15714","title":"Even GPT-5.2 Can't Count to Five: The Case for Zero-Error Horizons in Trustworthy LLMs","created":"2026-01-22","cited_by_count":1,"area":null},{"id":"2601.23166","title":"Monotonic Reference-Free Refinement for Autoformalization","created":"2026-01-30","cited_by_count":1,"area":null},{"id":"2603.14147","title":"An Alternative Trajectory for Generative AI","created":"2026-03-14","cited_by_count":1,"area":null},{"id":"2603.19828","title":"FormalEvolve: Neuro-Symbolic Evolutionary Search for Diverse Autoformalization","created":"2026-03-20","cited_by_count":1,"area":null},{"id":"2604.23698","title":"Benchmarking Testing in Automated Theorem Proving","created":"2026-04-26","cited_by_count":1,"area":null},{"id":"2604.23712","title":"OptProver: Bridging Olympiad and Optimization through Continual Training in Formal Theorem Proving","created":"2026-04-26","cited_by_count":1,"area":null},{"id":"2605.22257","title":"What are the Right Symmetries for Formal Theorem Proving?","created":"2026-05-21","cited_by_count":1,"area":null},{"id":"2606.09450","title":"TheoremBench: Evaluating LLMs on Theorem Proving in Formal Mathematics","created":"2026-06-08","cited_by_count":1,"area":null},{"id":"2606.13782","title":"MA-ProofBench: A Two-Tiered Evaluation of LLMs for Theorem Proving in Mathematical Analysis","created":"2026-06-11","cited_by_count":1,"area":null},{"id":"2606.17289","title":"Nothing from Something: Can a Language Model Discover 0?","created":"2026-06-15","cited_by_count":1,"area":null},{"id":"2606.20642","title":"Hypothesis-Disciplined Multi-Agent Automated Formalization of Asymptotic Statistical Theory","created":"2026-06-03","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.14582","title":"MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Research","created":"2026-07-16","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.05157","title":"AxQM: A Textbook-Scale Benchmark for Formal Proof Synthesis in a Library of Finite-Dimensional Quantum Mechanics","created":"2026-09-04","cited_by_count":1,"area":null},{"id":"2511.15259","title":"Efficiency Will Not Lead to Sustainable Reasoning AI","created":"2025-11-19","cited_by_count":0,"area":null},{"id":"2605.04472","title":"Automated Formal Proofs of Combinatorial Identities via Wilf-Zeilberger Guidance and LLMs","created":"2026-05-06","cited_by_count":0,"area":null},{"id":"2605.22885","title":"ImProver 2: Iteratively Self-Improving LMs for Neurosymbolic Proof Optimization","created":"2026-05-21","cited_by_count":0,"area":null},{"id":"2605.28512","title":"On Compositional Learning Behaviours in Formal Mathematics","created":"2026-05-27","cited_by_count":0,"area":null},{"id":"2606.14867","title":"Evaluating the Robustness of Proof Autoformalization in Lean 4","created":"2026-06-12","cited_by_count":0,"area":null},{"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":"2608.14221","title":"MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement","created":"2026-08-14","cited_by_count":0,"area":null},{"id":"2608.18084","title":"Compiler-Guided Adaptive Proof Search with Cross-Model Synergy on Context-Dependent Theorem Proving","created":"2026-06-04","cited_by_count":0,"area":null},{"id":"2608.26334","title":"ProofEvolve: Neuro-Symbolic Evolution for Formal Automated Theorem Proving","created":"2026-08-26","cited_by_count":0,"area":null},{"id":"2609.10712","title":"An Open Recipe for IMO Gold: Training Nemotron for Olympiad Mathematics","created":"2026-09-09","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.39228","title":"Fyan: A Human--AI Harness with Semantic Auditing for Document-Level Formalization","created":"2026-09-30","cited_by_count":0,"area":null},{"id":"2610.11605","title":"NanoProof: Open and Efficient Automated Theorem Proving in Lean 4","created":"2026-10-08","cited_by_count":0,"area":null},{"id":"2610.11862","title":"LEVER: Adaptive Cost-Aware Proof Search Over AND/OR Graphs","created":"2026-10-08","cited_by_count":0,"area":null},{"id":"2610.12659","title":"MagicBeanStalk: Escaping the RLVR Zero Advantage Trap with Recursive Data Synthesis","created":"2026-10-08","cited_by_count":0,"area":null},{"id":"2610.17697","title":"LeanPRM: Lean-Grounded Process Supervision for Natural Language Proof Verification","created":"2026-10-13","cited_by_count":0,"area":null}],"next_cursor":null}