D1 · 7 月 15 日（周三）
从零到逻辑 + AI 工具上手
Course materials for the opening session: slides and a Lean script for getting started.
材料
D2 · 7 月 16 日（周四）
归纳类型与类型类
Inductive types, pattern matching, recursion and induction proofs, structures, the common inductive types (Option / List / Fin / Multiset), and type classes — ending in one integrated expression-tree example.
讲义
Lean 代码 · 点击在 live.lean-lang.org 打开
- D2_Inductive 归纳类型基础：Weekday、MyNat、MyOption、MyList、Tree
- D2_PatternMatching 模式匹配与结构递归
- D2_InductionProofs cases、induction 与归纳证明
- D2_Structure structure：Vector2、带性质的结构
- D2_CommonTypes Option / List / Fin（含 Multiset 注释）
- D2_IntegratedExample 综合示例：表达式树 Expr
- D2_Typeclass type class、instance、HasNorm、Add/Mul
- D2_Typeclass_Mathlib mathlib 中的 Ring / Field 等结构（需 mathlib 工程）
- D2_Exercises 学生练习模板
- D2_inductiveType 早期归纳类型 demo（讲义早期版本）
录像
- 🎥 IASM 视频回放 主讲：颜富彬
D3 · 7 月 17 日（周五）
代数结构 + 组合/图
Algebraic structures, instances, subobjects, modules, vector spaces, and graph examples in Lean.
Lean 代码
- D3_Demo.lean 课堂综合演示
- D3_isomorphism.lean 同构、商集与第一同构定理
- D3_01_Inspect.lean 结构与实例检查
- D3_02_AddGroup_Group.lean AddGroup 与 Group
- D3_03_Subtype.lean Subtype 与带条件对象
- D3_04_Group_Instance.lean 群实例构造
- D3_05_GroupHom.lean 群同态、核与像
- D3_05_Subgroup.lean 子群
- D3_06_Ring_Instance.lean 环实例构造
- D3_07_Subring.lean 子环
- D3_08_Field_Instance.lean 域实例构造
- D3_09_Module_Submodule.lean Module 与 Submodule
- D3_10_VectorSpace_Choose.lean 向量空间与选择
- D3_11_Category_Homological.lean 范畴与同调示例
- D3_12_Prop_Instance.lean Prop 实例
- D3_13_Deeper_Instance_Search.lean 更深入的实例搜索
- D3_14_Finset_SimpleGraph.lean Finset 与 SimpleGraph
- D3_15_AI_Examples.lean AI 相关示例
录像
- 🎥 IASM 视频回放 主讲：李哲
D4 · 7 月 18 日（周六）
分析结构与拓扑
A map of Mathlib's analysis library — algebraic / order / topological / metric structures, filters as a unified language for limits, continuity, differentiation, interval integration and the fundamental theorem of calculus, ending in a proof workflow that combines API search, AI drafts, and Lean verification.
讲义
Lean 代码 · 点击在 live.lean-lang.org 打开
- D4_AnalyticStructures Real 与代数/序/拓扑/度量结构、filter 作为统一极限语言
- D4_LimitsContinuity 序列与函数极限、ε-δ vs filter、Continuous
- D4_Differentiation deriv、HasDerivAt、求导规则
- D4_Integration 区间积分与微积分基本定理
- D4_ProofWorkflow Mathlib API 搜索与证明修复工作流
- D4_Exercises 学生练习模板
- D4_All 整节课的整合脚本（讲义内引用顺序的拼装版）
录像
- 🎥 IASM 视频回放 主讲：颜富彬
D5 · 7 月 19 日（周日）
函数式编程
Functional programming in Lean through inductive data structures, monads, and the design and evaluation of expression systems.
讲义
Lean 代码 · 点击在 live.lean-lang.org 打开
- D5_01_ListFunctions 自然数与列表上的递归、高阶函数和归并排序
- D5_01_ListFunctions_Exercises 自然数与列表函数练习
- D5_02_Structures 树、图及其递归操作
- D5_02_Structures_Exercises 树与图结构练习
- D5_03_Monad Option、Except、ReaderM、StateM 与 monad transformer
- D5_03_Monad_Exercises Monad 编程练习
- D5_04_Expr 表达式语法树与求值器
- D5_04_Expr_Exercises 表达式树函数练习
- D5_05_ProjectStarter 小型语言项目起始代码
- D5_06_Meta 宏、命令与 tactic elaborator
录像
- 🎥 IASM 视频回放 主讲：王铎磊
D6 · 7 月 20 日（周一）
算法的形式化与验证
A three-hour workshop on monad programs, S-expression verification, the sin x / x limit, verified merge sort in CSLib, and a small language for automatic complexity analysis.
讲义
Lean 代码 · 点击在 live.lean-lang.org 打开
- D6_01_MonadSupplement Reader、Writer、State 与 ExceptT 的顺序式用法
- D6_01_MonadSupplement_Exercises 第一小时的 Monad 练习
- D6_02_FormalizationVerification S-expression 求值器、Mini-C 编译器与正确性定理
- D6_02_FormalizationVerification_Exercises S-expression 分支与编译器验证练习
- D6_03_LHopital_Exercises 显式参数、@ 调用与 sin x / x 极限练习
- D6_04_ComplexityProof TimeM、merge sort 正确性与复杂度证明
- D6_04_ComplexityProof_Exercises 归并结果与计时计算练习
- D6_05_AutomaticComplexity 复杂度表达式、求值器与上界检查器
- D6_05_AutomaticComplexity_Exercises 自动复杂度项目练习
- D6_Termination 递归函数与终止性证明示例
- D6_TimeM 最小 TimeM 模型与 tick 计时方法
录像
- 🎥 IASM 视频回放 主讲：王铎磊
汇报 · 7 月 21 日（周一）
小组项目展示
现场展示，无单独课件。