LEAN — PROGRAM
Days: Saturday, 25 July 2026
Saturday, 25 July 2026
Location:
C6.10
| 09:00-09:30 |
Lean Project Update (abstract) 30 min
1 Lean FRO
|
Location:
C6.10
| 09:30-10:00 |
lean4-skills: Workflows for AI-Assisted Lean Development (abstract) 30 min
1 MIT
|
Location:
C6.10
| 11:00-11:30 |
Implementing Canonical in 185 lines of Lean (abstract) 30 min
1 Carnegie Mellon University
|
| 11:30-12:00 |
Metaprogramming for Formal Semantics: A Lean-Based Specification Tool (abstract) 30 min
1 University of Toronto
|
| 12:00-12:30 |
Reconstructing Proofs from Univariate Cylindrical Algebraic Decomposition in Lean (abstract) 30 min
1 Universidade Federal de Minas Gerais
|
Location:
C6.10
| 14:00-14:30 |
The Mathlib Initiative: past, present, and future (abstract) 30 min
1 Mathlib Initiative
|
Location:
C6.10
| 14:30-15:00 |
Formalizing Drinfeld Modules in Lean (abstract) 30 min
1 LMU München
2 Universität Bonn
|
| 15:00-15:20 |
Automated Root Certification in Lean for Transversal Polynomial Systems (abstract) 20 min
1 Indian Institute of Science, Bengaluru
|
Location:
C6.10
| 16:00-16:30 |
The Curious Case of Sphere Packing in Lean (abstract) 30 min
1 Carnegie Mellon University
|
Location:
C6.10
| 16:30-17:00 |
Formalizing Wu-Ritt Method in Lean 4 (abstract) 30 min
1 Shandong University
2 Academy of Mathematics and Systems Science
3 Sun Yat-sen University
|