验证

The Lumenary 力求比一般的 AI 生成材料更值得信赖。本页如实报告哪些内容经过了检验、用什么检验，以及哪些尚未检验。

形式化证明（Lean）

88 条声明已用 leanprover/lean4:v4.35.0 编译；其中 0 条依赖 sorry。3 条应用了库中的定理，59 条在此证明，26 条是定义。

生成于 2026-10-28 06:13

12 个实验中有 12 个运行并通过了测试。pytest：571 项通过，0 项失败。

Python 3.10.12 · sympy 1.13.3 · mpmath 1.3.0 · numpy 2.2.5 · pytest 8.3.5 · 生成于 2026-10-28 06:13

105 项自动检查通过，0 项失败（模式、前置知识图、登记表、翻译、答案解析）。

浏览器端到端检查（六种语言、练习、知识图、Python 沙盒）：通过 15 项，失败 0 项。

生成于 2026-10-28 06:16

目前还没有任何课程、译文或练习经过合格的人类数学家、教育工作者或译者审校。多个 AI 系统之间的一致并不被视为正确性的证据。

实验	证据	状态
Cantor's diagonal trick on a finite list	精确计算	通过
Clock arithmetic: which residues have inverses?	有限穷举检验, 精确计算	通过
Sorting and counting a market basket	精确计算, 有限穷举检验	通过
Composing functions: associative, but order matters	有限穷举检验, 反例	通过
Counting functions, injections and surjections	有限穷举检验, 精确计算	通过
Forty primes in a row, then a counterexample	实验证据, 反例	通过
Exact versus numerical: 0.1 + 0.2 and the square root of 2	数值近似, 精确计算, 符号计算	通过
Hunting for inverses in the integers and the rationals	实验证据, 精确计算	通过
Does a random walk come home? Statistical evidence	统计证据, 精确计算	通过
Remainder families: residue classes that add up	有限穷举检验, 反例	通过
Checking set identities exhaustively	有限穷举检验, 反例	通过
Negative times negative: grid, symbols and proof	实验证据, 符号计算	通过