{"total":63,"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":"2510.01346","title":"Aristotle: IMO-level Automated Theorem Proving","created":"2025-10-01","cited_by_count":58,"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":"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":"2502.05567","title":"ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data","created":"2025-02-08","cited_by_count":23,"area":null},{"id":"2505.23486","title":"Autoformalization in the Era of Large Language Models: A Survey","created":"2025-05-29","cited_by_count":21,"area":null},{"id":"2502.05714","title":"Proving the Coding Interview: A Benchmark for Formally Verified Code Generation","created":"2025-02-08","cited_by_count":19,"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":"2511.03108","title":"miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forward","created":"2025-11-05","cited_by_count":14,"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":"2408.11172","title":"SubgoalXL: Subgoal-based Expert Learning for Theorem Proving","created":"2024-08-20","cited_by_count":11,"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":"2501.18310","title":"ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis","created":"2025-01-30","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":"2605.29548","title":"Why Larger Models Learn More: Effects of Capacity, Interference, and Rare-Task Retention","created":"2026-05-28","cited_by_count":10,"area":null},{"id":"2602.12966","title":"ProbeLLM: Automating Principled Diagnosis of LLM Failures","created":"2026-02-13","cited_by_count":9,"area":null},{"id":"2408.14158","title":"Fire-Flyer AI-HPC: A Cost-Effective Software-Hardware Co-Design for Deep Learning","created":"2024-08-26","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":"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":"2411.18872","title":"A Lean Dataset for International Math Olympiad: Small Steps towards Writing Math Proofs for Hard Problems","created":"2024-11-28","cited_by_count":6,"area":null},{"id":"2505.15740","title":"HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement","created":"2025-05-21","cited_by_count":6,"area":null},{"id":"2506.07477","title":"Premise Selection for a Lean Hammer","created":"2025-06-09","cited_by_count":6,"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.06393","title":"Conflict-Aware Fusion: Mitigating Logic Inertia in Large Language Models via Structured Cognitive Priors","created":"2025-12-06","cited_by_count":5,"area":null},{"id":"2608.28433","title":"Prove2Me: An Open Collaborative Platform for Scaling Math Formalization","created":"2026-08-28","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":"2606.26525","title":"Theory-Scale Auto-Formalization of Logics for Computer Science","created":"2026-06-25","cited_by_count":4,"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.04829","title":"Model-Based and Sample-Efficient AI-Assisted Math Discovery in Sphere Packing","created":"2025-12-04","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":"2503.09730","title":"Local Look-Ahead Guidance via Verifier-in-the-Loop for Automated Theorem Proving","created":"2025-03-12","cited_by_count":2,"area":null},{"id":"2505.04528","title":"Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving","created":"2025-05-07","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":"2606.19399","title":"VERITAS: Verifier-Guided Proof Search for Zero-Shot Formal Theorem Proving","created":"2026-06-17","cited_by_count":2,"area":null},{"id":"2608.20153","title":"FormalTCS: Benchmarking End-to-End Frontier Formal Theoretical Computer Science Research of Large Language Models","created":"2026-08-20","cited_by_count":2,"area":null},{"id":"2502.03321","title":"Simplifying Formal Proof-Generating Models with ChatGPT and Basic Searching Techniques","created":"2025-02-05","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":"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":"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":"2607.28632","title":"LLM Framework for Discovering Major Mathematical Conjectures: AI's Quest for the Next Riemann Hypothesis","created":"2026-04-19","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.11829","title":"Towards Autoformalization of LLM-generated Outputs for Requirement Verification","created":"2025-11-14","cited_by_count":0,"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":"2605.15219","title":"NOVA: Fundamental Limits of Knowledge Discovery Through AI","created":"2026-05-12","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.00618","title":"Efficient Test-time Inference for Generative Planning Models with OCL Search","created":"2026-05-30","cited_by_count":0,"area":null},{"id":"2606.25394","title":"FactorLibrary: From Polynomials to Circuits via Recursive Subgoals","created":"2026-06-24","cited_by_count":0,"area":null},{"id":"2609.09264","title":"StochBench: A Domain-Specific Benchmark for Stochastic Processes in Lean","created":"2026-09-08","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.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.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.11862","title":"LEVER: Adaptive Cost-Aware Proof Search Over AND/OR Graphs","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}