Event URL : SMS Spring Meeting on Formalization and Proof Assistants Polynomial functors are one of the most useful tools in category theory. They have wide-ranging applications across functional programming, the semantics of dependent type…
Upper level undergraduate course, Johns Hopkins University 🇺🇸, 2025 The emphasis is on fundamental mathematical ideas (basic functional analysis, reproducing kernel Hilbert spaces, concentration inequalities, uniform central limit theorem…
At the most basic level, a category is a collection of objects and morphisms (arrows) between them, satisfying certain axioms. Categories may appear as categories of mathematical structures and the transformations between instances of certa…
A reading group run by Yaël Dillies and me, where we discuss different aspects of interactive theorem proving, programming, and metaprogramming in Lean. Everyone is welcome to join! More experienced users are welcome to propose projects in
Masters level course, Stockholm University 🇸🇪, 2025 Logic II is a second level logic course, giving an introduction to major topics of modern mathematical logic. It consists of three main parts: The course textbook is the following book:
Synthetic theories such as homotopy type theory axiomatize classical mathematical objects such as spaces up to homotopy. Although theorems in synthetic theories translate to theorems about the axiomatized structures on paper, this fact has
Stockholm University, Sweden 🇸🇪, 2025 I gave two guest lectures on metaprogramming and tactic writing in Lean 4. This github repository hosts the lecture notes and code. This course will give an introduction to computer formalisation of m…
Introduction: While elegant synthetic proofs such as those in Homotopy Type Theory (HoTT) are expected to “compile” to proofs of classical theorems when interpreted in suitable models, this idea has not yet been exploited in proof assistant…
You might have come the words “extensionality” and “intensionality” in logic, type theory, interactive theorem proving, etc. Sometimes you hear people say Martin-Löf Type Theory (MLTT) is an intensional type theory, first order logic is an
Mathematicians have used machines and datasets to aid their research for millennia. In our time, computational tools such as computer algebra systems, SAT/SMT solvers, Reinforcement Learning, and LLMs play an increasingly central role in ma…
die Walküre, conducted by Jaap van Zwede For one human being to love another; that is perhaps the most difficult of all our tasks, the ultimate, the last test and proof, the work for which all other work is but preparation. I hold this to b…
Towards the end of Götterdämmerung, the last opera of Wagner’s Ring cycle, Brünnhilde, standing on a rock and surrounded by the flames of the funeral pyre of Siegfried, is holding the cursed ring. She apostrophizes, murmuring to Wotan that