用 Coq 语言形式化 100 个定理

最编程 2024-04-30 16:36:57

...

由 Chesium 翻译、增补

Coq 是一个交互式证明助手
官网：The Coq Proof Assistant

原文链接：Formalizing 100 theorems in Coq

原文为《形式化 100 个定理》（Formalizing 100 Theorems）的一部分

上述文章中的 100 个定理来自《最伟大的 100 个定理》（The Hundred Greatest Theorems）

这些文章只是仅仅列出了定理的名字，绝大部分人是不认识这些定理的，因此我花了数天整理了这些定理的描述，如果描述涉及到一些较深的概念，我就一并把这些概念的定理列在定理描述之前，争取做到有高中数学基础的读者均能看懂定理的描述。

当然，其中一些定理（如勒贝格积分和格林公式）涉及的前置知识较多，尚未完全补全，一些定理（如公平博弈定理）在互联网上找不到相关的资料。

文中列出了定理的中文翻译、《最伟大的 100 个定理》中的英文定理名称（一部分为概述）、该定理所属的数学领域（为我的个人整理，标有问号的是我不确定的）、定理描述、其 Coq 形式化实现（一部分没有）和对应的 Wikipedia 链接（可作为拓展阅读）。

Coq 作为现代人类数理逻辑学的精华，在中文互联网上却十分冷门，作者希望通过本文来宣传一下 Coq神奇的定理检验功能。

1. \(\sqrt{2}\) 的无理性

The Irrationality of the Square Root of \(2\)

数学分析 > 实变函数论？

\(\sqrt{2}\) 无法被表示成 \(\displaystyle{\frac{p}{q}}\ (p,q\in N)\) 的形式。

存在多种版本（如：qarith-stern-brocot/theories/sqrt2）

Theorem sqrt2_not_rational : forall p q : nat, q <> 0 -> p * p = 2 * (q * q) -> False.

参考

Square root of \(2\) \(\S\)Proofs of irrationality - Wikipedia

2. 代数基本定理

Fundamental Theorem of Algebra

代数

\(n\) 次复系数多项式方程在复数域内有且只有 \(n\) 个根。

赫尔曼·格弗斯（Herman Geuvers）等人（corn/fta/FTA）

Lemma FTA : forall f : CCX, nonConst _ f -> {z : CC | f ! z [=] [0]}.

参考

Fundamental theorem of algebra - Wikipedia

3. 有理数集是可数集

The Denumerability of the Rational Numbers

数学基础 > 集合论

有理数集 \(\mathbb{Q}\) 中每个元素都能与自然数集 \(\mathbb{N}\) 的每个元素之间能建立一一对应的关系。

米拉德·尼基（Milad Niqui）（qarith-stern-brocot/theories/Q_denumerable）

Definition same_cardinality (A:Type) (B:Type) :=
  { f : A -> B & { g : B -> A |
    forall b,(compose _ _ _ f g) b = (identity B) b /\
    forall a,(compose _ _ _ g f) a = (identity A) a } }.

Definition is_denumerable A := same_cardinality A nat.

Theorem Q_is_denumerable: is_denumerable Q.

丹尼尔·施普勒（Daniel Schepler）（topology/theories/ZornsLemma/CountableTypes）

Inductive CountableT (X:Type) : Prop :=
  | intro_nat_injection: forall f:X->nat, injective f -> CountableT X.

Lemma Q_countable: CountableT Q.

参考

Rational number \(\S\)Properties - Wikipedia

4. 毕达哥拉斯定理（勾股定理）

Pythagorean Theorem

几何 > 欧几里得平面几何

直角三角形的两条直角边的平方和等于斜边的平方。

弗雷德里克·吉尔霍特（Frédérique Guilhot）（HighSchoolGeometry/theories/euclidien_classiques）

Theorem Pythagore :
 forall A B C : PO,
 orthogonal (vec A B) (vec A C) <->
 Rsqr (distance B C) = Rsqr (distance A B) + Rsqr (distance A C) :>R.

加布里埃尔·布朗（Gabriel Braun）（GeoCoq Chapter 15）

Lemma pythagoras :
 forall O E E' A B C AC BC AB AC2 BC2 AB2,
  O<>E ->
  Per A C B ->
  length O E E' A B AB ->
  length O E E' A C AC ->
  length O E E' B C BC ->
  prod O E E' AC AC AC2 ->
  prod O E E' BC BC BC2 ->
  prod O E E' AB AB AB2 ->
  sum  O E E' AC2 BC2 AB2.

参考

Pythagorean theorem - Wikipedia

5. 质数定理

Prime Number Theorem

数论 > 解析数论

定义 \(\pi(x)\) 为小于等于 \(x\) 的质数个数（例：\(\pi(10)=4\)）
则当 \(x\) 趋近于无限时，\(\pi(x)\) 与 \(\displaystyle{\frac{x}{\ln x}}\) 的比值趋近于 \(1\) 。
极限式：

\[\lim_{x\to\infty}\pi(x)/\frac{x}{\ln x}=1 \]

渐进式：

\[\pi(x)\sim\frac{x}{\ln x} \]

无已知 Coq 形式化实现。

参考

Prime number theorem - Wikipedia

6. 哥德尔不完备定理

Gödel's Incompleteness Theorem

数学基础 > 数理逻辑

任何自洽的形式系统，只要蕴涵皮亚诺算术公理，就可以在其中构造在体系中不能被证明的真命题，因此通过推理演绎不能得到所有真命题（即体系是不完备的）。

任何逻辑自洽的形式系统，只要蕴涵皮亚诺算术公理，它就不能用于证明其本身的自洽性。

（待补）

拉塞尔·奥康纳（Russell O'Connor）（goedel/theories/goedel1）

Theorem Goedel'sIncompleteness1st :
 wConsistent T ->
 exists f : Formula,
   ~ SysPrf T f /\
   ~ SysPrf T (notH f) /\ (forall v : nat, ~ In v (freeVarFormula LNN f)).

拉塞尔·奥康纳（Russell O'Connor）（goedel/theories/goedel2）
这个证明假定了后两条希尔伯特-贝尔奈斯可证性条件（Hilbert-Bernays provability conditions）的成立

Hypothesis HBL2 : forall f, SysPrf T (impH (box f) (box (box f))).
Hypothesis HBL3 : forall f g, SysPrf T (impH (box (impH f g)) (impH (box f) (box g))).

Theorem SecondIncompletness :
SysPrf T Con -> Inconsistent LNT T.

参考

Gödel's incompleteness theorems - Wikipedia

7. 二次互反律

Law of Quadratic Reciprocity

数论 > 代数数论

