{"total":95,"rows":[{"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":"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":"2411.17501","title":"The Limits of Inference Scaling Through Resampling","created":"2024-11-26","cited_by_count":53,"area":null},{"id":"2407.00379","title":"GraphArena: Evaluating and Exploring Large Language Models on Graph Computation","created":"2024-06-29","cited_by_count":49,"area":null},{"id":"2504.13139","title":"Syntactic and Semantic Control of Large Language Models via Sequential Monte Carlo","created":"2025-04-17","cited_by_count":46,"area":null},{"id":"2410.15700","title":"InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Search","created":"2024-10-21","cited_by_count":34,"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":"2504.05410","title":"Fast Controlled Generation from Language Models with Adaptive Weighted Rejection Sampling","created":"2025-04-07","cited_by_count":21,"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":"2502.05714","title":"Proving the Coding Interview: A Benchmark for Formally Verified Code Generation","created":"2025-02-08","cited_by_count":19,"area":null},{"id":"2408.11172","title":"SubgoalXL: Subgoal-based Expert Learning for Theorem Proving","created":"2024-08-20","cited_by_count":11,"area":null},{"id":"2501.18310","title":"ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis","created":"2025-01-30","cited_by_count":11,"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":"2605.29955","title":"Formalizing Mathematics at Scale","created":"2026-05-28","cited_by_count":10,"area":null},{"id":"2508.18914","title":"FormaRL: Enhancing Autoformalization with no Labeled Data","created":"2025-08-26","cited_by_count":9,"area":null},{"id":"2502.02558","title":"Particle Trajectory Representation Learning with Masked Point Modeling","created":"2025-02-04","cited_by_count":8,"area":null},{"id":"2503.01424","title":"From Hypothesis to Publication: A Comprehensive Survey of AI-Driven Research Support Systems","created":"2025-03-03","cited_by_count":8,"area":null},{"id":"2505.24264","title":"Faithful and Robust LLM-Driven Theorem Proving for NLI Explanations","created":"2025-05-30","cited_by_count":8,"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":"2412.17743","title":"YuLan-Mini: An Open Data-efficient Language Model","created":"2024-12-23","cited_by_count":7,"area":null},{"id":"2508.05242","title":"CodeBoost: Boosting Code LLMs by Squeezing Knowledge from Code Snippets with RL","created":"2025-08-07","cited_by_count":7,"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":"2411.18872","title":"A Lean Dataset for International Math Olympiad: Small Steps towards Writing Math Proofs for Hard Problems","created":"2024-11-28","cited_by_count":6,"area":null},{"id":"2506.07477","title":"Premise Selection for a Lean Hammer","created":"2025-06-09","cited_by_count":6,"area":null},{"id":"2509.08653","title":"Generative Data Refinement: Just Ask for Better Data","created":"2025-09-10","cited_by_count":6,"area":null},{"id":"2601.03764","title":"Learning Shrinks the Hard Tail: Training-Dependent Inference Scaling in a Solvable Linear Model","created":"2026-01-07","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":"2504.17017","title":"Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification","created":"2025-04-23","cited_by_count":5,"area":null},{"id":"2505.15993","title":"Explaining Puzzle Solutions in Natural Language: An Exploratory Study on 6x6 Sudoku","created":"2025-05-21","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":"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":"2609.19134","title":"ScienceIDE: Turning World's Scientific Codebase into Agent Learnable Environments","created":"2026-09-16","cited_by_count":4,"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":"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.15737","title":"PhysProver: Advancing Automatic Theorem Proving for Physics","created":"2026-01-22","cited_by_count":3,"area":null},{"id":"2605.30333","title":"COMPOSE: Composing Future Theorems from Citations and Formal Structure","created":"2026-05-28","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":"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":"2507.08425","title":"A Survey of Large Language Models in Discipline-specific Research: Challenges, Methods and Opportunities","created":"2025-07-11","cited_by_count":2,"area":null},{"id":"2510.09316","title":"A Survey of LLM Prompt Datasets: Taxonomy, Linguistic Patterns, and Practical Uses","created":"2025-10-10","cited_by_count":2,"area":null},{"id":"2601.14304","title":"Guided by the Plan: Enhancing Faithful Autoregressive Text-to-Audio Generation with Guided Decoding","created":"2026-01-18","cited_by_count":2,"area":null},{"id":"2601.22365","title":"Towards Solving the Gilbert-Pollak Conjecture via Large Language Models","created":"2026-01-29","cited_by_count":2,"area":null},{"id":"2606.14688","title":"Flood and Harvest: The Provable Necessity of Trivia for Generating Valuable Mathematics via the Lens of Language Generation in the Limit","created":"2026-06-12","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.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":"2410.02666","title":"AlphaIntegrator: Transformer Action Search for Symbolic Integration Proofs","created":"2024-10-03","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":"2504.20010","title":"Towards Automated Scoping of AI for Social Good Projects","created":"2025-04-28","cited_by_count":1,"area":null},{"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":"2510.23637","title":"Combining Textual and Structural Information for Premise Selection in Lean","created":"2025-10-24","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.00097","title":"Gold-Medal-Level Olympiad Geometry Solving with Efficient Heuristic Auxiliary Constructions","created":"2025-11-27","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":"2512.18682","title":"Solver-Independent Automated Problem Formulation via LLMs for High-Cost Simulation-Driven Design","created":"2025-12-21","cited_by_count":1,"area":null},{"id":"2601.07654","title":"Towards Automating Blockchain Consensus Verification with IsabeLLM","created":"2026-01-12","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":"2603.04852","title":"Non-Parametric Structural Priors for Geometry Theorem Prediction","created":"2026-03-05","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":"2606.13892","title":"Crypto x AI, AI x Crypto: A Survey","created":"2026-06-11","cited_by_count":1,"area":null},{"id":"2606.18098","title":"IsabeLLM: Automated Theorem Proving Applied to Formally Verifying Consensus","created":"2026-06-16","cited_by_count":1,"area":null},{"id":"2607.04631","title":"Formal Disco: Scalable Open-Ended Generation of Formally Verified Programs","created":"2026-07-06","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.19407","title":"ITPEval: Benchmarking Formal Translation Across Interactive Theorem Provers","created":"2026-07-07","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":"2607.28632","title":"LLM Framework for Discovering Major Mathematical Conjectures: AI's Quest for the Next Riemann Hypothesis","created":"2026-04-19","cited_by_count":1,"area":null},{"id":"2508.14294","title":"Explaining Hitori Puzzles: Neurosymbolic Proof Staging for Sequential Decisions","created":"2025-08-19","cited_by_count":0,"area":null},{"id":"2509.05331","title":"ForensicsData: A Digital Forensics Dataset for Large Language Models","created":"2025-08-31","cited_by_count":0,"area":null},{"id":"2602.18767","title":"Nazrin: An Atomic Neural Proof Automation Tactic in Lean 4","created":"2026-02-21","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":"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.20120","title":"Using Aristotle API for AI-Assisted Theorem Proving in Lean 4: A Formalisation Case Study of the Grasshopper Problem","created":"2026-05-19","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.02588","title":"Lean-GAP: A Dataset of Formalized Graduate Algebra Problems","created":"2026-05-20","cited_by_count":0,"area":null},{"id":"2606.05729","title":"Automated Proving of Shannon-Type Entropy Inequalities via Fine-Tuned Language Models and Guided Tree Search","created":"2026-06-04","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.16997","title":"PriorProof: A Point-in-Time Measure of Technique Novelty for Formal Proofs","created":"2026-07-18","cited_by_count":0,"area":null},{"id":"2608.05148","title":"Reasoning Core: Designing Broad Procedural Data for Completion-Supervised Reasoning Training","created":"2026-08-05","cited_by_count":0,"area":null},{"id":"2608.12325","title":"Position: Reasoning is a Learnable Rule-Based Process","created":"2026-05-29","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":"2609.27833","title":"From Reasoning Strings to Partial Orders: Verifier-Certified Rule Transport through Quotient Policy Optimization","created":"2026-08-20","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.34960","title":"ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimization","created":"2026-09-28","cited_by_count":0,"area":null},{"id":"2610.08246","title":"LeanPlan: Optimal Planning with LLM-Generated Heuristics and Admissibility Proofs","created":"2026-10-06","cited_by_count":0,"area":null},{"id":"2610.08319","title":"SCOPE: Certified Theorem Proving with a Language Model as the Policy Planner","created":"2026-10-06","cited_by_count":0,"area":null},{"id":"2610.09401","title":"Let the Library Speak: Self-Advertised Method Selection for Formal Proving","created":"2026-10-07","cited_by_count":0,"area":null},{"id":"2610.11605","title":"NanoProof: Open and Efficient Automated Theorem Proving in Lean 4","created":"2026-10-08","cited_by_count":0,"area":null},{"id":"2610.11620","title":"Where to Adapt Matters: Layer-Selective Fine-Tuning for Capability Retention","created":"2026-10-08","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}],"next_cursor":null}