{"total":88,"rows":[{"id":"2303.18223","title":"A Survey of Large Language Models","created":"2023-03-31","cited_by_count":2576,"area":null},{"id":"2307.05782","title":"Large Language Models","created":"2023-07-11","cited_by_count":780,"area":null},{"id":"2605.00674","title":"Beyond Benchmarks: MathArena as an Evaluation Platform for Mathematics with LLMs","created":"2026-05-01","cited_by_count":137,"area":null},{"id":"2502.07640","title":"Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving","created":"2025-02-11","cited_by_count":133,"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":"2312.17120","title":"MathPile: A Billion-Token-Scale Pretraining Corpus for Math","created":"2023-12-28","cited_by_count":67,"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.18321","title":"MathOdyssey: Benchmarking Mathematical Problem-Solving Skills in Large Language Models Using Odyssey Math Data","created":"2024-06-26","cited_by_count":52,"area":null},{"id":"2311.03755","title":"Multilingual Mathematical Autoformalization","created":"2023-11-07","cited_by_count":39,"area":null},{"id":"2408.03350","title":"miniCTX: Neural Theorem Proving with (Long-)Contexts","created":"2024-08-05","cited_by_count":37,"area":null},{"id":"2402.07625","title":"Autonomous Data Selection with Zero-shot Generative Classifiers for Mathematical Texts","created":"2024-02-12","cited_by_count":27,"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":"2410.10135","title":"FormalAlign: Automated Alignment Evaluation for Autoformalization","created":"2024-10-14","cited_by_count":24,"area":null},{"id":"2412.03205","title":"U-MATH: A University-Level Benchmark for Evaluating Mathematical Skills in LLMs","created":"2024-12-04","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":"2502.12065","title":"Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitions","created":"2025-02-17","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":"2506.07047","title":"Mathesis: Towards Formal Theorem Proving from Natural Languages","created":"2025-06-08","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":"2412.15184","title":"Data for Mathematical Copilots: Better Ways of Presenting Proofs for Machine Learning","created":"2024-12-19","cited_by_count":11,"area":null},{"id":"2306.08997","title":"Exploring the MIT Mathematics and EECS Curriculum Using Large Language Models","created":"2023-06-15","cited_by_count":10,"area":null},{"id":"2505.10962","title":"MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation","created":"2025-05-16","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.29955","title":"Formalizing Mathematics at Scale","created":"2026-05-28","cited_by_count":10,"area":null},{"id":"2606.31002","title":"Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization","created":"2026-06-30","cited_by_count":10,"area":null},{"id":"2604.06802","title":"Riemann-Bench: A Benchmark for Moonshot Mathematics","created":"2026-04-08","cited_by_count":8,"area":null},{"id":"2604.25031","title":"Faithful Autoformalization via Roundtrip Verification and Repair","created":"2026-04-27","cited_by_count":8,"area":null},{"id":"2510.06857","title":"Autoformalizer with Tool Feedback","created":"2025-10-08","cited_by_count":7,"area":null},{"id":"2406.06140","title":"Can I understand what I create? Self-Knowledge Evaluation of Large Language Models","created":"2024-06-10","cited_by_count":6,"area":null},{"id":"2411.18104","title":"Training and Evaluating Language Models with Template-based Data Generation","created":"2024-11-27","cited_by_count":6,"area":null},{"id":"2505.13406","title":"AutoMathKG: The automated mathematical knowledge graph based on LLM and vector database","created":"2025-05-19","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":"2510.02335","title":"FormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theory","created":"2025-09-26","cited_by_count":5,"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":"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":"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":"2512.10317","title":"Translating Informal Proofs into Formal Proofs Using a Chain of States","created":"2025-12-11","cited_by_count":3,"area":null},{"id":"2601.18005","title":"Flow-based Extremal Mathematical Structure Discovery","created":"2026-01-25","cited_by_count":3,"area":null},{"id":"2605.10379","title":"Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness","created":"2026-05-11","cited_by_count":3,"area":null},{"id":"2607.14345","title":"Value Leakage: An LLM's Answers Are Silently Shaped by Its Own Values","created":"2026-07-15","cited_by_count":3,"area":null},{"id":"2503.09730","title":"Local Look-Ahead Guidance via Verifier-in-the-Loop for Automated Theorem Proving","created":"2025-03-12","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.18256","title":"MSC-180: A Benchmark for Automated Formal Theorem Proving from Mathematical Subject Classification","created":"2025-12-20","cited_by_count":2,"area":null},{"id":"2606.26246","title":"Lacuna: A Research Map for Machine Learning","created":"2026-06-24","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":"2303.17513","title":"Improving the Diproche CNL through Autoformalization via Large Language Models","created":"2023-03-12","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":"2504.19188","title":"Hierarchical Attention Generates Better Proofs","created":"2025-04-27","cited_by_count":1,"area":null},{"id":"2511.13043","title":"Spark-Prover-X1: Formal Theorem Proving Through Diverse Data Training","created":"2025-11-17","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":"2602.11212","title":"Towards Compressive and Scalable Recurrent Memory","created":"2026-02-11","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":"2604.23135","title":"Characterizing Paraphrase-Induced Failures in Lean 4 Autoformalization","created":"2026-04-25","cited_by_count":1,"area":null},{"id":"2604.23698","title":"Benchmarking Testing in Automated Theorem Proving","created":"2026-04-26","cited_by_count":1,"area":null},{"id":"2604.23712","title":"OptProver: Bridging Olympiad and Optimization through Continual Training in Formal Theorem Proving","created":"2026-04-26","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.10799","title":"Evaluating Research-Level Math Proofs via Strict Step-Level Verification","created":"2026-06-09","cited_by_count":1,"area":null},{"id":"2606.28013","title":"The Signal-Coverage Matrix: Stratifying Type and Semantic Errors in Statement Autoformalization","created":"2026-06-26","cited_by_count":1,"area":null},{"id":"2607.27709","title":"MECA: A Mechanism-Centered Agent for Constructing Well-Specified and Valuable Mathematical Conjectures","created":"2026-07-30","cited_by_count":1,"area":null},{"id":"2304.06186","title":"Using Large Language Models for (De-)Formalization and Natural Argumentation Exercises for Beginner's Students","created":"2023-04-12","cited_by_count":0,"area":null},{"id":"2507.19419","title":"TokenSmith: Streamlining Data Editing, Search, and Inspection for Large-Scale Language Model Training and Interpretability","created":"2025-07-25","cited_by_count":0,"area":null},{"id":"2511.11829","title":"Towards Autoformalization of LLM-generated Outputs for Requirement Verification","created":"2025-11-14","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.01008","title":"FVSpec: Real-World Property-Based Tests as Lean Challenges","created":"2026-05-31","cited_by_count":0,"area":null},{"id":"2606.09449","title":"Reasoning without Gold Standards: A Proxy-Judge Theory of Autoformalization","created":"2026-06-08","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":"2607.23425","title":"TLA+-Bench: An Execution-Grounded Benchmark and Dataset for Natural-Language to TLA Specification Generation","created":"2026-07-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.15979","title":"ALPS: Measuring Valid Creativity in Large Language Models with Mathematical Construction","created":"2026-08-17","cited_by_count":0,"area":null},{"id":"2608.28997","title":"Verification abundance, adjudication scarcity: what happens to mathematical knowledge when proof checking becomes free","created":"2026-08-29","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.28603","title":"Learning to Discover Interesting Mathematics","created":"2026-09-23","cited_by_count":0,"area":null},{"id":"2609.34460","title":"When Does Structured Knowledge Help Neural Theorem Proving?","created":"2026-09-28","cited_by_count":0,"area":null},{"id":"2609.35606","title":"TCSAlgBench: Benchmarking Automated Proving for Research-Level Theoretical Computer Science","created":"2026-09-28","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.39228","title":"Fyan: A Human--AI Harness with Semantic Auditing for Document-Level Formalization","created":"2026-09-30","cited_by_count":0,"area":null},{"id":"2609.39568","title":"Self-Spec Verifiable Code Generation","created":"2026-09-30","cited_by_count":0,"area":null},{"id":"2610.02792","title":"Law And Order: Tax Law Autoformalization","created":"2026-10-02","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.17697","title":"LeanPRM: Lean-Grounded Process Supervision for Natural Language Proof Verification","created":"2026-10-13","cited_by_count":0,"area":null},{"id":"2610.18498","title":"Aligning Faithfulness for Theory-Scale Autoformalization","created":"2026-10-13","cited_by_count":0,"area":null},{"id":"2610.19223","title":"Definition Grounding in Theory-Level Auto-formalization","created":"2026-10-13","cited_by_count":0,"area":null}],"next_cursor":null}