定义勒让德符号 \(\displaystyle{\left(\frac{a}{b}\right)}\ (a,b,x\in\mathbb{N},b\) 为质数 \()\)：若二次同余方程 \(x^2\equiv a\ (\mathrm{mod}\ b)\) 有解则为 \(1\) ，否则为 \(-1\)。
二次互反律：设 \(p\) 和 \(q\) 为不相等的两奇质数，则有：

\[\left(\frac{q}{p}\right)\cdot\left(\frac{p}{q}\right) =(-1)^{(p-1)/2\cdot(q-1)/2} \]

纳撒尼尔·库朗（Nathanaël Courant）（Github）

Theorem Quadratic_reciprocity :
  (legendre p q) * (legendre q p) = (-1) ^ (((p - 1) / 2) * ((q - 1) / 2)).

参考

Quadratic reciprocity - Wikipedia

8. 尺规三等分角、倍立方的不可能性

The Impossibility of Trisecting the Angle and Doubling the Cube

几何；代数 > 抽象代数 > 群论域论

无法用无刻度的直尺和圆规按照以下要求作图：

将一个角三等分。

作一个立方体使其体积为已知立方体的 \(2\) 倍。

无已知 Coq 形式化实现。

参考

Angle trisection \(\S\)Proof of impossibility - Wikipedia

Doubling the cube \(\S\)Proof of impossibility - Wikipedia

9. 圆的面积公式

The Area of a Circle

几何 > 解析几何学；数学分析 > 微积分学

圆的面积为其半径长度的平方乘以 \(\pi\)，即：

\[S_{\odot}=\pi r^2 \]

无已知 Coq 形式化实现。

参考

Area of a circle \(\S\)Modern proofs - Wikipedia

10. 费马-欧拉定理

Euler's Generalization of Fermat's Little Theorem

数论 > 同余

设 \(a,m\in\mathbb{N^+}\) ，且 \(\gcd(a,m)=1\) ，则有：

\[a^{\varphi(m)}\equiv 1\ (\mathrm{mod}\ m) \]

其中 \(\varphi(x)\ (x\in\mathbb{N^+})\) 为欧拉函数，表示小于等于 \(x\) 的正整数中与 \(x\) 互质的数的个数。

洛朗·泰瑞（Laurent Théry）（mathcomp/solvable/cyclic.v）

Theorem Euler_exp_totient a n : coprime a n -> a ^ totient n  = 1 %[mod n].

参考

Euler's theorem - Wikipedia

11. 有无限个质数

The Infinitude of Primes

数论 > ？

如题，或者说，对于每一个质数 \(m\)，都能找到一个质数 \(p\) 使得 \(m<p\)。

JsCoq 开发组（A First Example: The Infinitude of Primes）

Lemma prime_above m : {p | m < p & prime p}.

参考

Euclid's theorem - Wikipedia

12. 平行公理的独立性

The Independence of the Parallel Postulate

几何 > 欧几里得几何

欧式几何的五条公理：

任意两个点可以通过一条直线连接。

任意线段能无限延长成一条直线。

给定任意线段，可以以其一个端点作为圆心，该线段作为半径作一个圆。

所有直角都相等。

若两条直线都与第三条直线相交，并且在同一边的内角之和小于两个直角和，则这两条直线在这一边必定相交。

其中第五条公理被称为平行公理，它无法由前四条公理推出。

无已知 Coq 形式化实现。

参考

Parallel postulate - Wikipedia

13. 多面体的欧拉公式

Polyhedron Formula

几何 > 离散几何学；拓扑学 > 代数拓扑拓扑图论

对于所有和一个球面同胚的多面体，有：

\[V-E+F=2 \]

其中 \(V\) 为顶点数，\(E\) 为边数，\(F\) 为面数

（待补）

让-弗朗索瓦·杜福尔（Jean-François Dufourd）（euler-formula/Euler3）

Theorem Euler_Poincare_criterion: forall m:fmap,
  inv_qhmap m -> (plf m <-> (nv m + ne m + nf m - nd m) / 2 = nc m).

参考

Euler characteristic \(\S\)Polyhedra - Wikipedia

14. 巴塞尔问题

Euler's Summation of 1 + (1/2)^2 + (1/3)^2 + …

数论 > 解析数论

所有自然数平方的倒数之和为圆周率平方的六分之一，即：
\(\zeta(2)=\displaystyle{\sum^\infty_{n=1}\frac{1}{n^2}=\frac{\pi^2}{6}}\)

让·玛丽·马迪奥（Jean-Marie Madiot）（coqtail-math/Reals/Rzeta2）

Theorem zeta2_pi_2_6 : Rser_cv (fun n => 1 / (n + 1) ^ 2) (PI ^ 2 / 6).

参考

Basel problem - Wikipedia

15. 微积分基本定理

Fundamental Theorem of Integral Calculus

数学分析 > 微积分学

定义区间的分割：一个闭区间 \([a,b]\) 的一个分割 \(\mathrm{P}\) 是指在此区间中取一个有限的序列 \(x_i\ (i=1,2,\dots,n)\) 使得 \(a=x_0<x_1<\dots<x_n=b\)。
其中每个闭区间 \([x_i,x_{i+1}]\) 叫做一个子区间。定义 \(\lambda\) 为这些子区间长度的最大值，即：

\[\lambda=\max\{x_{i+1}-x_i|i\in[0,n-1]\} \]

定义取样分割：一个闭区间 \([a,b]\) 的一个取样分割是指在进行分割 \(a=x_0<x_1<\dots<x_n=b\) 后，在每一个子区间 \([x_i,x_{i+1}]\) 中取出一点 \(t_i\in[x_i,x_{i+1}]\) ，其中 \(\lambda\) 定义同上。
定义黎曼积分：\(S\) 是函数 \(f\) 在闭区间 \([a,b]\) 上的黎曼积分，记为 \(\displaystyle{\int_a^bf(x)dx}\)
当且仅当：

\[\begin{aligned} \forall\epsilon>0,&\\ &\exists\delta>0,&\\ &&\forall\text{取样分割}x_0,\dots,x_n、t_0,\dots,x_{n-1}&\\ &&& \!\!\!\!\!\!\!\!\!\!\!\!\!\! \!\!\!\!\!\!\!\!\!\!\!\!\!\! \underset{\underset{ \displaystyle{ \left|\sum^{n-1}_{i=0}f(t_i)(x_{i+1}-x_i)-S\right|<\epsilon }}{\displaystyle{ \Downarrow }}}{ \lambda\le\delta }\\ \end{aligned} \]

此时称 \(f\) 在闭区间 \([a,b]\) 上是黎曼可积的。

