leanprover community
Videos hosted by the Lean theorem prover user community.
lean-auto (Yicheng Qian at Computer Aided Verification 2025)
Lean Together 2025: Jason Rute, The last mile
Lean Together 2025: Jack McKoen, Toward functor quasi-categories in Lean
Lean Together 2025: David Kurniadi Angdinata, Division polynomials of elliptic curves
Lean Together 2025: Yuma Mizuno, Metaprogramming on monoidal categories
Lean Together 2025: Joseph Tooby-Smith, Physics and Lean
Lean Together 2025: Hannah Fechtner, Braid Groups in Lean
Lean Together 2025: Christian Merten, Formalizing the Bruhat-Tits tree
Lean Together 2025: Alex Kontorovich, Complex Analysis and PrimeNumberTheorem+ in Lean
Lean Together 2025: Abdalrhman Mohamed, lean-SMT
Lean Together 2025: Jean-Baptiste Tristan, Verified Foundations for Differential Privacy
Lean Together 2025: Marcus Rossel, Egg: An Equality Saturation Tactic in Lean
Lean Together 2025: Floris van Doorn, Progress report on the Carleson Project
Lean Together 2025: Michael Rothgang, Scaling Mathlib.
Lean Together 2025: Joseph Rotella, Programming with Dependently Typed Tables in Lean
Lean Together 2025: Henrik Böving, Automated Bit-Level Reasoning in Lean 4
Lean Together 2025: Violeta Hernández Palacios, A Nimble Introduction to Nimbers
Lean Together 2025: Lorenzo Luccioli, Information theory in Lean: the DPI
Lean Together 2025: Siddhartha Gadgil, Real world Autoformalization
Lean Together 2025: Jakob von Raumer, Building a Formal Verification Framework for Smart Contracts
Lean Together 2025: Scott Carnahan, Vertex algebras in Mathlib: coming soon?
Lean Together 2025: The Lean FRO, The Lean FRO Year 2 Roadmap and Vision
Lean Together 2025: David Renshaw, Searching for Proof Improvements with tryAtEachStep
Lean Together 2025: Vlad Tsyrklevich and Daniel Weber, The Equational Theories Project
Lean Together 2025: Emily Riehl, The ∞-cosmos project: formalizing 1-, 2-, V-, and ∞-category theory
Lean Together 2025: Xavier Généreux and Jannis Limperg, Efficient Forward Reasoning for Aesop
Lean Together 2025: Damiano Testa, An introduction to linters
Lean Together 2025: Oliver Nash, Root systems and root data in Mathlib
Splitting files to reduce imports in Mathlib
Lean Together 2024: David Thrane Christiansen, Verso: Documentation as a DSL