人类思维
理解
直觉、例子、图示、猜想，以及由人写出的清晰证明。不只是怎么做——更是为什么成立。
Chloe, 数学家: “为什么这是对的？”
掌握现在。瞥见未来。理解现在，绝不以未来为前提。
三种认知方式，彼此交织
每个概念都通过三种互补的方式来讲授，它们相互加强，而不是分散在各自独立的书里。
形式化
证明
在 Lean 4 中给出精确的定义和经机器检验的证明。所有假设都明确写出；凡是没有通过编译的，一概不作声明。
Gideon, 形式主义者: “我们能精确地证明它吗？”
计算
计算
可以在浏览器中运行的 Python 实验。学会区分证据、近似和证明。
Margaret, 计算家: “如果算一算，会怎么样？”
第一条路径已经开放
五节相互衔接的课，从给一篮水果分类到函数的复合——通往范畴论的大门。
- 1幼儿园至二年级一组对象分类、属于，还有令人惊奇的空盒子——集合最初的想法。5–8 岁
- 2三至五年级SetsMembership, subsets, unions and intersections — the language almost all of mathematics is written in.Ages 8–12
- 3六至八年级IntegersNumbers below zero, the opposites that cancel them, and a proof of why negative times negative is positive.Ages 11–14
- 4六至八年级FunctionsRules that give exactly one output for every input — drawn as arrows, built from ordered pairs, and sorted into injective, surjective and bijective.Ages 12–15
- 5九至十二年级CompositionDoing one function and then another — why order matters, why brackets don't, and how this simple idea opens the door to category theory.Ages 14–18
可选 · 从不评分
探奇小径
为好奇者准备的可选支路。它们从不计入成绩，也总会带你回到原来的位置。
幼儿园至二年级Boxes inside boxesWhat is inside a box that contains only an empty box? Is it empty? And can every description you can think of make a collection?踏上小径 六至八年级How many infinities?There are infinitely many counting numbers and infinitely many infinite 0–1 sequences. Are these two infinities the same size?踏上小径 六至八年级Clock arithmeticIt's 9 o'clock. What time will it be in 5 hours — and in 29 hours? Can a clock teach us a whole new kind of arithmetic?踏上小径 六至八年级Inverses and structureEvery integer can be added to another integer to get . So why can almost no integer be multiplied by another integer to get ?踏上小径 六至八年级Remainder familiesSort every integer — positive, negative and zero — into families by its remainder after dividing by 3. If you add a member of one family to a member of another, does the family of the answer depend on which members you chose?踏上小径 九至十二年级The product, by its mapsCan you describe the set of pairs without ever looking inside it — only by how functions go into it?踏上小径
找到你的起点
每位学习者都从某处起步。选一扇适合你的门——你随时可以四处漫游。
今天已有的内容——如实相告
The Lumenary 才刚刚起步。以下就是到目前为止已经建成并检验过的全部内容。
目前还没有任何内容经过人类数学家或教育工作者的审校。这种审校是下一步必不可少的工作。
查看验证报告- 节课
- 5
- 条探奇小径
- 7
- 个已绘入地图的主题
- 169
- 条已编译的 Lean 声明
- 88
- 个已测试的实验
- 12
- 种演示语言
- 6