IAP 2026 class about Lean (mirror)
import Cluedump import GenerateSlidesLib #leantex_config latexConfig unsafe def main : IO Unit := do generateSlides latexConfig