SorryDB: Can AI Provers Complete Real-World Lean Theorems? (FM 2026 - Workshop: AIPV)

Who

Austin Letson, Leopoldo Sarra, Auguste Poiroux, Oliver Dressler, Paul Lezeau, Dhyan Aranha, Frederik Pu, Aaron Hill, Miguel Corredera Hidalgo, Julian Berman, George Tsoukalas, Lenny Taelman

Track

FM 2026 Workshop: AIPV

Time Zone

The program is currently displayed in (GMT+09:00) Osaka, Sapporo, Tokyo.

Use conference time zone: (GMT+09:00) Osaka, Sapporo, TokyoSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

When

Tue 19 May 2026 11:40 - 12:00 at 1F Room 101-103 - AIPV Day 2 Session 2 Lean

Austin Letson

Axiomatic AI

Spain

Leopoldo Sarra

Axiomatic AI

Spain

Auguste Poiroux

Math, Inc; EPFL

Switzerland

Oliver Dressler

--

Germany

Paul Lezeau

Imperial College; The London School of Geometry and NumberTheory

United Kingdom

Dhyan Aranha

University of Amsterdam; Cote d'Azur University

Netherlands

Frederik Pu

University of Toronto

Canada

Aaron Hill

---

United States

Miguel Corredera Hidalgo

ENSEIRB-MATMECA, INP-Bordeaux

France

Julian Berman

Columbia University

United States

George Tsoukalas

The University of Texas at Austin

United States

Lenny Taelman

University of Amsterdam

Netherlands

Time Zone

The program is currently displayed in (GMT+09:00) Osaka, Sapporo, Tokyo.

Use conference time zone: (GMT+09:00) Osaka, Sapporo, TokyoSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

Display full programSpecify a time band

Save

Session Program

Tue 19 May
Displayed time zone: Osaka, Sapporo, Tokyo change

11:00 - 12:20	AIPV Day 2 Session 2 LeanWorkshop: AIPV at 1F Room 101-103

11:00 20m Talk		Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium Workshop: AIPV Vasily Ilin Axiom Math Pre-print
11:20 20m Talk		Lean Atlas: An Integrated Proof Environment for Scalable Human-AI Collaborative Formalization Workshop: AIPV Banri Yanahama Nyx Foundation, Akiyoshi Sannai Kyoto University Pre-print
11:40 20m Talk		SorryDB: Can AI Provers Complete Real-World Lean Theorems? Workshop: AIPV Austin Letson Axiomatic AI, Leopoldo Sarra Axiomatic AI, Auguste Poiroux Math, Inc; EPFL, Oliver Dressler --, Paul Lezeau Imperial College; The London School of Geometry and NumberTheory, Dhyan Aranha University of Amsterdam; Cote d'Azur University, Frederik Pu University of Toronto, Aaron Hill ---, Miguel Corredera Hidalgo ENSEIRB-MATMECA, INP-Bordeaux, Julian Berman Columbia University, George Tsoukalas The University of Texas at Austin, Lenny Taelman University of Amsterdam
12:00 20m Talk		Sponsor Talk by Jimmy Shin, AxiomMath.ai: AXLE: Free, Public Lean 4 Tooling for AI-Driven Mathematics Workshop: AIPV