{"total":59,"rows":[{"id":"2412.16075","title":"Formal Mathematical Reasoning: A New Frontier in AI","created":"2024-12-20","cited_by_count":81,"area":"lr"},{"id":"2502.12289","title":"Evaluating Step-by-step Reasoning Traces: A Survey","created":"2025-02-17","cited_by_count":63,"area":"lr"},{"id":"2604.03789","title":"Automated Conjecture Resolution with Formal Verification","created":"2026-04-04","cited_by_count":28,"area":"lr"},{"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":"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":"2510.15981","title":"ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization","created":"2025-10-13","cited_by_count":21,"area":null},{"id":"2505.20613","title":"REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning","created":"2025-05-27","cited_by_count":18,"area":"lr"},{"id":"2506.07047","title":"Mathesis: Towards Formal Theorem Proving from Natural Languages","created":"2025-06-08","cited_by_count":18,"area":null},{"id":"2510.13888","title":"Reliable Fine-Grained Evaluation of Natural Language Math Proofs","created":"2025-10-14","cited_by_count":18,"area":"lr"},{"id":"2510.15681","title":"ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings","created":"2025-10-17","cited_by_count":18,"area":"rag"},{"id":"2506.11487","title":"Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models","created":"2025-06-13","cited_by_count":17,"area":"lr"},{"id":"2508.04440","title":"StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion","created":"2025-08-06","cited_by_count":16,"area":"lr"},{"id":"2602.17016","title":"M2F: Automated Formalization of Mathematical Literature at Scale","created":"2026-02-19","cited_by_count":15,"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":"2606.05400","title":"LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization","created":"2026-06-03","cited_by_count":12,"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.13137","title":"LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving","created":"2026-05-13","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":"2510.15940","title":"Lean Finder: Semantic Search for Mathlib That Understands User Intents","created":"2025-10-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":"2602.02990","title":"Learning to Repair Lean Proofs from Compiler Feedback","created":"2026-02-03","cited_by_count":7,"area":"agents"},{"id":"2603.12744","title":"TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib?","created":"2026-03-13","cited_by_count":6,"area":null},{"id":"2508.06931","title":"Automated Formalization via Conceptual Retrieval-Augmented LLMs","created":"2025-08-09","cited_by_count":5,"area":"rag"},{"id":"2608.10916","title":"FaithformBench: Benchmarking Faithfulness of Mathematical Chain-of-Thought Autoformalisation","created":"2026-08-11","cited_by_count":5,"area":"lr"},{"id":"2506.08321","title":"LeanTutor: Towards a Verified AI Mathematical Proof Tutor","created":"2025-06-10","cited_by_count":4,"area":null},{"id":"2602.02561","title":"MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics","created":"2026-01-30","cited_by_count":4,"area":"lr"},{"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,"area":"lr"},{"id":"2607.04655","title":"FormalRx: Rectify and eXamine Semantic Failures in Autoformalization","created":"2026-07-06","cited_by_count":4,"area":"lr"},{"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":"2607.13292","title":"Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases","created":"2026-07-14","cited_by_count":3,"area":null},{"id":"2604.01483","title":"Type-Checked Compliance: Deterministic Guardrails for Agentic Financial Systems Using Lean 4 Theorem Proving","created":"2026-04-01","cited_by_count":2,"area":"agents"},{"id":"2505.18492","title":"Formally Solving Answer-Construction Problems in Lean","created":"2025-05-24","cited_by_count":1,"area":"lr"},{"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":"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":"2509.09726","title":"Natural Language Translation of Formal Proofs through Informalization of Proof Steps and Recursive Summarization along Proof Structure","created":"2025-09-10","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":"2601.06795","title":"GDEPO: Group Dual-dynamic and Equal-right Advantage Policy Optimization with Enhanced Training Data Utilization for Sample-Constrained Reinforcement Learning","created":"2026-01-11","cited_by_count":1,"area":"lr"},{"id":"2601.17332","title":"TheoremForge: Scaling up Formal Data Synthesis with Low-Budget Agentic Workflow","created":"2026-01-24","cited_by_count":1,"area":"agents"},{"id":"2601.23166","title":"Monotonic Reference-Free Refinement for Autoformalization","created":"2026-01-30","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":"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":"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":"2608.25220","title":"FLARE: Verifying MILP Reformulations with LLM-Based Theorem Proving","created":"2026-08-25","cited_by_count":1,"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":"2601.17473","title":"LeanTutor: Towards a Verified AI Mathematical Proof Tutor","created":"2026-01-24","cited_by_count":0,"area":null},{"id":"2604.13515","title":"SFT-GRPO Data Overlap as a Post-Training Hyperparameter for Autoformalization","created":"2026-04-15","cited_by_count":0,"area":"lr"},{"id":"2604.16538","title":"Understanding Tool-Augmented Agents for Lean Formalization: A Factorial Analysis","created":"2026-04-16","cited_by_count":0,"area":"agents"},{"id":"2606.02588","title":"Lean-GAP: A Dataset of Formalized Graduate Algebra Problems","created":"2026-05-20","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.06820","title":"Evaluating SageMath-Augmented LLM Agents for Computational and Experimental Mathematics","created":"2026-07-07","cited_by_count":0,"area":"agents"},{"id":"2608.25449","title":"MathAdv: What Theorem Provers Know, Reason, Formalize, and Generalize","created":"2026-08-26","cited_by_count":0,"area":"lr"},{"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":"2609.38384","title":"LeanPolish: Verified Supervision for Lean Proof Compression","created":"2026-09-29","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.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}