Imagen de Portada

REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning

Fuente: arXiv

Guardado en:

Detalles Bibliográficos
Autores principales:	Shen, Ziju, Huang, Naohao, Yang, Fanyi, Wang, Yutong, Gao, Guoxiong, Xu, Tianyi, Jiang, Jiedong, He, Wanyi, Yang, Pu, Sun, Mengzhou, Ju, Haocheng, Wu, Peihao, Dai, Bryan, Dong, Bin
Formato:	Preprint
Publicado:	2025
Materias:	Computation and Language Artificial Intelligence Machine Learning Logic in Computer Science
Acceso en línea:	Acceder al recurso
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

Ejemplares similares

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

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

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

Formalizing Automated Market Makers in the Lean 4 Theorem Prover
por: Pusceddu, Daniele, et al.
Publicado: (2024)

A Comprehensive Survey of the Lean 4 Theorem Prover: Architecture, Applications, and Advances
por: Tang, Xichen
Publicado: (2025)

A Semantic Search Engine for Mathlib4
por: Gao, Guoxiong, et al.
Publicado: (2024)

Proof Strategy Extraction from LLMs for Enhancing Symbolic Provers
por: Fang, Jian, et al.
Publicado: (2025)

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

Theorem Provers: One Size Fits All?
por: Oates, Harrison, et al.
Publicado: (2025)

PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition
por: Tsoukalas, George, et al.
Publicado: (2024)

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

A Rust-to-Lean Verification Pipeline with AI Provers: An Experience Report
por: Klaus, Natalia, et al.
Publicado: (2026)

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

SMLP: Symbolic Machine Learning Prover
por: Brauße, Franz, et al.
Publicado: (2024)

Elenchus: Generating Knowledge Bases from Prover-Skeptic Dialogues
por: Allen, Bradley P.
Publicado: (2026)

SMLP: Symbolic Machine Learning Prover (User Manual)
por: Brauße, Franz, et al.
Publicado: (2024)

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

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

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

DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search
por: Xin, Huajian, et al.
Publicado: (2024)

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

ImProver 2: Iteratively Self-Improving LMs for Neurosymbolic Proof Optimization
por: Ahuja, Riyaz, et al.
Publicado: (2026)

Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs
por: Li, Guchan, et al.
Publicado: (2026)

FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levels
por: Jiang, Jiedong, et al.
Publicado: (2025)

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

ScenicProver: A Framework for Compositional Probabilistic Verification of Learning-Enabled Systems
por: Vin, Eric, et al.
Publicado: (2025)

Construction-Verification: A Benchmark for Applied Mathematics in Lean 4
por: Yang, Bowen, et al.
Publicado: (2026)

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

OnlineProver: Experience with a Visualisation Tool for Teaching Formal Proofs
por: Perháč, Ján, et al.
Publicado: (2025)

LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving
por: Gao, Guoxiong, et al.
Publicado: (2026)

Understanding and Improving Automated Proof Synthesis for Interactive Theorem Provers
por: Zhang, Manqing, et al.
Publicado: (2026)

LeanCat: A Benchmark Suite for Formal Category Theory in Lean (Part I: 1-Categories)
por: Xu, Rongge, et al.
Publicado: (2025)

Lean-SMT: An SMT tactic for discharging proof goals in Lean
por: Mohamed, Abdalrhman, et al.
Publicado: (2025)

Automated Tactics for Polynomial Reasoning in Lean 4
por: Shen, Hao, et al.
Publicado: (2026)

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

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

CSLibPremiseBench: Structure-Guided Premise Retrieval and Label Robustness for Lean 4 Computer-Science Theorems
por: Ji, Junye
Publicado: (2026)

Meta-Mathematics of Computational Complexity Theory
por: Oliveira, Igor C.
Publicado: (2025)

Kimina Lean Server: A High-Performance Lean Server for Large-Scale Verification
por: Santos, Marco Dos, et al.
Publicado: (2025)

Intuitionistic Propositional Logic in Lean
por: Trufaş, Dafina
Publicado: (2024)