{"total":69,"rows":[{"id":"2303.18223","title":"A Survey of Large Language Models","created":"2023-03-31","cited_by_count":2576,"area":null},{"id":"2210.12283","title":"Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs","created":"2022-10-21","cited_by_count":291,"area":null},{"id":"2205.11491","title":"HyperTree Proof Search for Neural Theorem Proving","created":"2022-05-23","cited_by_count":197,"area":null},{"id":"2204.06031","title":"A Review on Language Models as Knowledge Bases","created":"2022-04-12","cited_by_count":157,"area":null},{"id":"2206.03126","title":"Signal Propagation in Transformers: Theoretical Perspectives and the Role of Rank Collapse","created":"2022-06-07","cited_by_count":141,"area":null},{"id":"2406.16838","title":"From Decoding to Meta-Generation: Inference-time Algorithms for Large Language Models","created":"2024-06-24","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":"2206.04301","title":"Unveiling Transformers with LEGO: a synthetic reasoning task","created":"2022-06-09","cited_by_count":106,"area":null},{"id":"2205.10893","title":"Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers","created":"2022-05-22","cited_by_count":98,"area":null},{"id":"2502.03438","title":"BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving","created":"2025-02-05","cited_by_count":84,"area":null},{"id":"2205.12910","title":"NaturalProver: Grounded Mathematical Proof Generation with Language Models","created":"2022-05-25","cited_by_count":72,"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":"2510.01346","title":"Aristotle: IMO-level Automated Theorem Proving","created":"2025-10-01","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":"2309.04295","title":"FIMO: A Challenge Formal Dataset for Automated Theorem Proving","created":"2023-09-08","cited_by_count":55,"area":null},{"id":"2303.04488","title":"Magnushammer: A Transformer-Based Approach to Premise Selection","created":"2023-03-08","cited_by_count":50,"area":null},{"id":"2407.00695","title":"Learning Formal Mathematics From Intrinsic Motivation","created":"2024-06-30","cited_by_count":45,"area":null},{"id":"2512.17260","title":"Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience","created":"2025-12-19","cited_by_count":44,"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":"2410.15756","title":"Automated Proof Generation for Rust Code via Self-Evolution","created":"2024-10-21","cited_by_count":33,"area":null},{"id":"2405.10313","title":"How Far Are We From AGI: Are LLMs All We Need?","created":"2024-05-16","cited_by_count":31,"area":null},{"id":"2310.18021","title":"FormalGeo: An Extensible Formalized Framework for Olympiad Geometric Problem Solving","created":"2023-10-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":"2502.05567","title":"ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data","created":"2025-02-08","cited_by_count":23,"area":null},{"id":"2406.14219","title":"Proving Olympiad Algebraic Inequalities without Human Demonstrations","created":"2024-06-20","cited_by_count":20,"area":null},{"id":"2206.06315","title":"JiuZhang: A Chinese Pre-trained Language Model for Mathematical Problem Understanding","created":"2022-06-13","cited_by_count":15,"area":null},{"id":"2212.10079","title":"A Survey on Pretrained Language Models for Neural Code Intelligence","created":"2022-12-20","cited_by_count":13,"area":null},{"id":"2305.18577","title":"Towards Constituting Mathematical Structures for Learning to Optimize","created":"2023-05-29","cited_by_count":13,"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":"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.29955","title":"Formalizing Mathematics at Scale","created":"2026-05-28","cited_by_count":10,"area":null},{"id":"2408.10268","title":"Generating Streamlining Constraints with Large Language Models","created":"2024-08-16","cited_by_count":7,"area":null},{"id":"2308.15605","title":"Benchmarks for Detecting Measurement Tampering","created":"2023-08-29","cited_by_count":6,"area":null},{"id":"2405.06677","title":"ATG: Benchmarking Automated Theorem Generation for Generative Language Models","created":"2024-05-05","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":"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":"2503.04763","title":"MiniF2F in Rocq: Automatic Translation Between Proof Assistants -- A Case Study","created":"2025-02-11","cited_by_count":5,"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":"2510.26094","title":"Lean4Physics: Comprehensive Reasoning Framework for College-level Physics in Lean4","created":"2025-10-30","cited_by_count":5,"area":null},{"id":"2311.07618","title":"Large Language Models' Understanding of Math: Source Criticism and Extrapolation","created":"2023-11-12","cited_by_count":4,"area":null},{"id":"2410.15748","title":"Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation","created":"2024-10-21","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":"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":"2606.05632","title":"Evaluation of LLMs for Mathematical Formalization in Lean","created":"2026-06-04","cited_by_count":3,"area":null},{"id":"2312.14188","title":"Enhancing Neural Theorem Proving through Data Augmentation and Dynamic Sampling Method","created":"2023-12-20","cited_by_count":2,"area":null},{"id":"2402.02104","title":"Learning Structure-Aware Representations of Dependent Types","created":"2024-02-03","cited_by_count":2,"area":null},{"id":"2406.18616","title":"Towards Large Language Model Aided Program Refinement","created":"2024-06-26","cited_by_count":2,"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":"2602.04892","title":"Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Induction","created":"2026-01-30","cited_by_count":2,"area":null},{"id":"2209.02562","title":"Project proposal: A modular reinforcement learning based automated theorem prover","created":"2022-09-06","cited_by_count":1,"area":null},{"id":"2212.11353","title":"Contrastive Distillation Is a Sample-Efficient Self-Supervised Loss Policy for Transfer Learning","created":"2022-12-21","cited_by_count":1,"area":null},{"id":"2306.16951","title":"Applying language models to algebraic topology: generating simplicial cycles using multi-labeling in Wu's formula","created":"2023-06-01","cited_by_count":1,"area":null},{"id":"2401.02950","title":"The Tactician's Web of Large-Scale Formal Knowledge","created":"2024-01-05","cited_by_count":1,"area":null},{"id":"2402.08365","title":"Learning Better Representations From Less Data For Propositional Satisfiability","created":"2024-02-13","cited_by_count":1,"area":null},{"id":"2402.09047","title":"FGeo-TP: A Language Model-Enhanced Solver for Geometry Problems","created":"2024-02-14","cited_by_count":1,"area":null},{"id":"2403.05713","title":"tsGT: Stochastic Time Series Modeling With Transformer","created":"2024-03-08","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":"2512.14252","title":"G\\\"odel's Poetry","created":"2025-12-16","cited_by_count":1,"area":null},{"id":"2603.04528","title":"Discovering mathematical concepts through a multi-agent system","created":"2026-03-04","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":"2407.11008","title":"Figuring out Figures: Using Textual References to Caption Scientific Figures","created":"2024-06-25","cited_by_count":0,"area":null},{"id":"2603.13761","title":"Level Up: Defining and Exploiting Transitional Problems for Curriculum Learning","created":"2026-03-14","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.28572","title":"Geometric Measurements of the Axiom of Choice in Neural Proof Embeddings","created":"2026-06-26","cited_by_count":0,"area":null},{"id":"2609.25575","title":"Direct Optimization of Generators for Search in Automated Theorem Proving","created":"2026-09-22","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}],"next_cursor":null}