{"total":114,"rows":[{"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":"2209.00626","title":"The Alignment Problem from a Deep Learning Perspective","created":"2022-08-30","cited_by_count":258,"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":"2406.16838","title":"From Decoding to Meta-Generation: Inference-time Algorithms for Large Language Models","created":"2024-06-24","cited_by_count":137,"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":"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":"2404.12534","title":"Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean","created":"2024-04-18","cited_by_count":58,"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":"2406.08467","title":"DafnyBench: A Benchmark for Formal Software Verification","created":"2024-06-12","cited_by_count":57,"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":"2310.02227","title":"SNIP: Bridging Mathematical Symbolic and Numeric Realms with Unified Pre-training","created":"2023-10-03","cited_by_count":47,"area":null},{"id":"2407.00695","title":"Learning Formal Mathematics From Intrinsic Motivation","created":"2024-06-30","cited_by_count":45,"area":null},{"id":"2302.11223","title":"Deep Generative Symbolic Regression with Monte-Carlo-Tree-Search","created":"2023-02-22","cited_by_count":41,"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":"2309.01933","title":"Provably safe systems: the only path to controllable AGI","created":"2023-09-05","cited_by_count":29,"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":"2310.18021","title":"FormalGeo: An Extensible Formalized Framework for Olympiad Geometric Problem Solving","created":"2023-10-27","cited_by_count":27,"area":null},{"id":"2405.17216","title":"Autoformalizing Euclidean Geometry","created":"2024-05-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":"2211.07524","title":"Towards a Mathematics Formalisation Assistant using Large Language Models","created":"2022-11-14","cited_by_count":22,"area":null},{"id":"2405.01787","title":"Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming","created":"2024-05-03","cited_by_count":20,"area":null},{"id":"2406.14219","title":"Proving Olympiad Algebraic Inequalities without Human Demonstrations","created":"2024-06-20","cited_by_count":20,"area":null},{"id":"2405.16674","title":"Limits of Deep Learning: Sequence Modeling through the Lens of Complexity Theory","created":"2024-05-26","cited_by_count":19,"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":"2401.02949","title":"Graph2Tac: Online Representation Learning of Formal Math Concepts","created":"2024-01-05","cited_by_count":15,"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":"2402.13321","title":"Rigor with Machine Learning from Field Theory to the Poincar\\'e Conjecture","created":"2024-02-20","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":"2404.07382","title":"Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving","created":"2024-04-10","cited_by_count":11,"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":"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":"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":"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.29955","title":"Formalizing Mathematics at Scale","created":"2026-05-28","cited_by_count":10,"area":null},{"id":"2307.13453","title":"Monte-Carlo Tree Search for Multi-Agent Pathfinding: Preliminary Results","created":"2023-07-25","cited_by_count":9,"area":null},{"id":"2311.03583","title":"Finding Increasingly Large Extremal Graphs with AlphaZero and Tabu Search","created":"2023-11-06","cited_by_count":8,"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":"2602.18307","title":"VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Lean","created":"2026-02-20","cited_by_count":8,"area":null},{"id":"2408.10268","title":"Generating Streamlining Constraints with Large Language Models","created":"2024-08-16","cited_by_count":7,"area":null},{"id":"2405.06677","title":"ATG: Benchmarking Automated Theorem Generation for Generative Language Models","created":"2024-05-05","cited_by_count":6,"area":null},{"id":"2408.04720","title":"Learning the Simplicity of Scattering Amplitudes","created":"2024-08-08","cited_by_count":6,"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":"2506.07477","title":"Premise Selection for a Lean Hammer","created":"2025-06-09","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":"2304.10486","title":"CoProver: A Recommender System for Proof Construction","created":"2023-03-01","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":"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":"2311.07178","title":"Game Solving with Online Fine-Tuning","created":"2023-11-13","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":"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":"2312.14188","title":"Enhancing Neural Theorem Proving through Data Augmentation and Dynamic Sampling Method","created":"2023-12-20","cited_by_count":2,"area":null},{"id":"2406.18616","title":"Towards Large Language Model Aided Program Refinement","created":"2024-06-26","cited_by_count":2,"area":null},{"id":"2411.00863","title":"Next-Token Prediction Task Assumes Optimal Data Ordering for LLM Training in Proof Generation","created":"2024-10-30","cited_by_count":2,"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":"2507.08425","title":"A Survey of Large Language Models in Discipline-specific Research: Challenges, Methods and Opportunities","created":"2025-07-11","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.14688","title":"Flood and Harvest: The Provable Necessity of Trivia for Generating Valuable Mathematics via the Lens of Language Generation in the Limit","created":"2026-06-12","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":"2309.12711","title":"The Mathematical Game","created":"2023-09-22","cited_by_count":1,"area":null},{"id":"2501.14951","title":"E-Gen: Leveraging E-Graphs to Improve Continuous Representations of Symbolic Expressions","created":"2025-01-24","cited_by_count":1,"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":"2502.04671","title":"ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving","created":"2025-02-07","cited_by_count":1,"area":null},{"id":"2504.19188","title":"Hierarchical Attention Generates Better Proofs","created":"2025-04-27","cited_by_count":1,"area":null},{"id":"2505.17964","title":"Counting Cycles with AI: Counting Cycles with AI: Computationally Efficient Equivalent Forms with Applications","created":"2025-05-23","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.04719","title":"Advocate for Complete Benchmarks for Formal Reasoning with Formal/Informal Statements and Formal/Informal Proofs","created":"2025-07-07","cited_by_count":1,"area":null},{"id":"2510.21999","title":"Foundation of Intelligence: Review of Math Word Problems from Human Cognition Perspective","created":"2025-10-24","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.04653","title":"Vibe Coding an LLM-powered Theorem Prover","created":"2026-01-08","cited_by_count":1,"area":null},{"id":"2603.04852","title":"Non-Parametric Structural Priors for Geometry Theorem Prediction","created":"2026-03-05","cited_by_count":1,"area":null},{"id":"2603.19715","title":"Neuro-Symbolic Proof Generation for Scaling Systems Software Verification","created":"2026-03-20","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":"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":"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":"2310.02896","title":"Notes on a Path to AI Assistance in Mathematical Reasoning","created":"2023-10-04","cited_by_count":0,"area":null},{"id":"2310.08066","title":"The Search-and-Mix Paradigm in Approximate Nash Equilibrium Algorithms","created":"2023-10-12","cited_by_count":0,"area":null},{"id":"2402.16878","title":"EvoGPT-f: An Evolutionary GPT Framework for Benchmarking Formal Math Languages","created":"2024-02-12","cited_by_count":0,"area":null},{"id":"2511.10339","title":"Massively Parallel Proof-Number Search for Impartial Games and Beyond","created":"2025-11-13","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":"2602.18767","title":"Nazrin: An Atomic Neural Proof Automation Tactic in Lean 4","created":"2026-02-21","cited_by_count":0,"area":null},{"id":"2605.06690","title":"State Representation and Termination for Recursive Reasoning Systems","created":"2026-05-02","cited_by_count":0,"area":null},{"id":"2605.22874","title":"NeuroNL2LTL: A Neurosymbolic Framework for Natural Language Translation of Linear Temporal Logic","created":"2026-05-20","cited_by_count":0,"area":null},{"id":"2606.05729","title":"Automated Proving of Shannon-Type Entropy Inequalities via Fine-Tuned Language Models and Guided Tree Search","created":"2026-06-04","cited_by_count":0,"area":null},{"id":"2606.24899","title":"From Meta Idea to Advanced Mathematical Discovery -- Human-AI Co-Discovery of Sign-Embedding Quantum Algorithms","created":"2026-06-12","cited_by_count":0,"area":null}],"next_cursor":"100"}