Cover Image

Discovering New Theorems via LLMs with In-Context Proof Learning in Lean

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Kasaura, Kazumi, Onda, Naoto, Oriike, Yuta, Taniguchi, Masaya, Sannai, Akiyoshi, Sonoda, Sho
Format:	Preprint
Published:	2025
Subjects:	Machine Learning Artificial Intelligence Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem Proving
by: Onda, Naoto, et al.
Published: (2025)

Lean Atlas: An Integrated Proof Environment for Scalable Human-AI Collaborative Formalization
by: Yanahama, Banri, et al.
Published: (2026)

Generating Millions Of Lean Theorems With Proofs By Exploring State Transition Graphs
by: Yin, David, et al.
Published: (2025)

Lean Formalization of Generalization Error Bound by Rademacher Complexity and Dudley's Entropy Integral
by: Sonoda, Sho, et al.
Published: (2025)

PBLean: Pseudo-Boolean Proof Certificates for Lean 4
by: Szeider, Stefan
Published: (2026)

Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4
by: Liu, Chengwu, et al.
Published: (2026)

LeanAgent: Lifelong Learning for Formal Theorem Proving
by: Kumarappan, Adarsh, et al.
Published: (2024)

Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean
by: Song, Peiyang, et al.
Published: (2024)

Keep the Proof State Live: Snapshotting for Efficient Tactic Search in Lean 4
by: Shen, Austin, et al.
Published: (2026)

Proof Recommendation System for the HOL4 Theorem Prover
by: Dekhil, Nour, et al.
Published: (2024)

LeanTutor: Towards a Verified AI Mathematical Proof Tutor
by: Patel, Manooshree, et al.
Published: (2025)

Stress-Testing the Reasoning Competence of LLMs With Proofs Under Minimal Formalism
by: Arkoudas, Konstantine, et al.
Published: (2026)

Compactness in Constructive Mathematics via Affine Logic
by: Kasaura, Kazumi
Published: (2026)

Exponential Sample Complexity Separation between Flat and Hierarchical Agentic Theorem Provers
by: Sonoda, Sho, et al.
Published: (2026)

An Automated Theorem Generator with Theoretical Foundation Based on Rectangular Standard Contradiction
by: Xu, Yang, et al.
Published: (2025)

Partial Label Learning for Automated Theorem Proving
by: Zombori, Zsolt, et al.
Published: (2025)

ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving
by: Thakur, Amitayush, et al.
Published: (2025)

The Axiom-Based Atlas: A Structural Mapping of Theorems via Foundational Proof Vectors
by: Yoo, Harim
Published: (2025)

APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning
by: Ospanov, Azim, et al.
Published: (2025)

Translating Informal Proofs into Formal Proofs Using a Chain of States
by: Wang, Ziyu, et al.
Published: (2025)

ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization
by: Cabral, Rafael, et al.
Published: (2025)

An In-Context Learning Agent for Formal Theorem-Proving
by: Thakur, Amitayush, et al.
Published: (2023)

Investigations into Proof Structures
by: Wernhard, Christoph, et al.
Published: (2023)

Towards Advanced Mathematical Reasoning for LLMs via First-Order Logic Theorem Proving
by: Cao, Chuxue, et al.
Published: (2025)

Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search
by: Lu, Jialin, et al.
Published: (2026)

An Undecidability Proof for the Plan Existence Problem
by: Achilleos, Antonis
Published: (2026)

Large Language Model for OWL Proofs
by: Yang, Hui, et al.
Published: (2026)

Premise Selection for a Lean Hammer
by: Zhu, Thomas, et al.
Published: (2025)

Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs
by: Zhang, Terry Jingchen, et al.
Published: (2025)

Logical Lease Litigation: Prolog and LLMs for Rental Law Compliance in New York
by: Sehgal, Sanskar, et al.
Published: (2025)

Vibe Coding an LLM-powered Theorem Prover
by: Hou, Zhe
Published: (2026)

Abstraction-Based Proof Production in Formal Verification of Neural Networks
by: Elboher, Yizhak Yisrael, et al.
Published: (2025)

StepProof: Step-by-step verification of natural language mathematical proofs
by: Hu, Xiaolin, et al.
Published: (2025)

TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib?
by: Taylor, Alexander K, et al.
Published: (2026)

Simplifying Formal Proof-Generating Models with ChatGPT and Basic Searching Techniques
by: Han, Sangjun, et al.
Published: (2025)

Automated Completion of Statements and Proofs in Synthetic Geometry: an Approach based on Constraint Solving
by: Gonzalez, Salwa Tabet, et al.
Published: (2024)

Risk-Controlled Lean-as-Judge for Natural-Language Mathematical Reasoning
by: Bourigault, Pauline, et al.
Published: (2026)

3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes
by: Lamont, Sean, et al.
Published: (2024)

Proceedings 19th International Workshop on the ACL2 Theorem Prover and Its Applications
by: Gamboa, Ruben, et al.
Published: (2025)

The mechanization of science illustrated by the Lean formalization of the multi-graded Proj construction
by: Mayeux, Arnaud, et al.
Published: (2025)