Imagen de Portada

Generating Millions Of Lean Theorems With Proofs By Exploring State Transition Graphs

Fuente: arXiv

Guardado en:

Detalles Bibliográficos
Autores principales:	Yin, David, Gao, Jing
Formato:	Preprint
Publicado:	2025
Materias:	Logic in Computer Science Artificial Intelligence
Acceso en línea:	Acceder al recurso
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

Ejemplares similares

Discovering New Theorems via LLMs with In-Context Proof Learning in Lean
por: Kasaura, Kazumi, et al.
Publicado: (2025)

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

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

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

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

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

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

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

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

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

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

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

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

Investigations into Proof Structures
por: Wernhard, Christoph, et al.
Publicado: (2023)

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

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

An Undecidability Proof for the Plan Existence Problem
por: Achilleos, Antonis
Publicado: (2026)

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

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

Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification
por: Rao, Balaji, et al.
Publicado: (2025)

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

Herald: A Natural Language Annotated Lean 4 Dataset
por: Gao, Guoxiong, et al.
Publicado: (2024)

Vibe Coding an LLM-powered Theorem Prover
por: Hou, Zhe
Publicado: (2026)

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

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

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

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

Policy-Adaptable Methods For Resolving Normative Conflicts Through Argumentation and Graph Colouring
por: Joyce, Johnny
Publicado: (2025)

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

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

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

Combining Textual and Structural Information for Premise Selection in Lean
por: Petrovčič, Job, et al.
Publicado: (2025)

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

Hierarchical Attention Generates Better Proofs
por: Chen, Jianlong, et al.
Publicado: (2025)

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

Generating Theorems by Generating Proof Structures
por: Wernhard, Christoph
Publicado: (2026)

MSC-180: A Benchmark for Automated Formal Theorem Proving from Mathematical Subject Classification
por: Li, Sirui, et al.
Publicado: (2025)

Enhancing Formal Theorem Proving: A Comprehensive Dataset for Training AI Models on Coq Code
por: Florath, Andreas
Publicado: (2024)

Homomorphic Encryption of Intuitionistic Logic Proofs and Functional Programs: A Categorical Approach Inspired by Composite-Order Bilinear Groups
por: Goertzel, Ben
Publicado: (2025)

REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning
por: Shen, Ziju, et al.
Publicado: (2025)