{"total":92,"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":"2301.13867","title":"Mathematical Capabilities of ChatGPT","created":"2023-01-31","cited_by_count":268,"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":"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":"2310.00656","title":"LEGO-Prover: Neural Theorem Proving with Growing Libraries","created":"2023-10-01","cited_by_count":109,"area":null},{"id":"2304.11062","title":"Scaling Transformer to 1M tokens and beyond with RMT","created":"2023-04-19","cited_by_count":98,"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":"2311.14125","title":"Scalable AI Safety via Doubly-Efficient Debate","created":"2023-11-23","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":"2101.06223","title":"LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning","created":"2021-01-15","cited_by_count":46,"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":"2505.23135","title":"VERINA: Benchmarking Verifiable Code Generation","created":"2025-05-29","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":"2406.07222","title":"Reliable Evaluation and Benchmarks for Statement Autoformalization","created":"2024-06-11","cited_by_count":32,"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":"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":"2405.01787","title":"Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming","created":"2024-05-03","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":"2602.17016","title":"M2F: Automated Formalization of Mathematical Literature at Scale","created":"2026-02-19","cited_by_count":15,"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":"2304.00994","title":"Machine-Learned Premise Selection for Lean","created":"2023-03-17","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":"2509.22246","title":"ASSESS: A Semantic and Structural Evaluation Framework for Statement Similarity","created":"2025-09-26","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":"2510.10815","title":"DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems","created":"2025-10-12","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.03071","title":"Automatic Textbook Formalization","created":"2026-04-03","cited_by_count":8,"area":null},{"id":"2504.19110","title":"APE-Bench: Evaluating Automated Proof Engineering for Formal Math Libraries","created":"2025-04-27","cited_by_count":7,"area":null},{"id":"2506.07477","title":"Premise Selection for a Lean Hammer","created":"2025-06-09","cited_by_count":6,"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":"2603.26996","title":"FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?","created":"2026-03-27","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":"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":"2503.19605","title":"Lean Formalization of Generalization Error Bound by Rademacher Complexity and Dudley's Entropy Integral","created":"2025-03-25","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":"2605.30333","title":"COMPOSE: Composing Future Theorems from Citations and Formal Structure","created":"2026-05-28","cited_by_count":3,"area":null},{"id":"2606.23959","title":"Does My Embedding Reflect That $A = B$? Evaluating Mathematical Equivalence in Embedding Models","created":"2026-06-22","cited_by_count":3,"area":null},{"id":"2402.04689","title":"Stein Boltzmann Sampling: A Variational Approach for Global Optimization","created":"2024-02-07","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":"2512.07766","title":"Formalized Hopfield Networks and Boltzmann Machines","created":"2025-12-08","cited_by_count":2,"area":null},{"id":"2604.16584","title":"Certified Program Synthesis with a Multi-Modal Verifier","created":"2026-04-17","cited_by_count":2,"area":null},{"id":"2605.27246","title":"Many Logics, One Methodology: A Plea for Logical Pluralism in Formalised Reasoning (preprint)","created":"2026-05-26","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":"2607.09632","title":"Lean-QIT: Towards a Formal Infrastructure for Quantum Information Theory","created":"2026-07-10","cited_by_count":2,"area":null},{"id":"2608.13522","title":"Vero: Can AI Agents Build Formally Verified Software Repositories?","created":"2026-08-13","cited_by_count":2,"area":null},{"id":"2608.15432","title":"Does the Proof Prove It That Way? Faithful Formalization of Elements Proofs","created":"2026-08-15","cited_by_count":2,"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":"2510.23637","title":"Combining Textual and Structural Information for Premise Selection in Lean","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":"2605.19063","title":"Mapping Uncharted Symmetries: Machine Discovery in Combinatorics","created":"2026-05-18","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.00329","title":"Benchmarking Recursive-Collapse Warning Claims Under Matched False-Positive Control","created":"2026-05-29","cited_by_count":1,"area":null},{"id":"2606.10799","title":"Evaluating Research-Level Math Proofs via Strict Step-Level Verification","created":"2026-06-09","cited_by_count":1,"area":null},{"id":"2606.13782","title":"MA-ProofBench: A Two-Tiered Evaluation of LLMs for Theorem Proving in Mathematical Analysis","created":"2026-06-11","cited_by_count":1,"area":null},{"id":"2606.20642","title":"Hypothesis-Disciplined Multi-Agent Automated Formalization of Asymptotic Statistical Theory","created":"2026-06-03","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":"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":"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":"2506.07066","title":"From Axioms to Algorithms: Mechanized Proofs of the vNM Utility Theorem","created":"2025-06-08","cited_by_count":0,"area":null},{"id":"2510.11944","title":"TopoAlign: A Framework for Aligning Code to Math via Topological Decomposition","created":"2025-10-13","cited_by_count":0,"area":null},{"id":"2511.21104","title":"BRIDGE: Building Representations In Domain Guided Program Synthesis","created":"2025-11-26","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":"2604.21187","title":"Doubly Saturated Ramsey Graphs: A Case Study in Computer-Assisted Mathematical Discovery","created":"2026-04-23","cited_by_count":0,"area":null},{"id":"2605.22885","title":"ImProver 2: Iteratively Self-Improving LMs for Neurosymbolic Proof Optimization","created":"2026-05-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":"2607.01734","title":"Reformalization of the Jordan Curve Theorem","created":"2026-07-02","cited_by_count":0,"area":null},{"id":"2607.28459","title":"LeanCSP: A Framework for Certifying Constraint Reformulation and Solving in Lean","created":"2026-07-30","cited_by_count":0,"area":null},{"id":"2608.11173","title":"A Quantum Roadmap for Softmax Attention: Exact Born-Rule Analogs for Softmax Attention on the Probability Simplex","created":"2026-08-11","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.14585","title":"Euclid-Omni : A Unified Neuro-Symbolic Framework for Plane Geometry","created":"2026-06-17","cited_by_count":0,"area":null},{"id":"2608.16155","title":"REFLEX: Reflexive Equilibrium Fixed-point Learning for Endogenous eXchanges","created":"2026-08-17","cited_by_count":0,"area":null},{"id":"2608.21356","title":"AI with Authority, from Application to Silicon","created":"2026-08-21","cited_by_count":0,"area":null},{"id":"2608.22117","title":"TANGO: Treating Tokens as Operators","created":"2026-08-22","cited_by_count":0,"area":null},{"id":"2608.26310","title":"FaithSieve: Fine-Grained Evaluation of Math Proofs with Faithful Formal Evidence","created":"2026-08-26","cited_by_count":0,"area":null},{"id":"2609.00420","title":"How Temporal Correlations Shape Memory in Linear Recurrent Neural Networks","created":"2026-08-31","cited_by_count":0,"area":null},{"id":"2609.00706","title":"A Certificate-Producing Cascade for Equational Implication: The SAIR EQT2 Stage 2 Solver","created":"2026-09-01","cited_by_count":0,"area":null},{"id":"2609.00969","title":"The zbMATH Open Knowledge Graph: Tracing Centuries of Mathematical Research","created":"2026-09-01","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.10579","title":"A machine-checked proof of the Dong-Yang classification of optimal (n,4) binary codes for BSCs","created":"2026-09-05","cited_by_count":0,"area":null},{"id":"2609.13057","title":"Benign Loss Landscapes Can Coexist with Worst-Case Hardness","created":"2026-09-11","cited_by_count":0,"area":null},{"id":"2609.13703","title":"Gap Entropy and Almost Instance-Wise Optimal Best-Arm Identification","created":"2026-09-12","cited_by_count":0,"area":null},{"id":"2609.15289","title":"Math for AI safety: an invitation for mathematicians","created":"2026-09-14","cited_by_count":0,"area":null},{"id":"2609.35790","title":"Sage: Formalization with Semantic Correction","created":"2026-09-16","cited_by_count":0,"area":null},{"id":"2609.36663","title":"GenLimitLib: A Formal Library for Language Generation in the Limit and AI-Assisted Mathematical Research","created":"2026-09-29","cited_by_count":0,"area":null},{"id":"2610.13461","title":"SqueezeBench: Saturation-Resilient Evaluation of Mathematical Capability","created":"2026-10-09","cited_by_count":0,"area":null},{"id":"2610.17132","title":"Masked Attention Pooling Is Invariant to Padding and Permutation: A Formal Proof in Lean","created":"2026-10-12","cited_by_count":0,"area":null},{"id":"2610.18301","title":"A dataset of formalised theorem statements from the Annals of Mathematics","created":"2026-10-13","cited_by_count":0,"area":null}],"next_cursor":null}