London Learning Lean

general mathematics number theory

Imperial College London

Audience: Advanced learners
Seminar series time: Thursday 15:00-16:00 in your time zone, UTC
Organizer: Kevin Buzzard*
*contact for this listing

This is a seminar on formalising research level, MSc, or advanced undergraduate level mathematics in the Lean theorem prover. It is suitable for people who have some mathematical background, e.g. MSc students in a mathematics department. Speakers will assume some familiarity with the Lean but you certainly don't have to be a Lean expert

Speakers are told to spend 50 percent of their time explaining the mathematics, and 50 percent on the Lean implementation.

Past seminars are available on the YouTube playlist here

The seminar series is hybrid/online -- it will meet in person at Imperial College in room Huxley 410, and will also be live streamed on Zoom.

Upcoming talks
Past talks
Your timeSpeakerTitle
ThuMay 0415:00Amelia LivingstonTori
ThuMar 2316:00Matej PenciakImplementing Cryptographic Primitives in Lean 4
ThuMar 1616:00Joy Hu/Runchang LiSome Basics of Gaussian Measure in Lean
ThuMar 0916:00Jujian ZhangFlat modules
ThuMar 0216:00cancelled(speaker illness)
ThuFeb 2316:00Jineon BaekOn the Erdős-Tuza-Valtr Conjecture
ThuFeb 1616:00Ella Yu + Xiang LiEuler's Totient Theorem and the Prime Number Theorem
ThuFeb 0916:00Anand Rao Tadipatri + Siddhartha GadgilFormalising Giles Gardam's disproof of Kaplansky's Unit Conjecture
ThuFeb 0216:00Alex BestSolving Diophantine equations via the class group
ThuJan 2616:00Oliver NashErgodicity and Gallagher's theorem
ThuJan 1916:00Ashvni NarayananTBA
ThuJan 1216:00Billy MiaoOstrowski's theorem
ThuJun 3015:00Wrenna RobsonPost-Quantum Cryptography
ThuJun 2315:00Yael DilliesBehrend's construction and additive combinatorics
ThuJun 1615:00María Inés de Frutos FernándezExtensions of norms and Fontaine’s period rings
ThuJun 0915:00Sebastian MonnetThe Krull Topology
ThuJun 0215:00No seminar (UK holiday)No seminar (UK holiday)
ThuMay 2615:00David AngdinataElliptic curves and the Mordell-Weil theorem
ThuMay 1915:00Pierre-Alexandre BazinClassification of finitely-generated modules over a PID
ThuMay 1215:00Violeta Hernández PalaciosOrdinals
ThuMay 0515:00Jujian ZhangProj
ThuMar 2416:00Heather MacbethFourier series
ThuMar 1716:00Oliver NashEngel's theorem in Mathlib
ThuMar 1016:00Ashvni Narayananp-adic L-functions
ThuMar 0316:00Alena GusakovIntroduction to matroids
ThuFeb 2416:00Bhavik MehtaThe Erdős-Szemerédi conjecture and working with finiteness
ThuFeb 1716:00Kexing YingProbability theory and martingales
ThuFeb 1016:00Nicolò CavalleriTopological vector bundles
ThuFeb 0316:00Kenny LauTilting Perfectoid Fields
ThuJan 2716:00Amelia LivingstonGroup cohomology
ThuJan 2016:00Chris BirkbeckModular forms and Eisenstein series
ThuJan 1316:00María Inés de Frutos-FernándezAdeles and ideles
Embed this schedule
Export series to