Cover Image

Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Liu, Chengwu, Yin, Yichun, Yuan, Ye, Xie, Jiaxuan, Li, Botao, Li, Siqi, Shen, Jianhao, Xu, Yan, Shang, Lifeng, Zhang, Ming
Format:	Preprint
Published:	2026
Subjects:	Artificial Intelligence Computation and Language Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Canonical for Automated Theorem Proving in Lean
by: Norman, Chase, et al.
Published: (2025)

MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving
by: Li, Jinzheng, et al.
Published: (2026)

Automated Theorem Proving for Prolog Verification
by: Mesnard, Fred, 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)

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

Nazrin: Atomic Tactics for Graph Neural Networks for Theorem Proving in Lean 4
by: Aniva, Leni, et al.
Published: (2026)

Equational Theorem Proving for Clauses over Strings
by: Kim, Dohan
Published: (2023)

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

Proving Behavioural Apartness
by: Turkenburg, Ruben, et al.
Published: (2024)

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

LLM-Powered Automatic Theorem Proving and Synthesis for Hybrid Systems and Game
by: Kabra, Aditi, et al.
Published: (2026)

Agentic Proving for Program Verification
by: Sosso, Alessandro, et al.
Published: (2026)

Local Look-Ahead Guidance via Verifier-in-the-Loop for Automated Theorem Proving
by: Rajaee, Sara, et al.
Published: (2025)

Type-Checked Compliance: Deterministic Guardrails for Agentic Financial Systems Using Lean 4 Theorem Proving
by: Rashie, Devakh, et al.
Published: (2026)

What are the Right Symmetries for Formal Theorem Proving?
by: Olejniczak, Krzysztof, et al.
Published: (2026)

On the Complexity of Proving Polyhedral Reductions
by: Amat, Nicolas, et al.
Published: (2023)

Twitch: Learning Abstractions for Equational Theorem Proving
by: Axelrod, Guy, et al.
Published: (2026)

Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving
by: Liu, Qi, et al.
Published: (2025)

BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving
by: Lamont, Sean, et al.
Published: (2024)

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

Proving Circuit Functional Equivalence in Zero Knowledge
by: Shen, Sirui, et al.
Published: (2026)

SubgoalXL: Subgoal-based Expert Learning for Theorem Proving
by: Zhao, Xueliang, et al.
Published: (2024)

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

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

Lean-auto: An Interface between Lean 4 and Automated Theorem Provers
by: Qian, Yicheng, et al.
Published: (2025)

Towards Proving Liveness on Weak Memory (Extended Version)
by: Bargmann, Lara, et al.
Published: (2026)

STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
by: Dong, Kefan, et al.
Published: (2025)

Proving Confluence in the Confluence Framework with CONFident
by: Gutiérrez, Raúl, et al.
Published: (2023)

Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4
by: Aniva, Leni, et al.
Published: (2024)

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

Enhancing Neural Theorem Proving through Data Augmentation and Dynamic Sampling Method
by: Vishwakarma, Rahul, et al.
Published: (2023)

Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version)
by: Dardinier, Thibault, et al.
Published: (2023)

Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving
by: An, Chenyang, et al.
Published: (2024)

Process-Driven Autoformalization in Lean 4
by: Lu, Jianqiao, et al.
Published: (2024)

Symbolic Sets for Proving Bounds on Rado Numbers
by: Ahmed, Tanbir, et al.
Published: (2025)

Lyra: Orchestrating Dual Correction in Automated Theorem Proving
by: Zheng, Chuanyang, et al.
Published: (2023)

From Width-Based Model Checking to Width-Based Automated Theorem Proving
by: Oliveira, Mateus de Oliveira, et al.
Published: (2022)

Verifying Quantum Phase Estimation (QPE) using Prove-It
by: Witzel, Wayne M., et al.
Published: (2023)

Expansion Laws for Forward-Reverse, Forward, and Reverse Bisimilarities via Proved Encodings
by: Bernardo, Marco, et al.
Published: (2024)