Lean Together 2026

logic in computer science mathematical software Mathematics

Audience:	Researchers in the discipline
Conference dates:	Mon Jan 19 to Fri Jan 23
Organizer:	Jireh Loreaux*
	*contact for this listing

Upcoming talks

Past talks

Your time			Speaker	Title
Tue	Jan 20	12:30	Moritz Doll	Formalizing Schwartz functions and tempered distributions
Tue	Jan 20	13:00	Fabrizio Montesi	CSLib: The Lean Computer Science Library
Tue	Jan 20	13:30	María Inés de Frutos Fernández	Formalizing the universal divided power algebra
Tue	Jan 20	14:00	Break	Break
Tue	Jan 20	14:30	Sebastian Ullrich	The Lean module system
Tue	Jan 20	15:00	Stefan Kebekus	Project VD: Formalizing Value Distribution Theory of Complex Analysis
Tue	Jan 20	15:30	Break	Break
Tue	Jan 20	16:00	Sebastian Graf	Simpler $\texttt{do}$ proofs with $\texttt{mvcgen}$
Tue	Jan 20	16:30	David Ledvinka	Formalization of Brownian Motion in Lean
Tue	Jan 20	17:00	Harry Goldstein	Metaprogramming the Next Generation of Testing Tools
Wed	Jan 21	16:00	Markus Himmel, Sofia Rodrigues	What's new in the Lean standard library
Wed	Jan 21	16:30	Break	Break
Wed	Jan 21	17:00	Jovan Gerbscheid	New tools for theorem proving in Lean
Wed	Jan 21	17:30	Sophie Morel	TBA
Wed	Jan 21	18:00	Break	Break
Wed	Jan 21	18:30	Thomas R. Murrills	Better living through metaprogramming: Solving the Goldblum Dilemma with cotools
Wed	Jan 21	19:00	Sidharth Hariharan, Seewoo Lee, Chris Birkbeck	Progress on the Sphere Packing Project
Wed	Jan 21	19:30	Break	Break
Wed	Jan 21	20:00	Alex Kontorovich	Teaching Real Analysis as a Video Game
Wed	Jan 21	20:30	Chris Henson	Proof Automation and Metaprogramming in CSLib: Locally Nameless Lambda Calculi
Thu	Jan 22	15:00	Wojciech Różowski	Coinductive predicates in Lean
Thu	Jan 22	15:30	Oliver Dressler	lean-lsp-mcp: Tools for agentic interaction with Lean
Thu	Jan 22	16:00	Break	Break
Thu	Jan 22	16:30	Hannah Scholz	Formalisation of CW complexes
Thu	Jan 22	17:00	Salvatore Mercuri	A bottom-up approach to formalisation in the FLT project
Thu	Jan 22	17:30	Etienne Marion	Formalization of the Ionescu-Tulcea theorem in Mathlib
Thu	Jan 22	18:00	Julius Marx	MRiscX: Certified RISC-V interpreter with Hoare logic as a DSL in Lean
Fri	Jan 23	13:00	Kim Morrison	grind
Fri	Jan 23	13:30	Alex Best	Aristotle, an AI theorem prover using Lean
Fri	Jan 23	14:00	Son Ho	Formal Verification of Rust Cryptographic Code in Lean with Aeneas
Fri	Jan 23	14:30	Break	Break
Fri	Jan 23	15:00	Christoph Thiele	TBA
Fri	Jan 23	15:30	Michal Mrugala	Formalizing Class Field Theory
Fri	Jan 23	16:00	Break	Break
Fri	Jan 23	16:30	Joël Riou	Formalization of homotopy theory in Lean
Fri	Jan 23	17:00	Atticus Kuhn	Verification of model-checking techniques in Lean

Embed this schedule

Your time			Speaker	Title
Mon	Jan 19	18:30	Siddharth Bhat	Sound & Complete Tactics for the Linear-Bitwise Fragment of Multi-Width Parametric Bitvector Theory
Mon	Jan 19	17:30	Leo de Moura	The State of Lean
Mon	Jan 19	17:00	Break	Break
Mon	Jan 19	16:30	Yaël Dillies	Hopf algebras, affine group schemes and all of that
Mon	Jan 19	16:00	Leopoldo Sarra	Towards autoformalization for physics and engineering with Lean
Mon	Jan 19	15:45	Break	Break
Mon	Jan 19	15:15	Jonas van der Schaaf	Internal Projectivity of the Sequence Space in Lean
Mon	Jan 19	14:45	Vasilii Nesterov	Verified computation of real asymptotics
Mon	Jan 19	14:15	Johan Commelin	The Mathlib Initiative: Scaling, Infrastructure, and Future Directions
Mon	Jan 19	14:00	Lean Together Organizers	Opening Remarks

Embed this schedule

Export series to