{"total":123,"rows":[{"id":"2507.15061","title":"WebShaper: Agentically Data Synthesizing via Information-Seeking Formalization","created":"2025-07-20","cited_by_count":121,"area":null},{"id":"2510.01346","title":"Aristotle: IMO-level Automated Theorem Proving","created":"2025-10-01","cited_by_count":58,"area":null},{"id":"2505.11792","title":"Solver-Informed RL: Grounding Large Language Models for Authentic Optimization Modeling","created":"2025-05-17","cited_by_count":45,"area":null},{"id":"2505.23135","title":"VERINA: Benchmarking Verifiable Code Generation","created":"2025-05-29","cited_by_count":34,"area":null},{"id":"2506.21621","title":"The Open Proof Corpus: A Large-Scale Study of LLM-Generated Mathematical Proofs","created":"2025-06-23","cited_by_count":30,"area":null},{"id":"2511.02872","title":"FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levels","created":"2025-11-04","cited_by_count":27,"area":null},{"id":"2505.23486","title":"Autoformalization in the Era of Large Language Models: A Survey","created":"2025-05-29","cited_by_count":21,"area":null},{"id":"2510.15981","title":"ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization","created":"2025-10-13","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":"2505.17505","title":"L-MTP: Leap Multi-Token Prediction Beyond Adjacent Context for Large Language Models","created":"2025-05-23","cited_by_count":15,"area":null},{"id":"2509.26076","title":"IMProofBench: Benchmarking AI on Research-Level Mathematical Proof Generation","created":"2025-09-30","cited_by_count":13,"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":"2602.09464","title":"AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms","created":"2026-02-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":"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":"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":"2605.13137","title":"LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving","created":"2026-05-13","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":"2511.00796","title":"AReaL-Hex: Accommodating Asynchronous RL Training over Heterogeneous GPUs","created":"2025-11-02","cited_by_count":9,"area":null},{"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,"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":"2510.25427","title":"RLMEval: Evaluating Research-Level Neural Theorem Proving","created":"2025-10-29","cited_by_count":8,"area":null},{"id":"2602.18307","title":"VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Lean","created":"2026-02-20","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.06802","title":"Riemann-Bench: A Benchmark for Moonshot Mathematics","created":"2026-04-08","cited_by_count":8,"area":null},{"id":"2510.00732","title":"EvolProver: Advancing Automated Theorem Proving by Evolving Formalized Problems via Symmetry and Difficulty","created":"2025-10-01","cited_by_count":7,"area":null},{"id":"2510.06857","title":"Autoformalizer with Tool Feedback","created":"2025-10-08","cited_by_count":7,"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":"2603.12744","title":"TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib?","created":"2026-03-13","cited_by_count":6,"area":null},{"id":"2606.14502","title":"From Chatbot to Digital Colleague: The Paradigm Shift Toward Persistent Autonomous AI","created":"2026-06-12","cited_by_count":6,"area":null},{"id":"2505.23851","title":"ASyMOB: Algebraic Symbolic Mathematical Operations Benchmark","created":"2025-05-28","cited_by_count":5,"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.26442","title":"AXLE: A Cloud Infrastructure for Lean 4 Theorem Proving Utilities","created":"2026-06-24","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":"2505.15811","title":"On the creation of narrow AI: hierarchy and nonlocality of neural network skills","created":"2025-05-21","cited_by_count":4,"area":null},{"id":"2505.20573","title":"Collision- and Reachability-Aware Multi-Robot Control with Grounded LLM Planners","created":"2025-05-26","cited_by_count":4,"area":null},{"id":"2512.09443","title":"A Human-AI Collaborative Workflow for Mathematical Discovery: A Case Study in Grover-Compatible Riemannian Optimization","created":"2025-12-10","cited_by_count":4,"area":null},{"id":"2512.24796","title":"LeanCat: A Benchmark Suite for Formal Category Theory in Lean (Part I: 1-Categories)","created":"2025-12-31","cited_by_count":4,"area":null},{"id":"2601.18944","title":"Neural Theorem Proving for Verification Conditions: A Real-World Benchmark","created":"2026-01-26","cited_by_count":4,"area":null},{"id":"2605.23109","title":"Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems","created":"2026-05-22","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":"2506.14794","title":"Assembly of Experts: Linear-time construction of the Chimera LLM variants with emergent and adaptable behaviors","created":"2025-05-31","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":"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.04829","title":"Model-Based and Sample-Efficient AI-Assisted Math Discovery in Sphere Packing","created":"2025-12-04","cited_by_count":3,"area":null},{"id":"2601.15737","title":"PhysProver: Advancing Automatic Theorem Proving for Physics","created":"2026-01-22","cited_by_count":3,"area":null},{"id":"2603.09065","title":"Learning Adaptive LLM Decoding","created":"2026-03-10","cited_by_count":3,"area":null},{"id":"2606.29687","title":"A Machine-Verified Proof of a Quantum-Optimization Conjecture","created":"2026-06-29","cited_by_count":3,"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":"2508.03763","title":"Refine-IQA: Multi-Stage Reinforcement Finetuning for Perceptual Image Quality Assessment","created":"2025-08-04","cited_by_count":2,"area":null},{"id":"2509.14274","title":"Discovering New Theorems via LLMs with In-Context Proof Learning in Lean","created":"2025-09-16","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":"2607.28110","title":"BlueprintRepair: Typed Local Edits for Failed Lean Proof Blueprints","created":"2026-07-30","cited_by_count":2,"area":null},{"id":"2608.09277","title":"P$^{3}$: Joint Program-and-Proof Planning for Verified Code Generation","created":"2026-08-10","cited_by_count":2,"area":null},{"id":"2608.16977","title":"The Problem Is the Problem: Towards Scalable Mathematical Discovery","created":"2026-08-17","cited_by_count":2,"area":null},{"id":"2608.20153","title":"FormalTCS: Benchmarking End-to-End Frontier Formal Theoretical Computer Science Research of Large Language Models","created":"2026-08-20","cited_by_count":2,"area":null},{"id":"2505.07247","title":"SAS-Bench: A Fine-Grained Benchmark for Evaluating Short Answer Scoring with Large Language Models","created":"2025-05-12","cited_by_count":1,"area":null},{"id":"2505.16221","title":"LightRouter: Towards Efficient LLM Collaboration with Minimal Overhead","created":"2025-05-22","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":"2601.15714","title":"Even GPT-5.2 Can't Count to Five: The Case for Zero-Error Horizons in Trustworthy LLMs","created":"2026-01-22","cited_by_count":1,"area":null},{"id":"2601.23166","title":"Monotonic Reference-Free Refinement for Autoformalization","created":"2026-01-30","cited_by_count":1,"area":null},{"id":"2603.03668","title":"Can LLM Aid in Solving Constraints with Inductive Definitions?","created":"2026-03-04","cited_by_count":1,"area":null},{"id":"2603.12183","title":"Proof-Carrying Materials: Falsifiable Safety Certificates for Machine-Learned Interatomic Potentials","created":"2026-03-12","cited_by_count":1,"area":null},{"id":"2603.14147","title":"An Alternative Trajectory for Generative AI","created":"2026-03-14","cited_by_count":1,"area":null},{"id":"2604.16347","title":"Lean Atlas: An Integrated Proof Environment for Scalable Human-AI Collaborative Formalization","created":"2026-03-16","cited_by_count":1,"area":null},{"id":"2604.16804","title":"AutoOR: Scalably Post-training LLMs to Autoformulate Operations Research Problems","created":"2026-04-18","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.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":"2605.04916","title":"A Foundation Model for Zero-Shot Logical Rule Induction","created":"2026-05-06","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":"2605.30628","title":"The Architecture of Errors: From Universal Impossibility to Patch-Local LLM Reliability","created":"2026-05-28","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.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.17289","title":"Nothing from Something: Can a Language Model Discover 0?","created":"2026-06-15","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.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":"2607.14582","title":"MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Research","created":"2026-07-16","cited_by_count":1,"area":null},{"id":"2607.19374","title":"Euclean: Automated Geometry Problem Formalization with Unified Verification in Lean","created":"2026-06-17","cited_by_count":1,"area":null},{"id":"2608.19047","title":"Eureka: Task-Conditioned Meta-Agent Orchestration for Scientific Discovery","created":"2026-08-19","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":"2511.11829","title":"Towards Autoformalization of LLM-generated Outputs for Requirement Verification","created":"2025-11-14","cited_by_count":0,"area":null},{"id":"2511.15259","title":"Efficiency Will Not Lead to Sustainable Reasoning AI","created":"2025-11-19","cited_by_count":0,"area":null},{"id":"2601.16172","title":"Inference-Time Diversity in RL-Trained Lean Theorem Provers: A Diagnostic Study","created":"2026-01-22","cited_by_count":0,"area":null},{"id":"2601.19739","title":"TokenSeek: Memory Efficient Fine Tuning via Instance-Aware Token Ditching","created":"2026-01-27","cited_by_count":0,"area":null},{"id":"2603.20405","title":"Putnam 2025 Problems in Rocq using Opus 4.6 and Rocq-MCP","created":"2026-03-20","cited_by_count":0,"area":null},{"id":"2604.27644","title":"ANCORA: Learning to Question via Manifold-Anchored Self-Play for Verifiable Reasoning","created":"2026-04-30","cited_by_count":0,"area":null},{"id":"2605.04472","title":"Automated Formal Proofs of Combinatorial Identities via Wilf-Zeilberger Guidance and LLMs","created":"2026-05-06","cited_by_count":0,"area":null},{"id":"2605.06184","title":"Teaching LLMs Program Semantics via Symbolic Execution Traces","created":"2026-05-07","cited_by_count":0,"area":null},{"id":"2605.15219","title":"NOVA: Fundamental Limits of Knowledge Discovery Through AI","created":"2026-05-12","cited_by_count":0,"area":null},{"id":"2605.25556","title":"Keep the Proof State Live: Snapshotting for Efficient Tactic Search in Lean 4","created":"2026-05-25","cited_by_count":0,"area":null},{"id":"2605.28512","title":"On Compositional Learning Behaviours in Formal Mathematics","created":"2026-05-27","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.04273","title":"Human agency in initial human-AI proof formalization workflows","created":"2026-06-02","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":"2606.17581","title":"Visored: A Controlled-Natural-Language Prover for LLM-Generated Mathematics","created":"2026-06-16","cited_by_count":0,"area":null},{"id":"2607.04534","title":"Mechanism-level routing failure in LLMs over Lean-verified algebraic structures","created":"2026-07-05","cited_by_count":0,"area":null}],"next_cursor":"100"}