请问HN：寻找一个好的课程来学习证明助手 Lean 4。
嗨，HN，
我最近在探索 Lean 4，这是一种定理证明器和编程语言，我对它在形式推理和证明方面所提供的功能印象深刻。然而，找到一个结构化的、由讲师主导的课程或组织的学习小组（而不仅仅是教程或文档）一直很困难。
有没有人知道：
- 教授 Lean 4 的大学或在线课程（开放注册）
- 任何指导性的小组、训练营或社区学习项目。
我的目标是以更系统和互动的方式学习 Lean 4——理想情况下能够获得反馈、参与项目或进行同伴讨论。
如果你参加过这样的课程、组织过这样的课程，或者知道可以去哪里寻找（例如 Discord、Zulip 群组或大学链接），我将非常感激你的指引。
谢谢！
查看原文
Hi HN,
I’ve been exploring Lean 4, the theorem prover and programming language, and I’m impressed by what it offers for formal reasoning and proofs. However, it’s been difficult to find a structured, instructor-led course or organized study group (as opposed to just tutorials or documentation).
Does anyone know of:
University or online courses (open enrollment) teaching Lean 4
Any guided cohorts, bootcamps, or community study programs.
My goal is to learn Lean 4 in a more systematic and interactive way — ideally with feedback, projects, or peer discussion.
If you’ve taken such a course, organized one, or know where to look (e.g. Discords, Zulip groups, or university links), I’d love your pointers.<p>Thanks!