{"total":196,"rows":[{"id":"2303.18223","title":"A Survey of Large Language Models","created":"2023-03-31","cited_by_count":2576,"area":null},{"id":"2407.21787","title":"Large Language Monkeys: Scaling Inference Compute with Repeated Sampling","created":"2024-07-31","cited_by_count":991,"area":null},{"id":"2307.05782","title":"Large Language Models","created":"2023-07-11","cited_by_count":780,"area":null},{"id":"2210.12283","title":"Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs","created":"2022-10-21","cited_by_count":291,"area":null},{"id":"2205.12615","title":"Autoformalization with Large Language Models","created":"2022-05-25","cited_by_count":263,"area":null},{"id":"2205.11491","title":"HyperTree Proof Search for Neural Theorem Proving","created":"2022-05-23","cited_by_count":197,"area":null},{"id":"2302.12433","title":"ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics","created":"2023-02-24","cited_by_count":192,"area":null},{"id":"2407.11214","title":"PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition","created":"2024-07-15","cited_by_count":165,"area":null},{"id":"2202.01344","title":"Formal Mathematics Statement Curriculum Learning","created":"2022-02-03","cited_by_count":142,"area":null},{"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":"2406.03847","title":"Lean Workbook: A large-scale Lean problem set formalized from natural language math problems","created":"2024-06-06","cited_by_count":122,"area":null},{"id":"2303.04910","title":"Baldur: Whole-Proof Generation and Repair with Large Language Models","created":"2023-03-08","cited_by_count":119,"area":null},{"id":"2310.00656","title":"LEGO-Prover: Neural Theorem Proving with Growing Libraries","created":"2023-10-01","cited_by_count":109,"area":null},{"id":"2205.10893","title":"Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers","created":"2022-05-22","cited_by_count":98,"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":"2404.09939","title":"A Survey on Deep Learning for Theorem Proving","created":"2024-04-15","cited_by_count":57,"area":null},{"id":"2309.04295","title":"FIMO: A Challenge Formal Dataset for Automated Theorem Proving","created":"2023-09-08","cited_by_count":55,"area":null},{"id":"2406.18321","title":"MathOdyssey: Benchmarking Mathematical Problem-Solving Skills in Large Language Models Using Odyssey Math Data","created":"2024-06-26","cited_by_count":52,"area":null},{"id":"2303.04488","title":"Magnushammer: A Transformer-Based Approach to Premise Selection","created":"2023-03-08","cited_by_count":50,"area":null},{"id":"2407.00695","title":"Learning Formal Mathematics From Intrinsic Motivation","created":"2024-06-30","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":"2408.03350","title":"miniCTX: Neural Theorem Proving with (Long-)Contexts","created":"2024-08-05","cited_by_count":37,"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":"2506.21621","title":"The Open Proof Corpus: A Large-Scale Study of LLM-Generated Mathematical Proofs","created":"2025-06-23","cited_by_count":30,"area":null},{"id":"2505.13938","title":"CLEVER: A Curated Benchmark for Formally Verified Code Generation","created":"2025-05-20","cited_by_count":29,"area":null},{"id":"2509.16865","title":"Large Language Models as End-to-end Combinatorial Optimization Solvers","created":"2025-09-21","cited_by_count":28,"area":null},{"id":"2310.18021","title":"FormalGeo: An Extensible Formalized Framework for Olympiad Geometric Problem Solving","created":"2023-10-27","cited_by_count":27,"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":"2405.14414","title":"Proving Theorems Recursively","created":"2024-05-23","cited_by_count":26,"area":null},{"id":"2309.15806","title":"Lyra: Orchestrating Dual Correction in Automated Theorem Proving","created":"2023-09-27","cited_by_count":25,"area":null},{"id":"2312.07622","title":"Mathematical Language Models: A Survey","created":"2023-12-12","cited_by_count":24,"area":null},{"id":"2409.18433","title":"Easy2Hard-Bench: Standardized Difficulty Labels for Profiling LLM Performance and Generalization","created":"2024-09-27","cited_by_count":24,"area":null},{"id":"2410.10135","title":"FormalAlign: Automated Alignment Evaluation for Autoformalization","created":"2024-10-14","cited_by_count":24,"area":null},{"id":"2412.03205","title":"U-MATH: A University-Level Benchmark for Evaluating Mathematical Skills in LLMs","created":"2024-12-04","cited_by_count":24,"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":"2211.07524","title":"Towards a Mathematics Formalisation Assistant using Large Language Models","created":"2022-11-14","cited_by_count":22,"area":null},{"id":"2406.14408","title":"FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving","created":"2024-06-20","cited_by_count":22,"area":null},{"id":"2409.14274","title":"Proof Automation with Large Language Models","created":"2024-09-22","cited_by_count":22,"area":null},{"id":"2502.12065","title":"Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitions","created":"2025-02-17","cited_by_count":22,"area":null},{"id":"2410.04194","title":"Consistent Autoformalization for Constructing Mathematical Libraries","created":"2024-10-05","cited_by_count":21,"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":"2406.14219","title":"Proving Olympiad Algebraic Inequalities without Human Demonstrations","created":"2024-06-20","cited_by_count":20,"area":null},{"id":"2406.11915","title":"miniCodeProps: a Minimal Benchmark for Proving Code Properties","created":"2024-06-16","cited_by_count":18,"area":null},{"id":"2410.16429","title":"Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4","created":"2024-10-21","cited_by_count":18,"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":"2602.17016","title":"M2F: Automated Formalization of Mathematical Literature at Scale","created":"2026-02-19","cited_by_count":15,"area":null},{"id":"2402.17205","title":"Measuring Vision-Language STEM Skills of Neural Models","created":"2024-02-27","cited_by_count":14,"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":"2509.26076","title":"IMProofBench: Benchmarking AI on Research-Level Mathematical Proof Generation","created":"2025-09-30","cited_by_count":13,"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":"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":"2310.07957","title":"A New Approach Towards Autoformalization","created":"2023-10-12","cited_by_count":10,"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.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":"2205.15231","title":"A Survey in Mathematical Language Processing","created":"2022-05-30","cited_by_count":9,"area":null},{"id":"2508.18914","title":"FormaRL: Enhancing Autoformalization with no Labeled Data","created":"2025-08-26","cited_by_count":9,"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":"2503.01424","title":"From Hypothesis to Publication: A Comprehensive Survey of AI-Driven Research Support Systems","created":"2025-03-03","cited_by_count":8,"area":null},{"id":"2506.21545","title":"Data Efficacy for Language Model Training","created":"2025-06-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":"2510.25427","title":"RLMEval: Evaluating Research-Level Neural Theorem Proving","created":"2025-10-29","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.06802","title":"Riemann-Bench: A Benchmark for Moonshot Mathematics","created":"2026-04-08","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":"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":"2410.11133","title":"3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes","created":"2024-10-14","cited_by_count":6,"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":"2603.12744","title":"TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib?","created":"2026-03-13","cited_by_count":6,"area":null},{"id":"2606.16541","title":"The Faithfulness Gap: Certifying Semantic Equivalence Between Natural-Language and Formal Mathematical Statements","created":"2026-06-15","cited_by_count":6,"area":null},{"id":"2503.04763","title":"MiniF2F in Rocq: Automatic Translation Between Proof Assistants -- A Case Study","created":"2025-02-11","cited_by_count":5,"area":null},{"id":"2504.17017","title":"Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification","created":"2025-04-23","cited_by_count":5,"area":null},{"id":"2505.23851","title":"ASyMOB: Algebraic Symbolic Mathematical Operations Benchmark","created":"2025-05-28","cited_by_count":5,"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":"2606.25363","title":"TheoremGraph: Bridging Formal and Informal Mathematics","created":"2026-06-24","cited_by_count":5,"area":null},{"id":"2311.07618","title":"Large Language Models' Understanding of Math: Source Criticism and Extrapolation","created":"2023-11-12","cited_by_count":4,"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":"2501.13959","title":"Learning an Effective Premise Retrieval Model for Efficient Mathematical Formalization","created":"2025-01-21","cited_by_count":4,"area":null},{"id":"2502.15507","title":"Steering LLMs for Formal Theorem Proving","created":"2025-02-21","cited_by_count":4,"area":null},{"id":"2502.15795","title":"Lean-ing on Quality: How High-Quality Data Beats Diverse Multilingual Data in AutoFormalization","created":"2025-02-18","cited_by_count":4,"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":"2601.18944","title":"Neural Theorem Proving for Verification Conditions: A Real-World Benchmark","created":"2026-01-26","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":"2606.26525","title":"Theory-Scale Auto-Formalization of Logics for Computer Science","created":"2026-06-25","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":"2501.15797","title":"LemmaHead: RAG Assisted Proof Generation Using Large Language Models","created":"2025-01-27","cited_by_count":3,"area":null},{"id":"2503.04772","title":"Generating Millions Of Lean Theorems With Proofs By Exploring State Transition Graphs","created":"2025-02-16","cited_by_count":3,"area":null},{"id":"2506.23924","title":"Performance of LLMs on Stochastic Modeling Operations Research Problems: From Theory to Practice","created":"2025-06-30","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":"2508.18587","title":"A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants","created":"2025-08-26","cited_by_count":3,"area":null}],"next_cursor":"100"}