Zulip Chat Archive
Stream: Lean Together 2026
Topics:
- Links to slides from schedule (7 messages, latest: Feb 12 2026 at 16:21)
- Alex Kontorovich - Teaching Real Analysis as a Video Game (13 messages, latest: Feb 01 2026 at 14:11)
- Julius Marx - MRiscX (5 messages, latest: Feb 01 2026 at 07:31)
- Videos (2 messages, latest: Jan 28 2026 at 13:33)
- Leopoldo Sarra - autoformalization in physics / engineering (11 messages, latest: Jan 27 2026 at 18:47)
- Feedback (14 messages, latest: Jan 27 2026 at 00:56)
- Sophie Morel - Nori's construction in Lean (12 messages, latest: Jan 26 2026 at 12:23)
- Floris van Doorn - Lessons from the Carleson project (17 messages, latest: Jan 25 2026 at 17:32)
- Thanks to the organisers! (1 message, latest: Jan 24 2026 at 12:48)
- Alex Best - Aristotle, an AI theorem prover using Lean (3 messages, latest: Jan 24 2026 at 00:09)
- Atticus Kuhn - Verification of model-checking techniques (2 messages, latest: Jan 23 2026 at 22:40)
- Kim Morrison -
grind(12 messages, latest: Jan 23 2026 at 20:17) - Joël Riou - Formalization of homotopy theory in Lean (3 messages, latest: Jan 23 2026 at 17:02)
- Son Ho - Formal Verification of Rust Cryptographic Code (1 message, latest: Jan 23 2026 at 15:32)
- Michal Mrugala - Formalizing Class Field Theory (2 messages, latest: Jan 23 2026 at 14:37)
- Markus Himmel & Sofia Rodrigues - What's New In Lean (7 messages, latest: Jan 23 2026 at 12:55)
- Key information (6 messages, latest: Jan 23 2026 at 12:49)
- Stefan Kebekus - Project VD (27 messages, latest: Jan 23 2026 at 11:45)
- Etienne Marion - Ionescu-Tulcea theorem in Mathlib (2 messages, latest: Jan 23 2026 at 08:04)
- Hannah Scholz - Formalisation of CW complexes (1 message, latest: Jan 22 2026 at 18:43)
- Salvatore Mercuri - A bottom-up approach to FLT (1 message, latest: Jan 22 2026 at 18:42)
- Wojciech Różowski - Coinductive predicates in Lean (2 messages, latest: Jan 22 2026 at 18:38)
- Oliver Dressler - lean-lsp-mcp (4 messages, latest: Jan 22 2026 at 16:40)
- Chris Henson - Proof Automation and Metaprogramming in CSLib (2 messages, latest: Jan 21 2026 at 22:54)
- Jovan Gerbscheid - Writing proofs by clicking (10 messages, latest: Jan 21 2026 at 22:21)
- Jonas van de Schaaf - Projectivity of the sequence space (3 messages, latest: Jan 21 2026 at 22:00)
- Break discussions on Gather (3 messages, latest: Jan 21 2026 at 16:33)
- Schedule change (1 message, latest: Jan 21 2026 at 15:19)
- Sebastian Ullrich - The Lean module system (16 messages, latest: Jan 21 2026 at 13:26)
- Fabrizio Montesi - CSLib: The Lean Computer Science Library (17 messages, latest: Jan 21 2026 at 00:05)
- Leo de Moura - The State of Lean (5 messages, latest: Jan 20 2026 at 22:00)
- Following asynchronously (via youtube?) (5 messages, latest: Jan 20 2026 at 20:56)
- Sebastian Graf - Simpler do proofs with mvcgen (3 messages, latest: Jan 20 2026 at 19:51)
- Harry Goldstein - Metaprogramming the Next Gen of Testing (3 messages, latest: Jan 20 2026 at 19:19)
- David Ledvinka - Formalization of Brownian Motion in Lean (2 messages, latest: Jan 20 2026 at 17:24)
- María Inés de Frutos Fernández - Universal DP algebra (3 messages, latest: Jan 20 2026 at 14:07)
- Moritz Doll - Schwartz functions and tempered distributions (1 message, latest: Jan 20 2026 at 12:34)
- Vasilii Nesterov - Verified computation of real asymptotics (7 messages, latest: Jan 20 2026 at 07:30)
- Yaël Dillies - Hopf algebras, affine group schemes and co (2 messages, latest: Jan 19 2026 at 16:39)
- Johan Commelin - The Mathlib Initiative (4 messages, latest: Jan 19 2026 at 14:51)
- Community news and workshop introduction (1 message, latest: Jan 19 2026 at 13:58)
- channel events (1 message, latest: Jan 12 2026 at 19:32)
Last updated: Feb 28 2026 at 14:05 UTC