Copertina

SorryDB: Can AI Provers Complete Real-World Lean Theorems?

Fuente: arXiv

Salvato in:

Dettagli Bibliografici
Autori principali:	Letson, Austin, Sarra, Leopoldo, Poiroux, Auguste, Dressler, Oliver, Lezeau, Paul, Aranha, Dhyan, Pu, Frederick, Hill, Aaron, Hidalgo, Miguel Corredera, Berman, Julian, Tsoukalas, George, Taelman, Lenny
Natura:	Preprint
Pubblicazione:	2026
Soggetti:	Artificial Intelligence Machine Learning
Accesso online:	Acceder al recurso
Tags:	Aggiungi Tag Nessun Tag, puoi essere il primo ad aggiungerne!!

Documenti analoghi

A Minimal Agent for Automated Theorem Proving
di: Requena, Borja, et al.
Pubblicazione: (2026)

RLMEval: Evaluating Research-Level Neural Theorem Proving
di: Poiroux, Auguste, et al.
Pubblicazione: (2025)

The chow weight structure for geometric motives of quotient stacks
di: Aranha, Dhyan, et al.
Pubblicazione: (2023)

Deformations and Lifts of Calabi-Yau Varieties in Characteristic $p$
di: Brantner, Lukas, et al.
Pubblicazione: (2024)

Teaching "Foundations of Mathematics" with the Lean Theorem Prover
di: Bottoni, Mattia Luciano, et al.
Pubblicazione: (2025)

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

Do LLMs Game Formalization? Evaluating Faithfulness in Logical Reasoning
di: Kim, Kyuhee, et al.
Pubblicazione: (2026)

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

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

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

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

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

Reliable Evaluation and Benchmarks for Statement Autoformalization
di: Poiroux, Auguste, et al.
Pubblicazione: (2024)

Inference-Time Diversity in RL-Trained Lean Theorem Provers: A Diagnostic Study
di: Burton, Zachary
Pubblicazione: (2026)

Los conflictos entre Ética, Moral y Política: criterios para su negociación
di: Silverio Sánchez Corredera
Pubblicazione: (2003)

Shaping the Future of Mathematics in the Age of AI
di: Commelin, Johan, et al.
Pubblicazione: (2026)

Virtual localization revisited
di: Aranha, Dhyan, et al.
Pubblicazione: (2022)

The stacky concentration theorem
di: Aranha, Dhyan, et al.
Pubblicazione: (2024)

SOFTWARE PARA FACILITAR EL TRATAMIENTO DE LA ÉTICA MARTIANA EN LA ENSEÑANZA TÉCNICA Y PROFESIONAL
di: Alain Rey Márquez Corredera
Pubblicazione: (2007)

Vibe Coding an LLM-powered Theorem Prover
di: Hou, Zhe
Pubblicazione: (2026)

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

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

Reinforcement learning with learned gadgets to tackle hard quantum problems on real hardware
di: Kundu, Akash, et al.
Pubblicazione: (2024)

CFP-MCFP: Machine-Verified Proofs of Riemann Hypothesis, Goldbach, Yang-Mills, Fermat, Beal, Collatz — Lean 4 Theorem Prover
di: Salden, Alfons H.
Pubblicazione: (2026)

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

Theorem Prover as a Judge for Synthetic Data Generation
di: Leang, Joshua Ong Jun, et al.
Pubblicazione: (2025)

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

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

Land Surface Temperature Dynamics during COVID‐19 Lockdown in Diverse Climatic and Physiographic Zones—A Study of Indian Mega Cities
di: Ashish Mishra, et al.
Pubblicazione: (2024)

LeanGeo: Formalizing Competitional Geometry problems in Lean
di: Song, Chendong, et al.
Pubblicazione: (2025)

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

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

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

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

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

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

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

Automated Theorem Provers Help Improve Large Language Model Reasoning
di: McGinness, Lachlan, et al.
Pubblicazione: (2024)

Joint Embeddings Go Temporal
di: Ennadir, Sofiane, et al.
Pubblicazione: (2025)

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