{"total":87,"rows":[{"id":"2109.00110","title":"MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics","created":"2021-08-31","cited_by_count":391,"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":"2202.01344","title":"Formal Mathematics Statement Curriculum Learning","created":"2022-02-03","cited_by_count":142,"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":"2104.01112","title":"NaturalProofs: Mathematical Theorem Proving in Natural Language","created":"2021-03-24","cited_by_count":81,"area":null},{"id":"2205.12910","title":"NaturalProver: Grounded Mathematical Proof Generation with Language Models","created":"2022-05-25","cited_by_count":72,"area":null},{"id":"2112.01898","title":"Linear algebra with transformers","created":"2021-12-03","cited_by_count":63,"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":"2309.04295","title":"FIMO: A Challenge Formal Dataset for Automated Theorem Proving","created":"2023-09-08","cited_by_count":55,"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":"2412.11427","title":"Towards Scientific Discovery with Generative AI: Progress, Opportunities, and Challenges","created":"2024-12-16","cited_by_count":41,"area":null},{"id":"2102.09756","title":"TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning","created":"2021-02-19","cited_by_count":37,"area":null},{"id":"2408.03350","title":"miniCTX: Neural Theorem Proving with (Long-)Contexts","created":"2024-08-05","cited_by_count":37,"area":null},{"id":"2405.13001","title":"Large Language Models for Education: A Survey","created":"2024-05-12","cited_by_count":34,"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":"2310.18457","title":"LLMSTEP: LLM proofstep suggestions in Lean","created":"2023-10-27","cited_by_count":32,"area":null},{"id":"2405.17216","title":"Autoformalizing Euclidean Geometry","created":"2024-05-27","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":"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":"2410.04194","title":"Consistent Autoformalization for Constructing Mathematical Libraries","created":"2024-10-05","cited_by_count":21,"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":"2306.13840","title":"Beyond Scale: The Diversity Coefficient as a Data Quality Metric for Variability in Natural Language Data","created":"2023-06-24","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":"2401.02949","title":"Graph2Tac: Online Representation Learning of Formal Math Concepts","created":"2024-01-05","cited_by_count":15,"area":null},{"id":"2304.12602","title":"Is deep learning a useful tool for the pure mathematician?","created":"2023-04-25","cited_by_count":14,"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":"2208.01545","title":"The Curse of Low Task Diversity: On the Failure of Transfer Learning to Outperform MAML and Their Empirical Equivalence","created":"2022-08-02","cited_by_count":10,"area":null},{"id":"2302.09350","title":"BERT is not The Count: Learning to Match Mathematical Statements with Proofs","created":"2023-02-18","cited_by_count":10,"area":null},{"id":"2310.07957","title":"A New Approach Towards Autoformalization","created":"2023-10-12","cited_by_count":10,"area":null},{"id":"2103.03798","title":"Training a First-Order Theorem Prover from Synthetic Data","created":"2021-03-05","cited_by_count":8,"area":null},{"id":"2306.13841","title":"Is Pre-training Truly Better Than Meta-Learning?","created":"2023-06-24","cited_by_count":6,"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":"2410.11133","title":"3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes","created":"2024-10-14","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":"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":"2205.14229","title":"Learning to Find Proofs and Theorems by Learning to Refine Search Strategies: The Case of Loop Invariant Synthesis","created":"2022-05-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":"2502.15507","title":"Steering LLMs for Formal Theorem Proving","created":"2025-02-21","cited_by_count":4,"area":null},{"id":"2201.04275","title":"PhysNLU: A Language Resource for Evaluating Natural Language Understanding and Explanation Coherence in Physics","created":"2022-01-12","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":"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":"2402.02104","title":"Learning Structure-Aware Representations of Dependent Types","created":"2024-02-03","cited_by_count":2,"area":null},{"id":"2403.03401","title":"BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving","created":"2024-03-06","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":"2410.17161","title":"Interchangeable Token Embeddings for Extendable Vocabulary and Alpha-Equivalence","created":"2024-10-22","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":"2205.15389","title":"Attention Flows for General Transformers","created":"2022-05-30","cited_by_count":1,"area":null},{"id":"2207.06679","title":"Learning to Prove Trigonometric Identities","created":"2022-07-14","cited_by_count":1,"area":null},{"id":"2303.14882","title":"TransCODE: Co-design of Transformers and Accelerators for Efficient Training and Inference","created":"2023-03-27","cited_by_count":1,"area":null},{"id":"2306.16951","title":"Applying language models to algebraic topology: generating simplicial cycles using multi-labeling in Wu's formula","created":"2023-06-01","cited_by_count":1,"area":null},{"id":"2401.02950","title":"The Tactician's Web of Large-Scale Formal Knowledge","created":"2024-01-05","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":"2504.20010","title":"Towards Automated Scoping of AI for Social Good Projects","created":"2025-04-28","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.23169","title":"Names Don't Matter: Symbol-Invariant Transformer for Open-Vocabulary Learning","created":"2026-01-30","cited_by_count":1,"area":null},{"id":"2603.19828","title":"FormalEvolve: Neuro-Symbolic Evolutionary Search for Diverse Autoformalization","created":"2026-03-20","cited_by_count":1,"area":null},{"id":"2605.26959","title":"MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving","created":"2026-05-26","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":"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":"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.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.14867","title":"Evaluating the Robustness of Proof Autoformalization in Lean 4","created":"2026-06-12","cited_by_count":0,"area":null},{"id":"2606.28572","title":"Geometric Measurements of the Axiom of Choice in Neural Proof Embeddings","created":"2026-06-26","cited_by_count":0,"area":null},{"id":"2608.12762","title":"PROVE-RT: Generating Mechanized Theorem Prover Scripts for Real-Time Systems using LLMs","created":"2026-08-13","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.25575","title":"Direct Optimization of Generators for Search in Automated Theorem Proving","created":"2026-09-22","cited_by_count":0,"area":null},{"id":"2609.31029","title":"Governed Deduction: Policy-Grounded Premise Authorization Beyond Relevance","created":"2026-09-25","cited_by_count":0,"area":null},{"id":"2609.32908","title":"Predicting the Next State Is Not Enough: JEPA Representations for Lean Theorem Proving","created":"2026-09-26","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}],"next_cursor":null}