用 Python 模拟 Lean 定理证明
Some content in this article was created with AI assistance. Please verify as needed.Lean 证明中的表达式、命题、证明项和 tactic 属于不同层次。只看执行效果时，ring、positivity、linarith 都像是在“帮我算一下”。实际上，tactic 负责构造证明，证明仍要经过 kernel 检查。 下面用一个单文件 Python demo 拆开这几层。程序处理如下代数问题：设 $0<p,q,r<1$，并且 $$(1-p^2)(1-q^2)(1-r^2)=8p^2q^2r^2, \tag{1}$$ 分别证明 $$1<p+q+r,\qquadp+q+r<2.$$ 程序不给 $p,q,r$ 赋浮点数，也不靠抽样验证结论。表达式、命题和证明都保存为数据，再由一个小型 checker 逐步检查： 1234567数学写法 ↓Expr / Prop 抽象语法树 ↓规则或 tactic 构造 Proof 树 ↓Kernel 递归检查 下文按源码顺序...
牛顿分形：用求根公式划分复平面
牛顿迭代通常用于求解实方程，但公式本身并不要求变量是实数。把复平面上的每个点都作为初值运行一次牛顿迭代，再按照最后收敛到的根着色，就能得到一张牛顿分形（Newton fractal）。 同一个多项式的几个根会像不同国家一样瓜分复平面。吸引域内部相当平静，边界却会不断分叉；在边界附近稍微改变初值，迭代就可能收敛到另一个根。 复平面上的牛顿迭代对于多项式 $p(z)$，牛顿迭代为 $$z_{k+1}=N_p(z_k)=z_k-\frac{p(z_k)}{p’(z_k)}.$$ 多项式的根是牛顿映射的不动点，根附近的初值会快速向它收敛。所有最终收敛到同一个根的初值组成该根的吸引域，不同吸引域的公共边界则是牛顿映射的 Julia 集。 牛顿分形例子最经典的例子是 $p(z)=z^3-1$，它的三个根位于单位圆上。 在绘图中，三个根各自分配一种颜色，颜色亮度表示收敛速度： 远离边界，尤其是在根附近时，通常只需几次迭代，颜色较亮； 越接近边界，迭代路线越曲折，颜色也越暗。 对于 $p(z)=z^n-1$，它的 $n$ 个根均匀分布在单位圆上，根...
Lean 学习笔记——7. 线性代数基础
Some content in this article was created with AI assistance. Please verify as needed.mathlib 区分坐标函数、线性映射和矩阵。三者都能描述线性变换，但保存的数据和可直接使用的定理不同；选定基以后，才谈得上用矩阵表示抽象线性映射。 1234import Mathlibopen Matrixopen scoped BigOperators 本篇只讨论有限维实向量、矩阵、线性映射和子空间，集中说明这些对象的类型、转换方式和常用证明入口。 有限向量向量表示长度为 n、元素类型为 α 的坐标向量可以直接表示成： 1Fin n → α Fin n 是小于 n 的自然数类型。函数的定义域决定向量长度，因此不同长度的向量具有不同类型。 123#check (fun i : Fin 3 => (i : Nat))#check (0 : Fin 3)#check (2 : Fin 3) 这种表示与普通数组不同。Array α 的长度是运行时数据，Fin n → α 的维数则出现在类型中。需要固定维数...
Lean 学习笔记——6. 集合、离散数学与代数自动化
Some content in this article was created with AI assistance. Please verify as needed.mathlib 为数值计算、多项式、线性不等式和离散算术分别提供了专用 tactic。使用前先判断目标属于哪套理论；连续试命令通常只会掩盖缺少的前提或转换步骤。 1import Mathlib 数值类型与代数自动化常见数系 Lean 类型 数学对象 备注 ℕ / Nat 自然数 减法截断到零 ℤ / Int 整数 可使用负数 ℚ / Rat 有理数 精确分数 ℝ / Real 实数 非可计算的数学实数 ℂ / Complex 复数 实部、虚部为实数 同一个字面量会根据上下文解释： 1234#check (2 : ℕ)#check (2 : ℤ)#check (2 : ℚ)#check (2 : ℝ) 自然数减法尤其需要注意： 12#eval (3 - 5 : Nat) -- 0#eval (3 - 5 : Int) -- -2 ...
Lean 学习笔记——5. 命题逻辑、证明项与等式推理
Some content in this article was created with AI assistance. Please verify as needed.本篇参考 Mathematics in Lean，按证明中常见的操作重新组织，不逐章翻译原书。 示例统一放在 mathlib 项目中，并从下面的导入开始： 1import Mathlib 实际项目可以只导入需要的模块，学习阶段直接 import Mathlib 更方便。 证明项与 tactic 基础命题也是类型Lean 使用 Prop 表示命题的类型： 1234#check 2 + 2 = 4 -- Prop#check 3 < 5 -- Prop#check True -- Prop#check False -- Prop 一个命题的值就是该命题的证明。声明定理和声明普通定义的语法非常接近： 12theorem two_add_two : 2 + 2 = 4 := by norm_num theorem 和 lemma 在内...
Lean 学习笔记——4. 模块、类型类、Monad 与 IO
Some content in this article was created with AI assistance. Please verify as needed.Lean 用命名空间管理名称，用结构体保存数据，用类型类描述多个类型共享的接口。mathlib 中许多看似自动的参数补全，实际来自类型类搜索。 模块、命名空间与作用域命名空间命名空间避免全局名称冲突： 1234567891011namespace Textdef surround (left right value : String) : String := left ++ value ++ rightdef quote (value : String) : String := surround "\"" "\"" valueend Text#eval Text.quote "Lean" open Text 会让当前作用域可以省略前缀： 123456sectionopen Text#eval quote "Lean&q...
Lean 学习笔记——3. 代数数据类型、递归与容器
Some content in this article was created with AI assistance. Please verify as needed.Lean 用乘积、和、结构体与归纳类型组织数据。代数数据类型规定一个值携带哪些字段，以及允许用哪些构造器产生值。 组合类型乘积类型α × β 表示同时保存一个 α 和一个 β： 1234def user : String × Nat := ("Ada", 36)#eval user.1 -- "Ada"#eval user.2 -- 36 可以使用模式一次拆开： 123def describeUser (u : String × Nat) : String := let (name, age) := u s!"{name} is {age}" Lean 的三元组实际是嵌套的二元组，α × β × γ 按 α × (β × γ) 解析。 和类型 Sum α β 表示值要么是 α，要么是 β，两个构造器分别为 ...
Lean 学习笔记——2. 语言基础、函数与类型系统
Some content in this article was created with AI assistance. Please verify as needed.本篇只用工具链自带的 Init 和 Std，讨论表达式、函数、类型推断和依赖类型等语言基础，不引入 mathlib。Lean 的整体定位、执行模型和学习路线见第一篇“语言概述与思维转换”。 语言基础表达式和类型Lean 中几乎所有语法结构都是表达式：字面量、函数调用、if 和 match 都会产生值。#check 查看表达式的类型，#eval 对可计算的表达式求值。 1234567#check 42 -- Nat#check true -- Bool#check "Lean" -- String#check (3, "three") -- Nat × String#eval 6 * 7 -- 42#eval String.length "Lean" -- 4 常用的基础类型如下： 类型 含义...
Lean 学习笔记——1. 语言概述与思维转换
Some content in this article was created with AI assistance. Please verify as needed.如果只看 def、函数调用和模式匹配，Lean 很像一门语法稍显特殊的函数式语言。实际写起来，类型检查会计算表达式，递归函数可能要证明终止，tactic 生成的定理还要再交给 kernel 检查。普通语言的编译流程不足以解释这些现象。 Lean 用依赖类型统一描述程序与证明。语法本身不算难记，先要放下“类型只约束运行时数据”这一习惯。本篇整理后续内容所需的语言背景。 语言定位编程语言与定理证明器Lean 是基于依赖类型理论的交互式定理证明器，也是一门严格求值的纯函数式语言。普通函数、数学定义、证明以及编译期扩展都写在 Lean 中，并登记到同一个声明环境。区别在于声明的类型以及代码在哪个阶段执行。 作为编程语言，Lean 有代数数据类型、模式匹配、高阶函数、类型类、Monad、宏和原生代码编译器。它的表面结构与 Haskell、OCaml 有不少相似之处。作为定理证明器，Lean 把命题放在 Prop 中，把证明...
LaTeX 编译引擎跨平台基准测试
这里是一份 LaTeX 引擎跨平台基准测试脚本，用于对比各个编译引擎的编译耗时以及增量编译效率，并生成一份测试报告。 测试报告示例 测试内容 纯英文：比较 pdfLaTeX、XeLaTeX、LuaLaTeX； 中文：比较 XeLaTeX、LuaLaTeX，不测试 pdfLaTeX； 从空辅助目录开始的完整编译； 修改少量源码并保留 .aux、.toc 后的增量编译； 自动输出包含逐轮测量、汇总统计和环境元数据的 JSON，以及编译日志和测试 PDF； 自动生成一页式中文性能简报，重点比较相同工作负载下不同引擎的速度、排名和相对差距； 图表包含 P50、样本区间误差线，并将冷启动到增量构建的加速比作为附带指标； 测试结束后在控制台直接输出各文档、各构建模式下的引擎排名和主要结论。 脚本只使用 Python 标准库。测试机器需要安装 Python 3.8 或更高版本以及 TeX Live，并确保 latexmk、pdflatex、xelatex、lualatex 位于 PATH。TeX Live 还应包含 ctex、Fandol 字体、pgfplots、booktabs、...