{"list":"other","total":53,"rows":[{"id":"2306.15626","title":"LeanDojo: Theorem Proving with Retrieval-Augmented Language Models","created":"2023-06-27","cited_by_count":427},{"id":"2109.00110","title":"MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics","created":"2021-08-31","cited_by_count":391},{"id":"2402.03927","title":"Leak, Cheat, Repeat: Data Contamination and Evaluation Malpractices in Closed-Source LLMs","created":"2024-02-06","cited_by_count":229},{"id":"2408.08152","title":"DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search","created":"2024-08-15","cited_by_count":197},{"id":"2504.11354","title":"Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning","created":"2025-04-15","cited_by_count":180},{"id":"2407.11214","title":"PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition","created":"2024-07-15","cited_by_count":165},{"id":"2508.03613","title":"Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction","created":"2025-08-05","cited_by_count":154},{"id":"2305.10160","title":"Stop Uploading Test Data in Plain Text: Practical Strategies for Mitigating Data Contamination by Evaluation Benchmarks","created":"2023-05-17","cited_by_count":142},{"id":"1910.09336","title":"The Lean mathematical library","created":"2019-10-21","cited_by_count":134},{"id":"2507.23726","title":"Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving","created":"2025-07-31","cited_by_count":101},{"id":"2504.16074","title":"PHYBench: Holistic Evaluation of Physical Perception and Reasoning in Large Language Models","created":"2025-04-22","cited_by_count":61},{"id":"2404.12534","title":"Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean","created":"2024-04-18","cited_by_count":58},{"id":"2510.01346","title":"Aristotle: IMO-level Automated Theorem Proving","created":"2025-10-01","cited_by_count":58},{"id":"2502.00334","title":"UGPhysics: A Comprehensive Benchmark for Undergraduate Physics Reasoning with Large Language Models","created":"2025-02-01","cited_by_count":48},{"id":"2505.02735","title":"FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models","created":"2025-05-05","cited_by_count":48},{"id":"2408.03350","title":"miniCTX: Neural Theorem Proving with (Long-)Contexts","created":"2024-08-05","cited_by_count":37},{"id":"2502.15815","title":"Theoretical Physics Benchmark (TPBench) -- a Dataset and Study of AI Reasoning Capabilities in Theoretical Physics","created":"2025-02-19","cited_by_count":34},{"id":"2510.12787","title":"Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics","created":"2025-10-14","cited_by_count":31},{"id":"2602.24273","title":"A Minimal Agent for Automated Theorem Proving","created":"2026-02-27","cited_by_count":18},{"id":"2602.17016","title":"M2F: Automated Formalization of Mathematical Literature at Scale","created":"2026-02-19","cited_by_count":15},{"id":"2405.08863","title":"HepLean: Digitalising high energy physics","created":"2024-05-14","cited_by_count":10},{"id":"2602.16554","title":"MerLean: An Agentic Framework for Autoformalization in Quantum Computation","created":"2026-02-18","cited_by_count":10},{"id":"2605.13171","title":"Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics","created":"2026-05-13","cited_by_count":10},{"id":"2210.12150","title":"Formalizing Chemical Physics using the Lean Theorem Prover","created":"2022-10-21","cited_by_count":9},{"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},{"id":"2602.18307","title":"VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Lean","created":"2026-02-20","cited_by_count":8},{"id":"2603.02668","title":"SorryDB: Can AI Provers Complete Real-World Lean Theorems?","created":"2026-03-03","cited_by_count":8},{"id":"1912.02250","title":"A Verified Optimizer for Quantum Circuits","created":"2019-12-04","cited_by_count":7},{"id":"2510.08672","title":"A Formalization of the Generalized Quantum Stein's Lemma in Lean","created":"2025-10-09","cited_by_count":7},{"id":"2603.12744","title":"TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib?","created":"2026-03-13","cited_by_count":6},{"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},{"id":"2510.26094","title":"Lean4Physics: Comprehensive Reasoning Framework for College-level Physics in Lean4","created":"2025-10-30","cited_by_count":5},{"id":"2603.08139","title":"Formalizing the stability of the two Higgs doublet model potential into Lean: identifying an error in the literature","created":"2026-03-09","cited_by_count":5},{"id":"2606.14000","title":"Formalizing Numerical Analysis: An Agent Pipeline and Quality Audit Beyond Kernel Acceptance","created":"2026-06-12","cited_by_count":5},{"id":"2411.07667","title":"Formalization of physics index notation in Lean 4","created":"2024-11-12","cited_by_count":4},{"id":"2604.23002","title":"FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean","created":"2026-04-24","cited_by_count":4},{"id":"2605.16523","title":"End-to-End Formalization of Quantum Error Correction","created":"2026-05-15","cited_by_count":4},{"id":"2204.07112","title":"A Formally Certified End-to-End Implementation of Shor's Factorization Algorithm","created":"2022-04-14","cited_by_count":3},{"id":"2606.29687","title":"A Machine-Verified Proof of a Quantum-Optimization Conjecture","created":"2026-06-29","cited_by_count":3},{"id":"2012.13925","title":"Certified Quantum Computation in Isabelle/HOL","created":"2020-12-27","cited_by_count":2},{"id":"2202.05360","title":"Formalized functional analysis with semilinear maps","created":"2022-02-10","cited_by_count":2},{"id":"2603.28406","title":"Physics as Code: From Scans to Theorems with ITP APIs in $SU(5)$ Model Building","created":"2026-03-30","cited_by_count":2},{"id":"2607.06379","title":"Axioms for physical reasoning: codifying the Seiberg--Witten solution in Lean","created":"2026-07-07","cited_by_count":2},{"id":"2607.07857","title":"Multi-agent Autoformalization of Tensor Network Theory","created":"2026-07-08","cited_by_count":2},{"id":"2607.08986","title":"A Formalization of the Mean-Field Derivation of the Vlasov Equation","created":"2026-07-09","cited_by_count":2},{"id":"2607.09632","title":"Lean-QIT: Towards a Formal Infrastructure for Quantum Information Theory","created":"2026-07-10","cited_by_count":2},{"id":"1511.01568","title":"Formalization of Quantum Protocols using Coq","created":"2015-11-05","cited_by_count":1},{"id":"2207.11350","title":"CoqQ: Foundational Verification of Quantum Programs","created":"2022-07-22","cited_by_count":1},{"id":"2306.12535","title":"A formalization of the CHSH inequality and Tsirelson's upper-bound in Isabelle/HOL","created":"2023-06-21","cited_by_count":1},{"id":"2604.03884","title":"Formalizing CHSH Rigidity in Lean 4","created":"2026-04-04","cited_by_count":1},{"id":"2607.05492","title":"Lean-Quantum: Toward AI-Assisted Formalization of Quantum Information","created":"2026-07-06","cited_by_count":1},{"id":"2607.19263","title":"Proving the Limits of Quantum Power Flow","created":"2026-07-21","cited_by_count":1},{"id":"2607.19407","title":"ITPEval: Benchmarking Formal Translation Across Interactive Theorem Provers","created":"2026-07-07","cited_by_count":1}],"next_cursor":null}