{"total":42,"rows":[{"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":"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":"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":"2605.29955","title":"Formalizing Mathematics at Scale","created":"2026-05-28","cited_by_count":10,"area":null},{"id":"2603.15929","title":"Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium","created":"2026-03-16","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":"2603.02668","title":"SorryDB: Can AI Provers Complete Real-World Lean Theorems?","created":"2026-03-03","cited_by_count":8,"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":"2511.11500","title":"Honesty over Accuracy: Trustworthy Language Models through Reinforced Hesitation","created":"2025-11-14","cited_by_count":5,"area":null},{"id":"2606.26442","title":"AXLE: A Cloud Infrastructure for Lean 4 Theorem Proving Utilities","created":"2026-06-24","cited_by_count":5,"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":"2509.24827","title":"Putnam-like dataset summary: LLMs as mathematical competition contestants","created":"2025-09-29","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":"2510.12829","title":"Mathematics with large language models as provers and verifiers","created":"2025-10-11","cited_by_count":1,"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":"2603.03352","title":"Perfect score on IPhO 2025 theory by Gemini agent","created":"2026-02-26","cited_by_count":1,"area":null},{"id":"2603.04528","title":"Discovering mathematical concepts through a multi-agent system","created":"2026-03-04","cited_by_count":1,"area":null},{"id":"2605.19063","title":"Mapping Uncharted Symmetries: Machine Discovery in Combinatorics","created":"2026-05-18","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":"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":"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":"2601.16172","title":"Inference-Time Diversity in RL-Trained Lean Theorem Provers: A Diagnostic Study","created":"2026-01-22","cited_by_count":0,"area":null},{"id":"2603.20405","title":"Putnam 2025 Problems in Rocq using Opus 4.6 and Rocq-MCP","created":"2026-03-20","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.06184","title":"Teaching LLMs Program Semantics via Symbolic Execution Traces","created":"2026-05-07","cited_by_count":0,"area":null},{"id":"2606.04273","title":"Human agency in initial human-AI proof formalization workflows","created":"2026-06-02","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.14585","title":"Euclid-Omni : A Unified Neuro-Symbolic Framework for Plane Geometry","created":"2026-06-17","cited_by_count":0,"area":null},{"id":"2608.26310","title":"FaithSieve: Fine-Grained Evaluation of Math Proofs with Faithful Formal Evidence","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.35790","title":"Sage: Formalization with Semantic Correction","created":"2026-09-16","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.13461","title":"SqueezeBench: Saturation-Resilient Evaluation of Mathematical Capability","created":"2026-10-09","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},{"id":"2610.18089","title":"One-Sided Verification Under Limited Expert Review","created":"2026-10-13","cited_by_count":0,"area":null}],"next_cursor":null}