{"total":65,"rows":[{"id":"2502.07640","title":"Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving","created":"2025-02-11","cited_by_count":133,"area":null},{"id":"2502.03438","title":"BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving","created":"2025-02-05","cited_by_count":84,"area":null},{"id":"2505.11792","title":"Solver-Informed RL: Grounding Large Language Models for Authentic Optimization Modeling","created":"2025-05-17","cited_by_count":45,"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":"2410.15700","title":"InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Search","created":"2024-10-21","cited_by_count":34,"area":null},{"id":"2406.07222","title":"Reliable Evaluation and Benchmarks for Statement Autoformalization","created":"2024-06-11","cited_by_count":32,"area":null},{"id":"2502.05567","title":"ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data","created":"2025-02-08","cited_by_count":23,"area":null},{"id":"2509.21016","title":"RL Grokking Recipe: How Does RL Unlock and Transfer New Algorithms in LLMs?","created":"2025-09-25","cited_by_count":23,"area":null},{"id":"2506.07047","title":"Mathesis: Towards Formal Theorem Proving from Natural Languages","created":"2025-06-08","cited_by_count":18,"area":null},{"id":"2506.11085","title":"LeanExplore: A search engine for Lean 4 declarations","created":"2025-06-04","cited_by_count":18,"area":null},{"id":"2602.17016","title":"M2F: Automated Formalization of Mathematical Literature at Scale","created":"2026-02-19","cited_by_count":15,"area":null},{"id":"2507.07399","title":"Generalized Tree Edit Distance (GTED): A Faithful Evaluation Metric for Statement Autoformalization","created":"2025-07-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":"2412.15184","title":"Data for Mathematical Copilots: Better Ways of Presenting Proofs for Machine Learning","created":"2024-12-19","cited_by_count":11,"area":null},{"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.22246","title":"ASSESS: A Semantic and Structural Evaluation Framework for Statement Similarity","created":"2025-09-26","cited_by_count":10,"area":null},{"id":"2602.24173","title":"LemmaBench: A Live, Research-Level Benchmark to Evaluate LLM Capabilities in Mathematics","created":"2026-02-27","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":"2606.31002","title":"Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization","created":"2026-06-30","cited_by_count":10,"area":null},{"id":"2408.14915","title":"Can Transformers Do Enumerative Geometry?","created":"2024-08-27","cited_by_count":8,"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":"2604.03071","title":"Automatic Textbook Formalization","created":"2026-04-03","cited_by_count":8,"area":null},{"id":"2604.25031","title":"Faithful Autoformalization via Roundtrip Verification and Repair","created":"2026-04-27","cited_by_count":8,"area":null},{"id":"2412.17743","title":"YuLan-Mini: An Open Data-efficient Language Model","created":"2024-12-23","cited_by_count":7,"area":null},{"id":"2509.09810","title":"Towards a Common Framework for Autoformalization","created":"2025-09-11","cited_by_count":7,"area":null},{"id":"2510.06296","title":"VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code","created":"2025-10-07","cited_by_count":7,"area":null},{"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.26094","title":"Lean4Physics: Comprehensive Reasoning Framework for College-level Physics in Lean4","created":"2025-10-30","cited_by_count":5,"area":null},{"id":"2603.26996","title":"FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?","created":"2026-03-27","cited_by_count":5,"area":null},{"id":"2410.15748","title":"Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation","created":"2024-10-21","cited_by_count":4,"area":null},{"id":"2506.08321","title":"LeanTutor: Towards a Verified AI Mathematical Proof Tutor","created":"2025-06-10","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":"2502.11167","title":"SURGE: On the Potential of Large Language Models as General-Purpose Surrogate Code Executors","created":"2025-02-16","cited_by_count":3,"area":null},{"id":"2507.14722","title":"LeanTree: Accelerating White-Box Proof Search with Factorized States in Lean 4","created":"2025-07-19","cited_by_count":3,"area":null},{"id":"2512.10317","title":"Translating Informal Proofs into Formal Proofs Using a Chain of States","created":"2025-12-11","cited_by_count":3,"area":null},{"id":"2607.13292","title":"Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases","created":"2026-07-14","cited_by_count":3,"area":null},{"id":"2504.19188","title":"Hierarchical Attention Generates Better Proofs","created":"2025-04-27","cited_by_count":1,"area":null},{"id":"2506.02565","title":"Towards Generating Controllable and Solvable Geometry Problem by Leveraging Symbolic Deduction Engine","created":"2025-06-03","cited_by_count":1,"area":null},{"id":"2507.08665","title":"KELPS: A Framework for Verified Multi-Language Autoformalization via Semantic-Syntactic Alignment","created":"2025-07-11","cited_by_count":1,"area":null},{"id":"2508.17200","title":"Large Language Model-Based Automatic Formulation for Stochastic Optimization Models","created":"2025-08-24","cited_by_count":1,"area":null},{"id":"2512.00097","title":"Gold-Medal-Level Olympiad Geometry Solving with Efficient Heuristic Auxiliary Constructions","created":"2025-11-27","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":"2604.23698","title":"Benchmarking Testing in Automated Theorem Proving","created":"2026-04-26","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":"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.19374","title":"Euclean: Automated Geometry Problem Formalization with Unified Verification in Lean","created":"2026-06-17","cited_by_count":1,"area":null},{"id":"2601.17473","title":"LeanTutor: Towards a Verified AI Mathematical Proof Tutor","created":"2026-01-24","cited_by_count":0,"area":null},{"id":"2606.00981","title":"Robust Asynchronous Planning via Auto-Formalization","created":"2026-05-31","cited_by_count":0,"area":null},{"id":"2606.01008","title":"FVSpec: Real-World Property-Based Tests as Lean Challenges","created":"2026-05-31","cited_by_count":0,"area":null},{"id":"2606.02588","title":"Lean-GAP: A Dataset of Formalized Graduate Algebra Problems","created":"2026-05-20","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.14867","title":"Evaluating the Robustness of Proof Autoformalization in Lean 4","created":"2026-06-12","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.26334","title":"ProofEvolve: Neuro-Symbolic Evolution for Formal Automated Theorem Proving","created":"2026-08-26","cited_by_count":0,"area":null},{"id":"2609.28603","title":"Learning to Discover Interesting Mathematics","created":"2026-09-23","cited_by_count":0,"area":null},{"id":"2609.35606","title":"TCSAlgBench: Benchmarking Automated Proving for Research-Level Theoretical Computer Science","created":"2026-09-28","cited_by_count":0,"area":null},{"id":"2609.38384","title":"LeanPolish: Verified Supervision for Lean Proof Compression","created":"2026-09-29","cited_by_count":0,"area":null},{"id":"2610.08319","title":"SCOPE: Certified Theorem Proving with a Language Model as the Policy Planner","created":"2026-10-06","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.13461","title":"SqueezeBench: Saturation-Resilient Evaluation of Mathematical Capability","created":"2026-10-09","cited_by_count":0,"area":null},{"id":"2610.17358","title":"claimcheck: Measuring and Improving Specification Faithfulness","created":"2026-10-12","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.18498","title":"Aligning Faithfulness for Theory-Scale Autoformalization","created":"2026-10-13","cited_by_count":0,"area":null}],"next_cursor":null}