Lecture Notes for the 2026 Zhejiang University Lean Summer School [qrcode]

Dong Anjie

The Chinese University of Hong Kong, Shenzhen

anjiedong at link dot cuhk dot edu dot cn

Finally, a note about ‘we’ in this book: ‘we’ will almost always mean the reader and the authors together, not the authors alone.

systemallowed (s1,s2)λ→(∗,∗)λ2(∗,∗)(□,∗)λω‾(∗,∗)(□,□)λP(∗,∗)(∗,□)λω(∗,∗)(□,∗)(□,□)λP2(∗,∗)(□,∗)(∗,□)λPω‾(∗,∗)(□,□)(∗,□)λPω=λC(∗,∗)(□,∗)(□,□)(∗,□)\begin{array}{|l|llll|} \hline \text{system} & \mathrlap{\text{allowed } (s_1, s_2)} & & & \\ \hline \lambda{\to} & (\ast,\ast) & & & \\ \lambda 2 & (\ast,\ast) & (\square,\ast) & & \\ \lambda\underline{\omega} & (\ast,\ast) & & (\square,\square) & \\ \lambda P & (\ast,\ast) & & & (\ast,\square) \\ \lambda\omega & (\ast,\ast) & (\square,\ast) & (\square,\square) & \\ \lambda P 2 & (\ast,\ast) & (\square,\ast) & & (\ast,\square) \\ \lambda P\underline{\omega} & (\ast,\ast) & & (\square,\square) & (\ast,\square) \\ \lambda P\omega = \lambda C & (\ast,\ast) & (\square,\ast) & (\square,\square) & (\ast,\square) \\ \hline \end{array}
λ→λPλ2λP2λωλCλωλPω
The λ\lambda-cube, modified from Nederpelt and Geuvers' Type Theory and Formal Proof.
TermElabM.run PrettyPrinter.delab TermElabM.toIO EIO.toBaseIO IO.toEIO EIO.toIO CoreM.toIO MetaM.toIO CoreM.run StateRefT'.run Tactic.run MetaM.run RequestM.runCommandElabM RequestM.runTermElabM runTermElabM, liftTermElabM Frontend.runCommandElabM RequestM.runCoreM liftCoreM liftCommandElabM TacticM TermElabM MetaM CoreM EIO IO RequestM DelabM BaseIO CommandElabM SimpM FrontendM
The map of Lean 4's metaprogramming monads, modified from the Mathlib 4 wiki's Monad map.