{"total":53,"rows":[{"id":"2303.18223","title":"A Survey of Large Language Models","created":"2023-03-31","cited_by_count":2576,"area":null},{"id":"2306.15626","title":"LeanDojo: Theorem Proving with Retrieval-Augmented Language Models","created":"2023-06-27","cited_by_count":427,"area":"rag"},{"id":"2205.12615","title":"Autoformalization with Large Language Models","created":"2022-05-25","cited_by_count":263,"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":"2310.15164","title":"LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers","created":"2023-10-23","cited_by_count":168,"area":"lr"},{"id":"2102.06203","title":"Proof Artifact Co-training for Theorem Proving with Language Models","created":"2021-02-11","cited_by_count":132,"area":"offlinerl"},{"id":"2310.00656","title":"LEGO-Prover: Neural Theorem Proving with Growing Libraries","created":"2023-10-01","cited_by_count":109,"area":null},{"id":"2412.16075","title":"Formal Mathematical Reasoning: A New Frontier in AI","created":"2024-12-20","cited_by_count":81,"area":"lr"},{"id":"2410.10878","title":"Herald: A Natural Language Annotated Lean 4 Dataset","created":"2024-10-09","cited_by_count":59,"area":"lr"},{"id":"2404.09939","title":"A Survey on Deep Learning for Theorem Proving","created":"2024-04-15","cited_by_count":57,"area":null},{"id":"2406.01940","title":"Process-Driven Autoformalization in Lean 4","created":"2024-06-04","cited_by_count":45,"area":"lr"},{"id":"2311.03755","title":"Multilingual Mathematical Autoformalization","created":"2023-11-07","cited_by_count":39,"area":null},{"id":"2206.01962","title":"Formal Specifications from Natural Language","created":"2022-06-04","cited_by_count":33,"area":null},{"id":"2301.02195","title":"Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs","created":"2023-01-05","cited_by_count":27,"area":null},{"id":"2405.17216","title":"Autoformalizing Euclidean Geometry","created":"2024-05-27","cited_by_count":27,"area":null},{"id":"2410.10135","title":"FormalAlign: Automated Alignment Evaluation for Autoformalization","created":"2024-10-14","cited_by_count":24,"area":null},{"id":"2502.05567","title":"ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data","created":"2025-02-08","cited_by_count":23,"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":"2510.04520","title":"Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graph","created":"2025-10-06","cited_by_count":21,"area":"agents"},{"id":"2601.03298","title":"130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone?","created":"2026-01-06","cited_by_count":18,"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":"2507.07399","title":"Generalized Tree Edit Distance (GTED): A Faithful Evaluation Metric for Statement Autoformalization","created":"2025-07-10","cited_by_count":12,"area":null},{"id":"2505.20047","title":"Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Tasks","created":"2025-05-26","cited_by_count":10,"area":"lr"},{"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":"2301.11479","title":"Alien Coding","created":"2023-01-27","cited_by_count":9,"area":null},{"id":"2404.01234","title":"GFLean: An Autoformalisation Framework for Lean via GF","created":"2024-04-01","cited_by_count":9,"area":null},{"id":"2511.09008","title":"A Neurosymbolic Approach to Natural Language Formalization and Verification","created":"2025-11-12","cited_by_count":9,"area":null},{"id":"2510.15940","title":"Lean Finder: Semantic Search for Mathlib That Understands User Intents","created":"2025-10-08","cited_by_count":8,"area":null},{"id":"2305.16433","title":"Neural Machine Translation for Mathematical Formulae","created":"2023-05-25","cited_by_count":7,"area":null},{"id":"2403.04017","title":"Learning Guided Automated Reasoning: A Brief Survey","created":"2024-03-06","cited_by_count":7,"area":"lr"},{"id":"2410.11900","title":"FLARE: Faithful Logic-Aided Reasoning and Exploration","created":"2024-10-14","cited_by_count":7,"area":"lr"},{"id":"2509.09810","title":"Towards a Common Framework for Autoformalization","created":"2025-09-11","cited_by_count":7,"area":null},{"id":"2303.06686","title":"MizAR 60 for Mizar 50","created":"2023-03-12","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":"2101.09142","title":"A Study of Continuous Vector Representationsfor Theorem Proving","created":"2021-01-22","cited_by_count":4,"area":null},{"id":"2502.15795","title":"Lean-ing on Quality: How High-Quality Data Beats Diverse Multilingual Data in AutoFormalization","created":"2025-02-18","cited_by_count":4,"area":null},{"id":"2508.00459","title":"Thinking Machines: Mathematical Reasoning in the Age of LLMs","created":"2025-08-01","cited_by_count":4,"area":"lr"},{"id":"2503.01389","title":"Learning Conjecturing from Scratch","created":"2025-03-03","cited_by_count":3,"area":null},{"id":"2504.04945","title":"A Llama walks into the 'Bar': Efficient Supervised Fine-Tuning for Legal Reasoning in the Multi-state Bar Exam","created":"2025-04-07","cited_by_count":3,"area":"lr"},{"id":"2511.11990","title":"Improving Autoformalization Using Direct Dependency Retrieval","created":"2025-11-15","cited_by_count":2,"area":"rag"},{"id":"2101.11716","title":"Disambiguating Symbolic Expressions in Informal Documents","created":"2021-01-25","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":"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.08665","title":"KELPS: A Framework for Verified Multi-Language Autoformalization via Semantic-Syntactic Alignment","created":"2025-07-11","cited_by_count":1,"area":null},{"id":"2604.07455","title":"Munkres' General Topology Autoformalized in Isabelle/HOL","created":"2026-04-08","cited_by_count":1,"area":null},{"id":"2604.19000","title":"Decompose, Structure, and Repair: A Neuro-Symbolic Framework for Autoformalization via Operator Trees","created":"2026-04-21","cited_by_count":1,"area":null},{"id":"2305.07903","title":"Translating SUMO-K to Higher-Order Set Theory","created":"2023-05-13","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":"2606.16893","title":"Symbolic Informalization: Fluent, Productive, Multilingual","created":"2026-06-15","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":"2610.08329","title":"An AI-Assisted Formalization of the Poincar\\'e Conjecture","created":"2026-10-06","cited_by_count":0,"area":null}],"next_cursor":null}