Floris van Doorn

carleson. A formalized proof of Carleson's theorem in Lean

LeanCourse24. Bonn Lean course for winter 24/25

LeanCourse23. Lean

LeanCourse25. Lean

lean-links. Links to recourses for the Lean Theorem Prover

BonnAnalysis. repository for the collaborative formalization seminar in Analysis in Bonn

HausdorffSchoolLean. Repository for the September 2023 Hausdorff School on Lean

Dagstuhl-tables. Dagstuhl's Happy Diner Problem

LeanInRome. Repository for the workshop Computer-verified proofs: 48 hours in Rome

BonnLeanSeminar. Past contents of Lean Seminars in Bonn

LogicColloquiumTutorial. The Lean tutorial for Logic Colloquium 2023

Spectral. Lean

mathlib. Lean mathematical components library

leansnippets. Miscellaneous Lean code which doesn't belong in the standard library

sard. Work towards a general version of Sard's theorem in Lean 4

hanabi. Computer players for a collaborative card game

flt3. Proof in Lean of Fermat Last Theorem for exponent 3

Harvard-tutoring. Lean

fast_marching. TeX

group-representations. The definition and basic properties of representations of groups in the Lean theorem prover