{"total":81,"rows":[{"id":"2206.14858","title":"Solving Quantitative Reasoning Problems with Language Models","created":"2022-06-29","cited_by_count":1392,"area":"lr"},{"id":"2306.15626","title":"LeanDojo: Theorem Proving with Retrieval-Augmented Language Models","created":"2023-06-27","cited_by_count":427,"area":"rag"},{"id":"2205.12615","title":"Autoformalization with Large Language Models","created":"2022-05-25","cited_by_count":263,"area":null},{"id":"2302.12433","title":"ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics","created":"2023-02-24","cited_by_count":192,"area":null},{"id":"2202.01344","title":"Formal Mathematics Statement Curriculum Learning","created":"2022-02-03","cited_by_count":142,"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":"2102.06203","title":"Proof Artifact Co-training for Theorem Proving with Language Models","created":"2021-02-11","cited_by_count":132,"area":"offlinerl"},{"id":"2212.10535","title":"A Survey of Deep Learning for Mathematical Reasoning","created":"2022-12-20","cited_by_count":124,"area":"lr"},{"id":"2310.00656","title":"LEGO-Prover: Neural Theorem Proving with Growing Libraries","created":"2023-10-01","cited_by_count":109,"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":"2104.01112","title":"NaturalProofs: Mathematical Theorem Proving in Natural Language","created":"2021-03-24","cited_by_count":81,"area":null},{"id":"2412.16075","title":"Formal Mathematical Reasoning: A New Frontier in AI","created":"2024-12-20","cited_by_count":81,"area":"lr"},{"id":"2402.08939","title":"Premise Order Matters in Reasoning with Large Language Models","created":"2024-02-14","cited_by_count":72,"area":"lr"},{"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":"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":"2408.03350","title":"miniCTX: Neural Theorem Proving with (Long-)Contexts","created":"2024-08-05","cited_by_count":37,"area":null},{"id":"2410.06209","title":"LeanAgent: Lifelong Learning for Formal Theorem Proving","created":"2024-10-08","cited_by_count":35,"area":"lr"},{"id":"2507.15225","title":"Solving Formal Math Problems by Decomposition and Iterative Reflection","created":"2025-07-21","cited_by_count":35,"area":"lr"},{"id":"2506.19923","title":"Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs","created":"2025-06-24","cited_by_count":31,"area":"agents"},{"id":"2510.12787","title":"Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics","created":"2025-10-14","cited_by_count":31,"area":"lr"},{"id":"2312.07622","title":"Mathematical Language Models: A Survey","created":"2023-12-12","cited_by_count":24,"area":null},{"id":"2409.14274","title":"Proof Automation with Large Language Models","created":"2024-09-22","cited_by_count":22,"area":null},{"id":"2106.09146","title":"Contrastive Reinforcement Learning of Symbolic Reasoning Domains","created":"2021-06-16","cited_by_count":17,"area":null},{"id":"2102.03824","title":"Neural Termination Analysis","created":"2021-02-07","cited_by_count":16,"area":null},{"id":"2106.03906","title":"Learning to Guide a Saturation-Based Theorem Prover","created":"2021-06-07","cited_by_count":15,"area":null},{"id":"2211.15864","title":"Peano: Learning Formal Mathematical Reasoning","created":"2022-11-29","cited_by_count":15,"area":"lr"},{"id":"2503.17726","title":"A Survey on Mathematical Reasoning and Optimization with Large Language Models","created":"2025-03-22","cited_by_count":12,"area":"lr"},{"id":"2404.07382","title":"Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving","created":"2024-04-10","cited_by_count":11,"area":null},{"id":"2102.03529","title":"Vampire With a Brain Is a Good ITP Hammer","created":"2021-02-06","cited_by_count":10,"area":null},{"id":"2304.00994","title":"Machine-Learned Premise Selection for Lean","created":"2023-03-17","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":"2111.12038","title":"Learning Symbolic Rules for Reasoning in Quasi-Natural Language","created":"2021-11-23","cited_by_count":9,"area":null},{"id":"2205.15231","title":"A Survey in Mathematical Language Processing","created":"2022-05-30","cited_by_count":9,"area":null},{"id":"2303.11730","title":"Abstract Visual Reasoning: An Algebraic Approach for Solving Raven's Progressive Matrices","created":"2023-03-21","cited_by_count":9,"area":"lr"},{"id":"2105.14706","title":"The Role of Entropy in Guiding a Connection Prover","created":"2021-05-31","cited_by_count":8,"area":null},{"id":"2205.01981","title":"The Isabelle ENIGMA","created":"2022-05-04","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":"2403.04017","title":"Learning Guided Automated Reasoning: A Brief Survey","created":"2024-03-06","cited_by_count":7,"area":"lr"},{"id":"2405.06677","title":"ATG: Benchmarking Automated Theorem Generation for Generative Language Models","created":"2024-05-05","cited_by_count":6,"area":null},{"id":"2511.17330","title":"Agentic Verification of Software Systems","created":"2025-11-21","cited_by_count":6,"area":"agents"},{"id":"2110.10054","title":"Generating Symbolic Reasoning Problems with Transformer GANs","created":"2021-10-19","cited_by_count":5,"area":null},{"id":"2304.10486","title":"CoProver: A Recommender System for Proof Construction","created":"2023-03-01","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":"2101.09142","title":"A Study of Continuous Vector Representationsfor Theorem Proving","created":"2021-01-22","cited_by_count":4,"area":null},{"id":"2505.22846","title":"RocqStar: Leveraging Similarity-driven Retrieval and Agentic Systems for Rocq generation","created":"2025-05-28","cited_by_count":4,"area":"agents"},{"id":"2303.05854","title":"Lemmas: Generation, Selection, Application","created":"2023-03-10","cited_by_count":3,"area":null},{"id":"2307.09564","title":"Reinforcement Learning and Data-Generation for Syntax-Guided Synthesis","created":"2023-07-13","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":"2605.30333","title":"COMPOSE: Composing Future Theorems from Citations and Formal Structure","created":"2026-05-28","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":"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":"2503.11657","title":"Scaling Natural-Language Graph-Based Test Time Compute for Automated Theorem Proving","created":"2025-02-04","cited_by_count":2,"area":"lr"},{"id":"2509.06809","title":"Saturation-Driven Dataset Generation for LLM Mathematical Reasoning in the TPTP Ecosystem","created":"2025-09-08","cited_by_count":2,"area":"lr"},{"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":"2206.06986","title":"Exploring Representation of Horn Clauses using GNNs (Extended Technical Report)","created":"2022-06-14","cited_by_count":1,"area":null},{"id":"2212.05200","title":"Neural Controller Synthesis for Signal Temporal Logic Specifications Using Encoder-Decoder Structured Networks","created":"2022-12-10","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":"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":"2510.21999","title":"Foundation of Intelligence: Review of Math Word Problems from Human Cognition Perspective","created":"2025-10-24","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":"2606.29894","title":"SABER-Math: Automated Benchmark for Information Retrieval Evaluation in Mathematics","created":"2026-06-29","cited_by_count":1,"area":"agents"},{"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":"2107.09766","title":"Learning Heuristics for Template-based CEGIS of Loop Invariants with Reinforcement Learning","created":"2021-07-16","cited_by_count":0,"area":null},{"id":"2303.00752","title":"Safety without alignment","created":"2023-02-27","cited_by_count":0,"area":null},{"id":"2402.16878","title":"EvoGPT-f: An Evolutionary GPT Framework for Benchmarking Formal Math Languages","created":"2024-02-12","cited_by_count":0,"area":null},{"id":"2403.14690","title":"Incorporating Graph Attention Mechanism into Geometric Problem Solving Based on Deep Reinforcement Learning","created":"2024-03-14","cited_by_count":0,"area":"deeprl"},{"id":"2411.01188","title":"Learning Rules Explaining Interactive Theorem Proving Tactic Prediction","created":"2024-11-02","cited_by_count":0,"area":null},{"id":"2412.18134","title":"Learning Randomized Reductions","created":"2024-12-24","cited_by_count":0,"area":"agents"},{"id":"2507.03314","title":"Partial Label Learning for Automated Theorem Proving","created":"2025-07-04","cited_by_count":0,"area":null},{"id":"2509.08808","title":"Handling Open-Vocabulary Constructs in Formalizing Specifications: Retrieval-Augmented Parsing with Expert Knowledge","created":"2025-09-10","cited_by_count":0,"area":"rag"},{"id":"2512.02677","title":"Exploring Depth Generalization in Large Language Models for Solving Recursive Logic Tasks","created":"2025-12-02","cited_by_count":0,"area":null},{"id":"2605.09012","title":"Re$^2$Math: Benchmarking Theorem Retrieval in Research-Level Mathematics","created":"2026-05-09","cited_by_count":0,"area":"lr"},{"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":"2607.22972","title":"Learned Interventions in Lean 4 grind","created":"2026-07-25","cited_by_count":0,"area":null},{"id":"2608.07540","title":"TREAT: Evaluating Access to Formal Knowledge across Equivalent Mathematical Representations","created":"2026-07-29","cited_by_count":0,"area":null},{"id":"2609.14533","title":"Proving olympiad geometry theorems on a superconducting quantum processor","created":"2026-09-13","cited_by_count":0,"area":null},{"id":"2609.31029","title":"Governed Deduction: Policy-Grounded Premise Authorization Beyond Relevance","created":"2026-09-25","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}],"next_cursor":null}