Lean Together 2025

logic in computer science mathematical software Mathematics

Audience:	Researchers in the discipline
Conference dates:	Tue Jan 14 to Fri Jan 17
Organizers:	Jireh Loreaux, Riccardo Brasca, Kevin Buzzard*
	*contact for this listing

Most of the talks from the conference are available on YouTube: www.youtube.com/watch?v=ZPPDktjL1Lw&list=PLlF-CfQhukNlzXdQvu1SVt9vcD4--fLlg

Upcoming talks

Past talks

Your time			Speaker	Title
Fri	Jan 17	18:30	Social Time	Gather Town
Fri	Jan 17	18:00	Yuma Mizuno	Metaprogramming on monoidal categories
Fri	Jan 17	17:30	David Kurniadi Angdinata	Division polynomials of elliptic curves
Fri	Jan 17	17:00	Joseph Tooby-Smith	Physics and Lean
Fri	Jan 17	16:30	Hannah Fechtner	Braid Groups in Lean
Fri	Jan 17	16:00	Social Time	Gather Town
Fri	Jan 17	15:30	Christian Merten	Formalizing the Bruhat-Tits tree
Fri	Jan 17	15:00	Alex Kontorovich	Complex Analysis and PrimeNumberTheorem+ in Lean
Thu	Jan 16	20:30	Leni Aniva	Pantograph: A Machine-to-Machine Interaction Interface for Lean 4
Thu	Jan 16	20:00	Jack McKoen	Toward functor quasi-categories in Lean
Thu	Jan 16	19:30	Social Time	Gather Town
Thu	Jan 16	19:00	Abdalrhman Mohamed	lean-SMT
Thu	Jan 16	18:30	Jean-Baptiste Tristan	Verified Foundations for Differential Privacy
Thu	Jan 16	18:00	Social hour	Gather Town
Thu	Jan 16	17:30	Marcus Rossel	Egg: An Equality Saturation Tactic in Lean
Thu	Jan 16	17:00	Floris van Doorn	Progress report on the Carleson Project
Thu	Jan 16	16:30	Social Time	Gather Town
Thu	Jan 16	16:00	Michael Rothgang	Scaling mathlib: tooling and automation for an ever-growing mathematics library
Wed	Jan 15	17:00	Violeta Hernández Palacios	A Nimble Introduction to Nimbers
Wed	Jan 15	16:30	Lorenzo Luccioli	Information theory in Lean: the DPI
Wed	Jan 15	16:00	Henrik Böving	Automated Bit-Level Reasoning in Lean 4
Wed	Jan 15	15:30	Social Time	Gather Town
Wed	Jan 15	15:00	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?
Wed	Jan 15	14:30	Joseph Rotella	Programming with Dependently Typed Tables in Lean
Wed	Jan 15	14:00	Social Time	Gather Town
Wed	Jan 15	13:30	Jakob von Raumer	Building a Formal Verification Framework for Smart Contracts
Wed	Jan 15	13:00	Siddhartha Gadgil	Real world Autoformalization
Wed	Jan 15	12:30	Scott Carnahan	Vertex algebras in Mathlib: coming soon?
Tue	Jan 14	19:00	Social Time	Gather Town
Tue	Jan 14	18:30	David Renshaw	Searching for Proof Improvements with tryAtEachStep
Tue	Jan 14	17:30	Lean FRO	The Lean FRO Year 2 Roadmap and Vision
Tue	Jan 14	17:15	Social Time	Gather Town
Tue	Jan 14	16:30	Daniel Weber, Vlad Tsyrklevich	Equational Theories Project
Tue	Jan 14	16:00	Emily Riehl	The ∞-cosmos project: formalizing 1-, 2-, V-, and ∞-category theory in Lean
Tue	Jan 14	15:45	Social Time	Gather Town
Tue	Jan 14	15:15	Xavier Généreux and Jannis Limperg	Efficient Forward Reasoning for Aesop
Tue	Jan 14	14:45	Damiano Testa	An introduction to linters
Tue	Jan 14	14:15	Oliver Nash	Root systems and root data in Mathlib
Tue	Jan 14	14:00	Jireh Loreaux	Welcome

Embed this schedule

Export series to