Cover Image

Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Lin, Yong, Tang, Shange, Lyu, Bohan, Wu, Jiayun, Lin, Hongzhou, Yang, Kaiyu, Li, Jia, Xia, Mengzhou, Chen, Danqi, Arora, Sanjeev, Jin, Chi
Format:	Preprint
Published:	2025
Subjects:	Machine Learning Artificial Intelligence
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction
by: Lin, Yong, et al.
Published: (2025)

Ineq-Comp: Benchmarking Human-Intuitive Compositional Reasoning in Automated Theorem Proving on Inequalities
by: Zhao, Haoyu, et al.
Published: (2025)

Awakening the Sleeping Agent: Lean-Specific Agentic Data Reactivates General Tool Use in Goedel Prover
by: Chung, Jui-Hui, et al.
Published: (2026)

Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification
by: Li, Zenan, et al.
Published: (2026)

Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving
by: Chen, Luoxin, et al.
Published: (2025)

LESS: Selecting Influential Data for Targeted Instruction Tuning
by: Xia, Mengzhou, et al.
Published: (2024)

Benign Overfitting in Out-of-Distribution Generalization of Linear Models
by: Tang, Shange, et al.
Published: (2024)

EvolProver: Advancing Automated Theorem Proving by Evolving Formalized Problems via Symmetry and Difficulty
by: Tian, Yuchen, et al.
Published: (2025)

Proving Properties of $φ$-Representations with the Walnut Theorem-Prover
by: Shallit, Jeffrey
Published: (2023)

PhysProver: Advancing Automatic Theorem Proving for Physics
by: Zhang, Hanning, et al.
Published: (2026)

InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Search
by: Wu, Zijian, et al.
Published: (2024)

EconProver: Towards More Economical Test-Time Scaling for Automated Theorem Proving
by: Li, Mukai, et al.
Published: (2025)

Rethinking Mixture-of-Agents: Is Mixing Different Large Language Models Beneficial?
by: Li, Wenzhe, et al.
Published: (2025)

HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving
by: Li, Yang, et al.
Published: (2024)

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

Trainable Transformer in Transformer
by: Panigrahi, Abhishek, et al.
Published: (2023)

SimPO: Simple Preference Optimization with a Reference-Free Reward
by: Meng, Yu, et al.
Published: (2024)

BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving
by: Xin, Ran, et al.
Published: (2025)

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

HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement
by: Hu, Jilin, et al.
Published: (2025)

Is Elo Rating Reliable? A Study Under Model Misspecification
by: Tang, Shange, et al.
Published: (2025)

On Reasoning-Centric LLM-based Automated Theorem Proving
by: Sun, Yican, et al.
Published: (2026)

Open Source Prover in the Attic
by: Kovács, Zoltán, et al.
Published: (2024)

Spark-Prover-X1: Formal Theorem Proving Through Diverse Data Training
by: Zhou, Xinyuan, et al.
Published: (2025)

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

OptProver: Bridging Olympiad and Optimization through Continual Training in Formal Theorem Proving
by: Li, Chenyi, et al.
Published: (2026)

MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation
by: Liang, Zhenwen, et al.
Published: (2025)

Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience
by: Chen, Jiangjie, et al.
Published: (2025)

HHLPar: Automated Theorem Prover for Parallel Hybrid Communicating Sequential Processes
by: Jin, Xiangyu, et al.
Published: (2024)

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

Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics
by: Breen, Benjamin, et al.
Published: (2025)

DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data
by: Xin, Huajian, et al.
Published: (2024)

MATP-BENCH: Can MLLM Be a Good Automated Theorem Prover for Multimodal Problems?
by: He, Zhitao, et al.
Published: (2025)

Sheared LLaMA: Accelerating Language Model Pre-training via Structured Pruning
by: Xia, Mengzhou, et al.
Published: (2023)

Lory: Fully Differentiable Mixture-of-Experts for Autoregressive Language Model Pre-training
by: Zhong, Zexuan, et al.
Published: (2024)

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

Leanabell-Prover-V2: Verifier-integrated Reasoning for Formal Theorem Proving via Reinforcement Learning
by: Ji, Xingguang, et al.
Published: (2025)

DreamProver: Evolving Transferable Lemma Libraries via a Wake-Sleep Theorem-Proving Agent
by: Zhang, Youyuan, et al.
Published: (2026)

Benchmarking Testing in Automated Theorem Proving
by: Kim, Jongyoon, et al.
Published: (2026)

Automated Theorem Proving for Prolog Verification
by: Mesnard, Fred, et al.
Published: (2026)