{"total":78,"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":"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":"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":"2104.01112","title":"NaturalProofs: Mathematical Theorem Proving in Natural Language","created":"2021-03-24","cited_by_count":81,"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":"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":"2205.12443","title":"Generating Natural Language Proofs with Verifier-Guided Search","created":"2022-05-25","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":"2409.13082","title":"AutoVerus: Automated Proof Generation for Rust Code","created":"2024-09-19","cited_by_count":49,"area":null},{"id":"2101.06223","title":"LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning","created":"2021-01-15","cited_by_count":46,"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.17216","title":"Autoformalizing Euclidean Geometry","created":"2024-05-27","cited_by_count":27,"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.14274","title":"Proof Automation with Large Language Models","created":"2024-09-22","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":"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":"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":"2106.09146","title":"Contrastive Reinforcement Learning of Symbolic Reasoning Domains","created":"2021-06-16","cited_by_count":17,"area":null},{"id":"2305.14699","title":"Can Transformers Learn to Solve Problems Recursively?","created":"2023-05-24","cited_by_count":17,"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":"2401.12947","title":"Transformer-Based Models Are Not Yet Perfect At Learning to Emulate Structural Recursion","created":"2024-01-23","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":"2311.03739","title":"Leveraging Large Language Models for Automated Proof Synthesis in Rust","created":"2023-11-07","cited_by_count":11,"area":null},{"id":"2405.16792","title":"Laurel: Unblocking Automated Verification with Large Language Models","created":"2024-05-27","cited_by_count":11,"area":null},{"id":"2410.19605","title":"CoqPilot, a plugin for LLM-based generation of proofs","created":"2024-10-25","cited_by_count":11,"area":null},{"id":"2111.12038","title":"Learning Symbolic Rules for Reasoning in Quasi-Natural Language","created":"2021-11-23","cited_by_count":9,"area":null},{"id":"2402.17032","title":"REFACTOR: Learning to Extract Theorems from Proofs","created":"2024-02-26","cited_by_count":9,"area":null},{"id":"2410.19940","title":"Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verification","created":"2024-10-25","cited_by_count":9,"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":"2105.14706","title":"The Role of Entropy in Guiding a Connection Prover","created":"2021-05-31","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":"2312.04556","title":"Large Language Models for Mathematicians","created":"2023-12-07","cited_by_count":7,"area":null},{"id":"2110.10054","title":"Generating Symbolic Reasoning Problems with Transformer GANs","created":"2021-10-19","cited_by_count":5,"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":"2304.10486","title":"CoProver: A Recommender System for Proof Construction","created":"2023-03-01","cited_by_count":5,"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.23109","title":"Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems","created":"2026-05-22","cited_by_count":4,"area":null},{"id":"2108.10821","title":"Graph Contrastive Pre-training for Effective Theorem Reasoning","created":"2021-08-24","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":"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},{"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":"2411.14870","title":"Application of AI to formal methods - an analysis of current trends","created":"2024-11-22","cited_by_count":2,"area":null},{"id":"2209.02562","title":"Project proposal: A modular reinforcement learning based automated theorem prover","created":"2022-09-06","cited_by_count":1,"area":null},{"id":"2304.10500","title":"Transformer Models for Type Inference in the Simply Typed Lambda Calculus: A Case Study in Deep Learning for Code","created":"2023-03-15","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":"2402.08365","title":"Learning Better Representations From Less Data For Propositional Satisfiability","created":"2024-02-13","cited_by_count":1,"area":null},{"id":"2403.12627","title":"Enhancing Formal Theorem Proving: A Comprehensive Dataset for Training AI Models on Coq Code","created":"2024-03-19","cited_by_count":1,"area":null},{"id":"2410.02666","title":"AlphaIntegrator: Transformer Action Search for Symbolic Integration Proofs","created":"2024-10-03","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":"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.07654","title":"Towards Automating Blockchain Consensus Verification with IsabeLLM","created":"2026-01-12","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":"2606.18098","title":"IsabeLLM: Automated Theorem Proving Applied to Formally Verifying Consensus","created":"2026-06-16","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.19407","title":"ITPEval: Benchmarking Formal Translation Across Interactive Theorem Provers","created":"2026-07-07","cited_by_count":1,"area":null},{"id":"2211.11937","title":"Genetic Algorithm for Program Synthesis","created":"2022-11-22","cited_by_count":0,"area":null},{"id":"2411.01188","title":"Learning Rules Explaining Interactive Theorem Proving Tactic Prediction","created":"2024-11-02","cited_by_count":0,"area":null},{"id":"2602.18843","title":"ABD: Default Exception Abduction in Finite First Order Worlds","created":"2026-02-21","cited_by_count":0,"area":null},{"id":"2602.18956","title":"INDUCTION: Finite-Structure Concept Synthesis in First-Order Logic","created":"2026-02-21","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.05420","title":"Can Open-Weight LLMs Produce Kernel-Verified Coq Proofs? A Pilot Study","created":"2026-08-05","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}],"next_cursor":null}