微积分基本定理第一部分：
设 \(a,b\in\mathbb{R}\)，\(f:[a,b]\mapsto\mathbb{R}\) 为黎曼可积函数，定义函数 \(F:[a,b]\mapsto\mathbb{R}\):

\[F(x)=\int_a^xf(t)dt \]

则 \(F\) 在闭区间 \([a,b]\) 连续。若 \(f\) 在 \(x\) 连续则 \(F\) 在 \(x\) 处可微，且有 \(F'(x)=f(x)\)。

微积分基本定理第二部分：
设两函数 \(f,F:[a,b]\mapsto\mathbb{R}\)，且满足以下条件：

\(f\) 是黎曼可积函数

\(\forall x\in(a,b),\ F'(x)=f(x)\)

则有：

\[\int_a^bf(t)dt=F(b)-F(a) \]

路易斯·克鲁兹-菲利普（Luís Cruz-Filipe）（corn/ftc/FTC）

Theorem FTC1 : Derivative J pJ G F.
Theorem FTC2 : {c : IR | Feq J (G{-}G0) [-C-]c}.

Coq 开发组（standard library, Reals/RiemannInt）

Lemma FTC_Riemann :
  forall (f:C1_fun) (a b:R) (pr:Riemann_integrable (derive f (diff0 f)) a b),
    RiemannInt pr = f b - f a.

参考

Fundamental theorem of calculus - Wikipedia

16. 阿贝尔-鲁菲尼定理

Insolvability of General Higher Degree Equations

代数 > 抽象代数 > 域论群论

五次及以上一元多项式方程的根无法通过其系数的代数式（即仅包含有限个加、减、乘、开方五种代数运算的表达式）来表示。

苏菲·伯纳德、西里尔·科恩、亚西亚·马布比、皮埃尔-伊夫·斯特鲁布（Sophie Bernard, Cyril Cohen, Assia Mahboubi, Pierre-Yves Strub）（Abel/theories/abel）

Lemma example_not_solvable_by_radicals :
  ~ solvable_by_radical_poly ('X^5 - 4 *: 'X + 2 : {poly rat}).

参考

Abel-Ruffini theorem - Wikipedia

17. 棣莫弗公式

De Moivre's Theorem

数学分析 > 复变函数论

设两个复数 \(z_1,z_2\)，其三角形式分别为 \(z_1=r_1(\cos\theta_1+i\sin\theta_1),z_2=r_2(\cos\theta_2+i\sin\theta_2)\)，则有：

\[z_1z_2=r_1r_2[\cos(\theta_1+\theta_2)+i\sin(\theta_1+\theta_2)] \]

Coqtail 库开发组（coqtail-math/Complex/Cexp）

Lemma Cexp_trigo_compat : forall a, Cexp (0 +i a) = cos a +i sin a.
Lemma Cexp_mult : forall a n, Cexp (INC n * a) = (Cexp a) ^ n.

参考

De Moivre's formula - Wikipedia

18. 刘维尔定理

Liouville's Theorem

数学分析 > 复变函数论

定义全纯：若 \(U\) 为 \(\mathbb{C}\) 的开子集，且 \(f:U\mapsto\mathbb{C}\) 是一个函数。我们称 \(f\) 在 \(U\) 中一点 \(z_0\) 是复可微或全纯的，当且仅当以下极限存在：

\[f'(z_0)=\lim_{z\to z_0}\frac{f(z)-f(z_0)}{z-z_0} \]

若 \(f\) 在 \(U\) 中任意点均为全纯的，则称 \(f\) 在 \(U\) 上全纯。

定义整函数：若函数在 \(\mathbb{C}\) 上全纯，则称该函数为整函数。

刘维尔定理：
对任意一个整函数 \(f:\mathbb{C}\mapsto\mathbb{C}\)，若存在一个正实数 \(M\) 使得对于所有的 \(z\in\mathbb{C}\) 都有 \(|f(z)\le M|\)，则该函数必为常数函数。

瓦伦丁·博洛特（Valentin Blot）（corn/liouville/Liouville）

Theorem Liouville_theorem2 :
    {n : nat | {C : IR | Zero [<] C | forall (x : Q),
         (C[*]inj_Q IR (1#Qden x)%Q[^]n) [<=] AbsIR (inj_Q _ x [-] a)}}.

参考

Liouville's theorem (complex analysis) - Wikipedia

19. 四平方和定理

Four Squares Theorem

数论 > 堆垒数论

每个正整数均可表示为 \(4\) 个整数的平方和。

纪尧姆·阿莱，让·玛丽·马迪奥（Guillaume Allais, Jean-Marie Madiot）（coqtail-math/Arith/Lagrange_four_square）

Theorem lagrange_4_square_theorem : forall n, 0 <= n ->
  { a : _ & { b: _ & { c : _ & { d |
    n = a * a + b * b + c * c + d * d } } } }.

参考

Lagrange's four-square theorem - Wikipedia

20. 费马平方和定理

All Primes Equal the Sum of Two Squares

数论 > 代数数论

奇质数能表示为两个平方数之和当且仅当该质数被 \(4\) 除的余数为 \(1\)。

洛朗·泰瑞（Laurent Théry）（sum-of-two-square/TwoSquares）

Definition sum_of_two_squares :=
  fun p => exists a , exists b , p = a * a + b * b.

Theorem two_squares_exists:
  forall p, prime p -> p = 2 \/ Zis_mod p 1 4 -> sum_of_two_squares p.

Lemma sum2sprime p :
  odd p -> prime p -> p \is a sum_of_two_square = (p %% 4 == 1).

参考

Fermat's theorem on sums of two squares - Wikipedia

21. 格林公式

Green's Theorem

数学分析 > 微积分学 > 向量分析

设闭区域 \(D\) 由分段光滑的曲线 \(L\) 围成，二元函数 \(P(x,y)\) 和 \(Q(x,y)\) 在 \(D\) 上具有一阶连续偏导数，则有：

\[\underset{D}{\iint}\left( \frac{\partial Q}{\partial x} -\frac{\partial P}{\partial y} \right)dxdy =\underset{D}{\oint}Pdx+Qdy \]

其中 \(L\) 是 \(D\) 取正向的边界曲线。

（待补）

无已知 Coq 形式化实现

参考

Green's theorem - Wikipedia

22. 实数集是不可数集

The Non-Denumerability of the Continuum

数学分析 > 实分析；数学基础 > 集合论

不存在有理数集 \(\mathbb{R}\) 中每个元素和自然数集 \(\mathbb{N}\) 的每个元素之间的一一对应关系。

皮埃尔-玛丽·佩德罗（Pierre-Marie Pédrot）（coqtail-math/Reals/Logic/Runcountable）

Theorem R_uncountable : forall (f : nat -> R),
  {l : R | forall n, l <> f n}.

Theorem R_uncountable_strong : forall (f : nat -> R) (x y : R),
  x < y -> {l : R | forall n, l <> f n & x <= l <= y}.

C-CoRN 开发组（corn/reals/RealCount）

Theorem reals_not_countable :
  forall (f : nat -> IR), {x :IR | forall n : nat, x [#] (f n)}.

参考

Cardinality of the continuum \(\S\)Uncountability - Wikipedia

23. 勾股数定理

Formula for Pythagorean Triples

数论 > ？

勾股数的生成公式：

\[a=m^2+n^2,\ b=2mn,\ c=m^2+n^2 \]

其中 \(m\) 和 \(n\) 互质且不都为奇数。

大卫·德拉哈耶（David Delahaye）（fermat4/Pythagorean）

Lemma pytha_thm3 : forall a b c : Z,
  is_pytha a b c -> Zodd a ->
  exists p : Z, exists q : Z, exists m : Z,
    a = m * (q * q - p * p) /\ b = 2 * m * (p * q) /\
    c = m * (p * p + q * q) /\ m >= 0 /\
    p >= 0 /\ q > 0 /\ p <= q /\ (rel_prime p q) /\
    (distinct_parity p q).

参考

Pythagorean triple - Wikipedia

24. 连续统假设的不确定性

The Undecidability of the Continuum Hypothesis

数学基础 > 集合论

连续统假设：不存在一个基数绝对大于可数集而绝对小于实数集的集合。
连续统假设和 ZFC 公理系统是彼此独立的。

（待补）

无已知 Coq 形式化实现。

参考

Continuum hypothesis \(\S\)Independence from ZFC - Wikipedia

25. 康托尔-伯恩斯坦-施罗德定理

Schröder-Bernstein theorem

数学基础 > 集合论

对于两个集合 \(A\) 和 \(B\)，若存在单射 \(f:A\mapsto B\) 和 \(g:B\mapsto A\) 则必存在双射 \(h:A\mapsto B\)。
另一种表述：对于两个集合 \(A\) 和 \(B\)，若 \(|A|\le|B|\) 且 \(|B|\le|A|\) 则 \(|A|=|B|\)。

（待补）

雨果·赫贝林（Hugo Herbelin）（schroeder/Schroeder）

Theorem Schroeder : A <=_card B -> B <=_card A -> A =_card B.

丹尼尔·施普勒（Daniel Schepler）（topology/theories/ZornsLemma/CSB）

Section CSB.
Variable X Y:Type.
Variable f:X->Y.
Variable g:Y->X.
Hypothesis f_inj: injective f.
Hypothesis g_inj: injective g.

Theorem CSB: exists h:X->Y, bijective h.

End CSB.

参考

Schröder-Bernstein theorem - Wikipedia

26. \(\pi\) 的莱布尼茨级数

Leibnitz's Series for Pi

数学分析 > 微积分学

\[\frac{\pi}{4} =1-\frac{1}{3}+\frac{1}{5}-\frac{1}{7}+\frac{1}{9}-\dots =\sum^\infty_{n=0}\frac{(-1)^n}{2n+1}\]

纪尧姆·阿莱（Guillaume Allais）（standard library, Reals/Ratan）

Lemma PI_2_aux : {z : R | 7 / 8 <= z <= 7 / 4 /\ - cos z = 0}.
Definition PI := 2 * proj1_sig PI_2_aux.

Definition PI_tg n := / INR (2 * n + 1).
Lemma exists_PI : {l:R | Un_cv (fun N => sum_f_R0 (tg_alt PI_tg) N) l}.
Definition Alt_PI : R := 4 * (let (a,_) := exist_PI in a).

Theorem Alt_PI_eq : Alt_PI = PI.

路易斯·克鲁兹-菲利普（Luís Cruz-Filipe）（corn/transc/MoreArcTan）

Lemma ArcTan_one : ArcTan One[=]Pi[/]FourNZ.

Lemma arctan_series : forall c : IR,
  forall (Hs :
    fun_series_convergent_IR
      (olor ([--]One) One)
      (fun i =>
        (([--]One)[^]i[/]nring (S (2*i))
        [//] nringS_ap_zero _ (2*i)){**}Fid IR{^}(2*i+1)))
    Hc,
       FSeries_Sum Hs c Hc[=]ArcTan c.

参考

Leibniz formula for \(\pi\) - Wikipedia

26. 三角形内角和为 \(180^\circ\)

Sum of the Angles of a Triangle

几何 > 欧几里得平面几何

在欧几里得空间中，任意三角形的三个内角之和等于平角（或 \(180^\circ\)、\(\displaystyle{\frac{\pi}{2}}\)、两个直角）。

弗雷德里克·吉尔霍特（Frédérique Guilhot）（HighSchoolGeometry/theories/angles_vecteurs）

Theorem somme_triangle :
 forall A B C : PO,
 A <> B :>PO ->
 A <> C :>PO ->
 B <> C :>PO ->
 plus (cons_AV (vec A B) (vec A C))
   (plus (cons_AV (vec B C) (vec B A)) (cons_AV (vec C A) (vec C B))) =
 image_angle pi :>AV.

布特里、格里斯、纳尔布（Boutry, Gries, Narboux）（GeoCoq/Meta_theory/Parallel_postulates/Euclid）

Theorem equivalent_postulates_assuming_greenberg_s_axiom :
  greenberg_s_axiom ->
  all_equiv
    (alternate_interior_angles_postulate::
     alternative_playfair_s_postulate::
     alternative_proclus_postulate::
     alternative_strong_parallel_postulate::
     consecutive_interior_angles_postulate::
     euclid_5::
     euclid_s_parallel_postulate::
     existential_playfair_s_postulate::
     existential_thales_postulate::
     inverse_projection_postulate::
     midpoint_converse_postulate::
     perpendicular_transversal_postulate::
     postulate_of_transitivity_of_parallelism::
     playfair_s_postulate::
     posidonius_postulate::
     universal_posidonius_postulate::
     postulate_of_existence_of_a_right_lambert_quadrilateral::
     postulate_of_existence_of_a_right_saccheri_quadrilateral::
     postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights::
     postulate_of_existence_of_similar_triangles::
     postulate_of_parallelism_of_perpendicular_transversals::
     postulate_of_right_lambert_quadrilaterals::
     postulate_of_right_saccheri_quadrilaterals::
     postulate_of_transitivity_of_parallelism::
     proclus_postulate::
     strong_parallel_postulate::
     tarski_s_parallel_postulate::
     thales_postulate::
     thales_converse_postulate::
     triangle_circumscription_principle::
     triangle_postulate::
     nil).

参考

Sum of angles of a triangle - Wikipedia

28. 帕斯卡定理

Pascal's Hexagon Theorem

欧几里得几何；射影几何（推广版本）

若一个六边形内接于一圆，那么它的三对对边的交点在同一条直线上。

马戈、纳尔布（Magaud and Narboux）（projective-geometry/Plane/hexamys）

Definition is_hexamy A B C D E F :=
  (A<>B / A<>C / A<>D / A<>E / A<>F /
  B<>C / B<>D / B<>E / B<>F /
  C<>D / C<>E / C<>F /
  D<>E / D<>F /
  E<>F) /
  let a:= inter (line B C) (line E F) in
  let b:= inter (line C D) (line F A) in
  let c:= inter (line A B) (line D E) in
Col a b c.

Lemma hexamy_prop: pappus_strong -> forall A B C D E F,
 (line C D) <> (line A F) ->
 (line B C) <> (line E F) ->
 (line A B) <> (line D E) ->

 (line A C) <> (line E F) ->
 (line B F) <> (line C D) ->
 is_hexamy A B C D E F -> is_hexamy B A C D E F.

参考

Pascal's theorem - Wikipedia

29. 费尔巴哈定理

Feuerbach's Theorem

欧几里得几何

三角形的九点圆与其内切圆以及三个旁切圆相切。

（待补）

本杰明·格雷瓜尔、洛伊克·波蒂尔、洛朗·泰瑞（Benjamin Grégoire, Loïc Pottier, and Laurent Théry）（Coq test suite for Nsatz tactic）

Lemma Feuerbach:  forall A B C A1 B1 C1 O A2 B2 C2 O2:point,
  forall r r2:R,
  X A = 0 -> Y A =  0 -> X B = 1 -> Y B =  0->
  middle A B C1 -> middle B C A1 -> middle C A B1 ->
  distance2 O A1 = distance2 O B1 ->
  distance2 O A1 = distance2 O C1 ->
  collinear A B C2 -> orthogonal A B O2 C2 ->
  collinear B C A2 -> orthogonal B C O2 A2 ->
  collinear A C B2 -> orthogonal A C O2 B2 ->
  distance2 O2 A2 = distance2 O2 B2 ->
  distance2 O2 A2 = distance2 O2 C2 ->
  r^2%Z = distance2 O A1 ->
  r2^2%Z = distance2 O2 A2 ->
  distance2 O O2 = (r + r2)^2%Z
  \/ distance2 O O2 = (r - r2)^2%Z
  \/ collinear A B C.

参考

Feuerbach point - Wikipedia

30. 伯特兰投票问题

The Ballot Problem

离散数学 > 组合数学

一场选举中候选人 \(A\) 得到了 \(p\) 张选票，而候选人得到了 \(q\) 张选票（\(p>q\)），那么在整个点票过程中 \(A\) 的票数都严格大于 \(B\) 的概率为 \(\displaystyle{\frac{p-q}{p+q}}\)。

让·玛丽·马迪奥（Jean-Marie Madiot）（coq-100-theorems/ballot）

Theorem bertrand_ballot p q :
  let l := filter (fun votes => count_votes votes "A" =? p) (picks (p + q) ["A"; "B"]) in
  p >= q ->
  (p + q) * List.length (filter (throughout (wins "A" "B")) l) =
  (p - q) * List.length (filter (wins "A" "B") l).

参考

Bertrand's ballot theorem - Wikipedia

31. 拉姆齐定理

Ramsey's Theorem

离散数学 > 图论

对任意正整数 \(c\) 和 \(n_1,n_2,\dots,n_c\)，必然存在某正整数 \(R\) 、\(i\ (1\le i\le c)\)，使得 \(R\) 阶的完全图无论如何将其边染成 \(c\) 种颜色，必能找到其的一个 \(n_i\) 阶的完全子图，其各边均被染为了第 \(i\) 种颜色。

（待补）

弗雷德里克·布朗基（Frédéric Blanqui）（color/Util/Set/Ramsey）

Theorem ramsey A (W : set A) n (P : Pinf W) B : forall (C : Pf B)
  (f : Pcard P (S n) -> elts C), Proper (Pcard_equiv ==> elts_eq) f ->
  exists c (Q : Pinf P), forall X : Pcard Q (S n), f (Pcard_subset Q X) = c.

参考

Ramsey's theorem - Wikipedia

32. 四色定理

The Four Color Problem

离散数学 > 组合数学图论

任何一张地图只用四种颜色就能使具有共同边界的国家着上不同的颜色。

乔治·冈蒂尔、本杰明·沃纳（Georges Gonthier, Benjamin Werner）（fourcolor/theories/fourcolor）

Theorem four_color m : simple_map m -> colorable_with 4 m.

参考

Four color theorem - Wikipedia

33. 费马大定理

Fermat's Last Theorem

数论
几何 > 代数几何；代数 > 抽象代数（用于证明）

当整数 \(n>2\) 时，关于 \(x,y,z\) 的方程 \(x^n+y^n=z^n\) 无整数解。

无已知 Coq 形式化实现

参考

Fermat's Last Theorem - Wikipedia

34. 调和级数发散

Divergence of the Harmonic Series

数学分析？

\[\sum^\infty_{k=1}\frac{1}{k}=\infty \]

Coqtail 开发组（coqtail-math/Reals/Rseries/Rseries_RiemannInt）

Lemma harmonic_series_equiv : (sum_f_R0 (fun n ⇒ / (S n))) ~ (fun n ⇒ ln (S (S n))).

参考

Harmonic series (mathematics) \(\S\)Divergence - Wikipedia

35. 泰勒定理

Taylor's Theorem

数学分析 > 微积分学

设 \(n\) 是一个正整数。如果定义在一个包含 \(a\) 的区间上的函数 \(f\) 在 \(a\) 点处 \(n+1\) 次可导，那么对于这个区间上的任意 \(x\) 均有：

\[f(x)=f(a)+\frac{f'(a)}{1!}(x-a)+\frac{f^{(2)}(a)}{2!}(x-a)^2+\dots+\frac{f^{(n)}(a)}{n!}(x-a)^n+R_n(x) \]

其中的多项式称为函数在 \(a\) 处的泰勒展开式，剩余的 \(R_n(x)\) 是泰勒公式的余项，是 \((x-a)^n\) 的高阶无穷小。

（待补）

路易斯·克鲁兹-菲利普（Luís Cruz-Filipe）（corn/ftc/Taylor）

Theorem Taylor : forall e, Zero [<] e -> forall Hb',
  {c : IR | Compact (Min_leEq_Max a b) c |
    forall Hc, AbsIR (F b Hb'[-]Part _ _ Taylor_aux[-]deriv_Sn c Hc[*] (b[-]a)) [<=] e}.

参考

Taylor's theorem - Wikipedia

36. 布劳威尔不动点定理

Brouwer Fixed Point Theorem

拓扑学

每一个从一个欧几里得空间的某个给定的凸紧子集映射到它自身的连续函数都至少有一个不动点。

（待补）

无已知 Coq 实现。

参考

Brouwer fixed-point theorem - Wikipedia

37. 三次方程的求解公式

The Solution of a Cubic

初等代数

卡尔达诺公式：
对任意给定的三次方程 \(at^3+bt^2+ct+d=0\)，可以令 \(t=x-\displaystyle{\frac{b}{3a}}\) 将方程化为形如 \(x^3+px+q=0\) 的三次方程，此时若 \(4p^3+27q^2>0\) 则方程有一实根：

\[x_0=\sqrt[\overset{\displaystyle{3}}{}]{-\frac{q}{2}+\sqrt{\frac{q^2}{4}+\frac{p^3}{27}}}+\sqrt[\overset{\displaystyle{3}}{}]{-\frac{q}{2}-\sqrt{\frac{q^2}{4}+\frac{p^3}{27}}} \]

另外两个根可以通过将上式两个根式中的其中一个乘以 \(\displaystyle{\frac{-1+i\sqrt{3}}{2}}\)，另一个乘以 \(\displaystyle{\frac{-1-i\sqrt{3}}{2}}\) 来得到。

弗雷德里克·查达德（Frédéric Chardard）（coq-100-theorems/cardan_ferrari）

Definition Cardan_Tartaglia_formula:=fun (a1:C) (a2:C) (a3:C) (n:nat) =>
let s:=-a1/3 in 
let p:=a2+2*s*a1+3*Cpow s 2 in
let q:=a3+a2*s+a1*Cpow s 2+Cpow s 3 in
let Delta:=(Cpow (q/2) 2)+(Cpow (p/3) 3) in
let alpha : C :=if(Ceq_dec p 0) then (RtoC 0) else (cubicroot (-(q/2)+Csqrt Delta)) in
let beta:=if(Ceq_dec p 0) then -cubicroot q else -(p/3)/alpha in
s+(alpha*Cpow CJ n+beta*Cpow CJ (n+n)).


Theorem Cardan_Tartaglia : forall a1 a2 a3 :C,
let u1:=(Cardan_Tartaglia_formula a1 a2 a3 0) in
let u2:=(Cardan_Tartaglia_formula a1 a2 a3 1) in
let u3:=(Cardan_Tartaglia_formula a1 a2 a3 2) in
forall u:C, (u-u1)*(u-u2)*(u-u3)=Cpow u 3+a1*Cpow u 2+a2*u+a3.

参考

Cubic equation \(\S\)Cardano's formula - Wikipedia

38. 几何平均数不大于算数平均数

Arithmetic Mean/Geometric Mean

初等代数？

对于任意数列 \(a_1,a_2,\dots,a_n\) 其几何平均数小于等于其算数平均数，即：

\[\sqrt[\overset{\displaystyle{n}}{}]{\prod^n_{i=1}x_i}\le\sum^n_{i=1}x_i \]

当且仅当 \(a_1=a_2=\dots=a_n\) 时取等号。

让·玛丽·马迪奥（Jean-Marie Madiot）（coq-100-theorems/mean）

Theorem geometric_arithmetic_mean (a : nat -> R) (n : nat) :
  n <> O ->
  (forall i, (i < n)%nat -> 0 <= a i) ->
  prod n a <= (sum n a / INR n) ^ n
  /\
  (prod n a = (sum n a / INR n) ^ n -> forall i, (i < n)%nat -> a i = a O).

参考

Inequality of arithmetic and geometric means - Wikipedia

39. 佩尔方程的解

Solutions to Pell's Equation

数论

佩尔方程是形如 \(x^2-ny^2=1\quad(n\in\mathbb{N}^+)\) 的二元二次不定方程
设 \(\displaystyle{\frac{p_i}{q_i}}\) 是 \(\sqrt{n}\) 连分数表示 \([a_0;a_1,a_2,a_3,\dots]\) 的渐进分数列，其中最小的 \(i\) 对应的 \(p\) 和 \(q\) 即为佩尔方程的基本解，记作 \((x_1,y_1)\)，则该方程的所有解 \((x_k,y_k)\) 可以表示为如下形式：

\[x_k+y_k\sqrt{n}=(x_1+y_1\sqrt{n})^k \]

且有以下递推式：

\[\begin{aligned} x_{k+1}&=x_1x_k+ny_1y_k\\ y_{k+1}&=x_1y_k+y_1x_k\\ \end{aligned} \]

无已知 Coq 形式化实现。

参考

Pell's equation \(\S\)Fundamental solution via continued fractions - Wikipedia

40. 闵可夫斯基定理

Minkowski's Fundamental Theorem

应用数学 > 最优化 > 凸分析；数论 > 几何数论

假设 \(L\) 是 \(n\) 维向量空间 \(\mathbb{R}^n\) 中的一片格点，其行列式值为 \(\det(L)\)，\(S\) 是 \(\mathbb{R}^n\) 的一个中心对称凸子集，若 \(\mathrm{vol}(S)>2^n\det(L)\)，则 \(S\) 必会包含至少一个除原点以外的格点。

（待补）

无已知 Coq 形式化实现。

参考

Minkowski's theorem - Wikipedia

41. 皮瑟定理

Puiseux's Theorem

代数 > 抽象代数 > 交换代数；数学分析 > 实分析复分析

（待补）

丹尼尔·德·劳格劳德（Daniel de Rauglaudre）（puiseuxth/coq/Puiseux）

Theorem puiseux_series_algeb_closed : ∀ (α : Type) (R : ring α) (K : field R),
  algeb_closed_field K
  → ∀ pol : polynomial (puiseux_series α),
    degree (ps_zerop K) pol ≥ 1
    → ∃ s : puiseux_series α, (ps_pol_apply pol s = 0)%ps.

参考

Puiseux series \(\S\)Newton-Puiseux theorem - Wikipedia

42. 所有三角形数的倒数和为 \(2\)

Sum of the Reciprocals of the Triangular Numbers

初等代数

裂项求和

一定数目的点在等距离的排列下可以形成一个等边三角形，这样的数被称为三角形数。
通项公式：\(T_n=\displaystyle{\frac{n(n+1)}{2}}\)。
所有三角形数的倒数和为 \(2\)，即：

\[\sum^\infty_{n=1}\frac{1}{T_n}=\sum^\infty_{n=1}\frac{2}{n(n+1)}=2 \]

Coqtail 开发组（coqtail-math/Reals/Triangular）

Lemma sum_reciprocal_triangular : Rser_cv (fun n => / triangle (S n)) 2.

参考

Triangular number \(\S\)Other properties - Wikipedia

43. 等周定理

The Isoperimetric Theorem

几何 > 解析几何；数学分析 > 微积分学

对于任意欧几里得平面上的封闭图形，设其周界长为 \(L\)，包围区域的面积为 \(S\)，则有以下不等式：

\[4\pi L\le S^2 \]

当且仅当该封闭图形为圆时等号成立。

无已知 Coq 形式化实现。

参考

Isoperimetric inequality - Wikipedia

44. 二项式定理

The Binomial Theorem

离散数学 > 组合数学

\[\begin{aligned} (x+y)^n&=\binom{n}{0}x^ny^0+\binom{n}{1}x^{n-1}y^1+\dots+\binom{n}{n-1}x^1y^{n-1}+\binom{n}{n}x^0y^n \\&=\sum^n_{k=0}\binom{n}{k}x^{n-k}y^k =\sum^n_{k=0}\binom{n}{k}x^ky^{n-k} \end{aligned} \]

Coq 开发组（standard library, Reals/Binomial）

Lemma binomial :
  forall (x y:R) (n:nat),
    (x + y) ^ n = sum_f_R0 (fun i:nat => C n i * x ^ i * y ^ (n - i)) n.

洛朗·泰瑞、何塞·C·阿尔梅达（Laurent Thery & Jose C. Almeida）（RSA/Binomials）

Theorem exp_Pascal :
 forall a b n : nat,
 power (a + b) n =
 sum_nm n 0 (fun k : nat => binomial n k * (power a (n - k) * power b k)).

让·玛丽·马迪奥（Jean-Marie Madiot）（coqtail-math/Hierarchy/Commutative_ring_binomial）

Definition newton_sum n a b : X :=
  CRsum (fun k => (Nbinomial n k) ** (a ^ k) * (b ^ (n - k))) n.

Theorem Newton : forall n a b, (a + b) ^ n == newton_sum n a b.

参考

Binomial theorem - Wikipedia

45. 欧拉整数分拆定理

The Partition Theorem

离散数学 > 组合数学

将整数 \(N\) 分拆为多个不等整数的方案数等于将 \(N\) 分拆为多个奇数的方案数。这是格莱舍定理的特殊情况。

无已知 Coq 形式化实现。

参考

Partition (number theory) \(\S\)Odd parts and distinct parts - Wikipedia

46. 四次方程的求解公式

The Solution of the General Quartic Equation

初等代数

法拉利公式：
对任意给定的四次方程 \(Ax^4+Bx^3+Cx^2+Dx+E=0\)
令 \(\alpha\)、\(\beta\)、\(\gamma\) 分别为：

\[\begin{aligned} \alpha&=-\frac{3B^2}{8A^2}+\frac{C}{A}\\ \beta&=\frac{B^3}{8A^3}-\frac{BC}{2A^2}+\frac{D}{A}\\ \gamma&=-\frac{3B^4}{256A^4}+\frac{B^2C}{16A^3}-\frac{BD}{4A^2}+\frac{E}{A} \end{aligned}\]

若 \(\beta=0\) 则

\[x_{1,2,3,4}=-\frac{B}{4A}\pm_1\sqrt{\frac{-\alpha\pm_2\sqrt{\alpha^2-4\gamma}}{2}}\qquad(\beta=0) \]

（上面所有公式中具有相同下标的正负号需相同，否则互相独立）
否则继续令 \(P\)、\(Q\)、\(R\)、\(S\)、\(T\)、\(U\) 依次为

\[\begin{aligned} P&=-\frac{\alpha^2}{12}-\gamma\\ Q&=-\frac{\alpha^3}{108}+\frac{\alpha\gamma}{3}-\frac{\beta}{8}\\ R&=-\frac{Q}{2}\pm\sqrt{\frac{Q^2}{4}+\frac{P^3}{27}}\\ S&=\sqrt[3]{R}\\ T&=-\frac{5}{6}\alpha+\begin{cases} -\sqrt[3]{Q}&\quad(S=0)\\ S-\displaystyle{\frac{P}{3S}}&\quad(S\neq0) \end{cases}\\ U&=\sqrt{\alpha+2T} \end{aligned}\]

（\(R\) 式中取正负号均可，\(S\) 式会得到三个复根，任取其一均可）
最后，我们有原方程的四个根为：

\[x_{1,2,3,4}=-\frac{B}{4A}+\frac{\pm_1U\pm_2\sqrt{-\left(3\alpha+2T\pm_1\displaystyle{\frac{2\beta}{U}}\right)}}{2} \]

（上面所有公式中具有相同下标的正负号需相同，否则互相独立）

弗雷德里克·查达德（Frédéric Chardard）（coq-100-theorems/cardan_ferrari）

Theorem Ferrari_formula: forall (a:C) (b:C) (c:C) (d:C), 
let s:=-a/4 in 
let p:= b+3*s*a+6*Cpow s 2 in
let q:= c+2*b*s+3*a*Cpow s 2+4*Cpow s 3 in
let r:= d+c*s+b*Cpow s 2+a*Cpow s 3+Cpow s 4 in
let lambda:=Cardan_Tartaglia_formula (-p/2) (-r) (r*p/2-/8*Cpow q 2) 0 in
let A:=Csqrt(2*lambda-p) in
let cond:=(Ceq_dec (2*lambda) p) in
let B:=if cond then (RtoC 0) else (-q/(2*A)) in
let z1:=if cond then Csqrt (binom_solution p r 0) 
                else binom_solution A (B+lambda) 0 in
let z2:=if cond then -Csqrt (binom_solution p r 0) 
                else binom_solution A (B+lambda) 1 in
let z3:=if cond then Csqrt (binom_solution p r 1) 
                else binom_solution (-A) (-B+lambda) 0 in
let z4:=if cond then -Csqrt (binom_solution p r 1) 
                else binom_solution (-A) (-B+lambda) 1 in
let u1:=z1+s in
let u2:=z2+s in
let u3:=z3+s in
let u4:=z4+s in
forall u:C, (u-u1)*(u-u2)*(u-u3)*(u-u4)=Cpow u 4+a*Cpow u 3+b*Cpow u 2+c*u+d.

参考

Quartic equation \(\S\)Ferrari's solution - Wikipedia

47. 中心极限定理

The Central Limit Theorem

概率论

设随机变量 \(x_1,x_2,\dots,x_n\) 独立同分布，并且具有有限的数学期望 \(E(x_i)=\mu\) 和方差 \(D(x_i)=\sigma^2\)（其中 \(i=1,2,\dots\)）则对任意 \(x\)，分布函数

\[F_n(x)=P\left\{\frac{\displaystyle{\sum^n_{i=1}}X_i-n\mu}{\sigma\sqrt{n}}\le x\right\} \]

满足：

\[\lim_{n\to\infty}F_n(x)=\frac{1}{\sqrt{2\pi}}\int_{-\infty}^xe^{-\frac{t^2}{2}}dt \]

即，满足正态分布。

（待补）

无已知 Coq 形式化实现。

参考

Central limit theorem - Wikipedia

48. 狄利克雷定理

Dirichlet's Theorem

数论 > 解析数论

若 \(r\) 和 \(N\) 互质，则有：

\[\lim_{x\to\infty}\frac{\pi(x;N,r)}{\pi(x)}=\frac{1}{\varphi(N)} \]

其中 \(\varphi(x)\) 为欧拉函数，表示小于等于 \(x\) 的正整数中与 \(x\) 互质的数的个数，\(\pi(x)\) 为质数计数函数，表示小于等于 \(x\) 的质数个数，\(\pi(x;N,r)\) 为模 \(N\) 与 \(r\) 集合中小于 \(x\) 的质数个数。

无已知 Coq 形式化实现。

参考

Dirichlet's theorem on arithmetic progressions - Wikipedia

49. 哈密尔顿-凯莱定理

The Cayley-Hamilton Thoerem

代数 > 线性代数

对任意 \(n\times n\) 矩阵 \(A\)，定义 \(A\) 的特征多项式为：

\[p(\lambda)=\det(\lambda I_n-A) \]

其中 \(I_n\) 为 \(n\times n\) 的单位矩阵，则有：

\[p(A)=O_n \]

其中 \(O_n\) 为 \(n\times n\) 的零矩阵。

西迪·乌尔德·比哈（Sidi Ould Biha）（mathcomp/algebra/mxpoly）

Theorem Cayley_Hamilton (R : comRingType) n' (A : 'M[R]_n'.+1) :
  horner_mx A (char_poly A) = 0.

参考

Cayley-Hamilton theorem - Wikipedia

50. 只有 \(5\) 种凸正多面体

The Number of Platonic Solids

几何

凸正多面体，又称为柏拉图立体，是指各面都是全等的正多边形且每一个顶点所接的面数都是一样的凸多面体。
符合这种特性的立体总共只有5种：正四面体、正六面体、正八面体、正十二面体和正二十面体。

无已知 Coq 形式化实现。

参考

Platonic solid \(\S\)Classification - Wikipedia

51. 威尔逊定理

Wilson's Theorem

数论 > 初等数论

\((n-1)!\equiv-1\quad(\mathrm{mod}\ n)\)

微软，INRIA（mathcomp/ssreflect/binomial）

Theorem Wilson : forall p, p > 1 -> prime p = (p %| ((p.-1)`!).+1).

洛朗·泰瑞（Laurent Théry）（sum-of-two-square/Wilson）

Theorem wilson: forall p, prime p ->  Zis_mod (Zfact (p - 1)) (- 1) p.

参考

Wilson's theorem - Wikipedia

52. 子集的个数

The Number of Subsets of a Set

数学基础 > 集合论；离散数学 > 组合数学

元质数量为 \(n\) 的集合的子集个数为 \(2^n\)。

微软，INRIA（mathcomp/ssreflect/finset）

Lemma card_powerset (T : finType) (A : {set T}) : #|powerset A| = 2 ^ #|A|.

皮埃尔·莱图泽（Pierre Letouzey）（fsets/PowerSet）

Lemma powerset_cardinal:
  forall s, MM.cardinal (powerset s) = two_power (M.cardinal s).

参考

Power set \(\S\)Properties - Wikipedia

53. \(\pi\) 是超越数

\(\pi\) is Trancendental

数论 > 解析数论 > 超越数论

定义一个复数是代数数，当且仅当其是某一整系数多项式的复根。
不是代数数的复数称为超越数。

苏菲·伯纳德、劳伦斯·里多（Sophie Bernard、Laurence Rideau）（Lindemann/LindemannTheorem）

Notation "x 'is_algebraic'" := (algebraicOver QtoC x) (at level 55).

Theorem Pi_trans_by_LB : ~ (RtoC Rtrigo1.PI is_algebraic).

参考

Transcendental number \(\S\)The transcendence of \(\pi\) - Wikipedia

Lindemann-Weierstrass theorem \(\S\)Transcendence of \(e\) and \(\pi\) - Wikipedia

54. 柯尼斯堡七桥问题

Königsberg Bridges Problem

离散数学 > 图论

让·玛丽·马迪奥（Jean-Marie Madiot）（coq-100-theorems/konigsberg_bridges）

Theorem konigsberg_bridges :
  let E := [(0, 1); (0, 2); (0, 3); (1, 2); (1, 2); (2, 3); (2, 3)] in
  forall p, path p -> eulerian E p -> False.

参考

Seven Bridges of Königsberg - Wikipedia

55. 切割线定理

Product of Segments of Chords

几何 > 欧几里得平面几何

从圆外一点引圆的切线和割线，切线长是这点到割线与圆交点的两条线段长的比例中项。

本杰明·格雷瓜尔、洛伊克·波蒂尔、洛朗·泰瑞（Benjamin Grégoire, Loïc Pottier, and Laurent Théry）（Coq test suite for Nsatz tactic）

Lemma chords: forall O A B C D M:point,
  equaldistance O A O B ->
  equaldistance O A O C ->
  equaldistance O A O D ->
  collinear A B M -> collinear C D M ->
  scalarproduct A M B = scalarproduct C M D
  \/ parallel A B C D.

参考

Tangent-secant theorem - Wikipedia

56. 林德曼定理

The Hermite-Lindemann Transcendence Theorem

数论 > 解析数论 > 超越数论

定义一个复数是代数数，当且仅当其是某一整系数多项式的复根。
不是代数数的复数称为超越数。
当 \(z\) 为非零代数数时，\(e^z\) 为超越数。

苏菲·伯纳德（Sophie Bernard）（Lindemann/LindemannTheorem）

Notation "x 'is_algebraic'" := (algebraicOver QtoC x) (at level 55).

Theorem HermiteLindemann (x : complexR) :
  x != 0 -> x is_algebraic -> ~ ((Cexp x) is_algebr


																				
						
							上一篇：							
								特别有趣和困难的镜像问题" Re.							
						
						
							下一篇：							
								当铺密码							
						
					
															
						
							推荐阅读						
						
														
								
									
										用 Coq 语言形式化 100 个定理