Junk Theorems in Lean
2 months ago
- #Lean 4
- #Mathlib
- #Type Theory
- 一组用Lean 4 + Mathlib形式化验证的垃圾定理，这些定理会让不熟悉类型论的数学家感到惊讶。
- 定理1：有理数1/2的第三个坐标是一个双射。
- 定理2：多项式X²(X³ + X + 1)的第一个坐标等于30的质因数分解。
- 定理3：多元多项式在单变量多项式的第一个坐标上的第二个坐标等于6。
- 定理4：集合{z : ℝ | z ≠ 0}是一个连续、非单调的满射。
- 定理5：黎曼猜想位于双重否定集合的拓扑闭包中。
- 定理6：7的二进制展开等价于其自身。
- 定理7：非运算与自身的点积，或运算的矩阵行列式，但不包括与运算的行列式。
- 定理8：群范畴上的存在量词是一个不可测集。
- 定理9：ζ(1) = ½(γ - log 4π)，其中ζ(s)是黎曼ζ函数。
- 定理10：2 - 3（作为ℕ上的部分函数）等于+∞。
- 定理11：二次互反律和贝尔纲定理不假的唯一证明在带点类型中相等。
- 定理12：多项式坐标与有理数坐标之间的复杂关系。
- 定理13：a = b = c，展示了Lean中定义性证明无关性存在的问题。
- 定理14：假设某些公理，0 = 1，突显了Lean编译器设计中的不一致性。