Lean Together 2025
logic in computer science mathematical software Mathematics
| Audience: | Researchers in the discipline |
| Conference dates: | 14-Jan-2025 to 17-Jan-2025 |
| Organizers: | Jireh Loreaux*, Riccardo Brasca*, Kevin Buzzard* |
| *contact for this listing |
Upcoming talks
Past talks
| Your time | Speaker | Title | |||
|---|---|---|---|---|---|
| Tue | Jan 14 | 14:00 | Jireh Loreaux | Welcome | |
| Tue | Jan 14 | 14:15 | Jason Rute | The last mile: How do we make AI theorem provers which work in the real world for real users and not just on benchmarks? | |
| Tue | Jan 14 | 14:45 | Damiano Testa | TBA | |
| Tue | Jan 14 | 15:15 | Xavier Généreux and Jannis Limperg | Efficient Forward Reasoning for Aesop | |
| Tue | Jan 14 | 15:45 | Coffee Break | TBA | |
| Tue | Jan 14 | 16:00 | Emily Riehl | The ∞-cosmos project: formalizing 1-, 2-, V-, and ∞-category theory in Lean | |
| Tue | Jan 14 | 16:30 | Daniel Weber, Vlad Tsyrklevich | Equational Theories Project | |
| Tue | Jan 14 | 17:15 | Coffee Break | TBA | |
| Tue | Jan 14 | 17:30 | Lean FRO | The Lean FRO Year 2 Roadmap and Vision | |
| Tue | Jan 14 | 18:30 | David Renshaw | TBA | |
| Wed | Jan 15 | 12:30 | Scott Carnahan | Vertex algebras in Mathlib: coming soon? | |
| Wed | Jan 15 | 13:00 | Siddhartha Gadgil | Real world Autoformalization | |
| Wed | Jan 15 | 13:30 | Jakob von Raumer | Building a Formal Verification Framework for Smart Contracts | |
| Wed | Jan 15 | 14:00 | Coffee Break | TBA | |
| Wed | Jan 15 | 14:30 | Joseph Rotella | TBA | |
| Wed | Jan 15 | 15:00 | Oliver Nash | Root systems and root data in Mathlib | |
| Wed | Jan 15 | 15:30 | Coffee Break | TBA | |
| Wed | Jan 15 | 16:00 | Henrik Böving | Automated Bit-Level Reasoning in Lean 4 | |
| Wed | Jan 15 | 16:30 | Lorenzo Luccioli | Information theory in Lean: the DPI | |
| Wed | Jan 15 | 17:00 | Violeta Hernández Palacios | TBA | |
| Thu | Jan 16 | 16:00 | Michael Rothgang | TBA | |
| Thu | Jan 16 | 16:30 | Coffee Break | TBA | |
| Thu | Jan 16 | 17:00 | Floris van Doorn | TBA | |
| Thu | Jan 16 | 17:30 | Marcus Rossel | Egg: An Equality Saturation Tactic in Lean | |
| Thu | Jan 16 | 18:00 | Social hour | TBA | |
| Thu | Jan 16 | 18:30 | Jean-Baptiste Tristan | TBA | |
| Thu | Jan 16 | 19:00 | Abdalrhman Mohamed | lean-SMT | |
| Thu | Jan 16 | 19:30 | Coffee Break | TBA | |
| Thu | Jan 16 | 20:00 | Jack McKoen | TBA | |
| Thu | Jan 16 | 20:30 | Leni Aniva | Pantograph and Proof Traces | |
| Fri | Jan 17 | 15:00 | Alex Kontorovich | Educational and research experiments with formalization | |
| Fri | Jan 17 | 15:30 | Christian Merten | Formalizing the Bruhat-Tits tree | |
| Fri | Jan 17 | 16:00 | Coffee Break | TBA | |
| Fri | Jan 17 | 16:30 | Hannah Fechtner | TBA | |
| Fri | Jan 17 | 17:00 | Joseph Tooby-Smith | Formalizing physics into Lean | |
| Fri | Jan 17 | 17:30 | David Kurniadi Angdinata | TBA | |
| Fri | Jan 17 | 18:00 | Yuma Mizuno | Metaprogramming on monoidal categories | |
Export series to