Coq 中的几何形式化 翻译自 GeoCoq
翻译完成度用这四个图标表示：
Wikiboook 相同
标星号的为尚未获得良好翻译的词条
-
Michael Beeson的公理系统/Axioms/beeson_s_axioms.v -
连续性公理
/Axioms/continuity_axioms.v -
欧几里得公理
/Axioms/euclidean_axioms.v -
塔斯基公理系统
Gupta变种/Axioms/gupta_inspired_variant_axioms.v -
希尔伯特公理系统
/Axioms/hilbert_axioms.v -
塔斯基公理系统
Makarios变种/Axioms/makarios_variant_axioms.v -
平行公设
/Axioms/parallel_postulates.v -
塔斯基公理系统
/Axioms/tarski_axioms.v
暂时不翻译
-
角平分线
/Highschool/bisector.v引理数：7
-
三角形外心
/Highschool/circumcenter.v引理数：16
-
共圆
/Highschool/concyclic.v引理数：26
-
欧拉线（三角形重心垂心外心三点共线）
/Highschool/Euler_line.v引理数：5
-
一些练习
/Highschool/exercises.v引理数：2
-
三角形重心
/Highschool/gravityCenter.v引理数：18
-
三角形内心
/Highschool/incenter.v引理数：7
-
泰勒斯定理（直径所对圆周角为直角）
/Highschool/midpoint_thales.v引理数：2
-
Orientation*/Highschool/orientation.v引理数：61
-
三角形垂心
/Highschool/orthocenter.v引理数：16
-
Sesamath中学几何练习示例/Highschool/sesamath_exercises.v引理数：12
-
三角形
/Highschool/triangles.v引理数：25
-
瓦里尼翁平行四边形
/Highschool/varignon.v引理数：4
暂时不翻译
暂时不翻译
-
定义
/Tarski_dev/Definitions.v引理数：
-
第二章：等长
/Tarski_dev/Ch02_cong.v引理数：34
-
第三章：中间线
/Tarski_dev/Ch03_bet.v引理数：29
-
第四章：共线
/Tarski_dev/Ch04_col.v引理数：25
-
第四章：等长与中间性
/Tarski_dev/Ch04_cong_bet.v引理数：6
-
第五章：中间性和偏序*
/Tarski_dev/Ch05_bet_le.v引理数：66
-
第六章：
out谓词*/Tarski_dev/Ch06_out_lines.v引理数：54
-
第七章：中点
/Tarski_dev/Ch07_midpoint.v引理数：55
-
第八章：垂直
/Tarski_dev/Ch08_orthogonality.v引理数：94
-
第九章：平面
/Tarski_dev/Ch09_plane.v引理数：111
-
第十章：线的自反性1*
/Tarski_dev/Ch10_line_reflexivity.v引理数：41
-
第十章：线的自反性2*
/Tarski_dev/Ch10_line_reflexivity_2.v引理数：31
-
第十一章：角
/Tarski_dev/Ch11_angles.v引理数：278
-
第十二章：平行
/Tarski_dev/Ch12_parallel.v引理数：84
-
第十二章：平行的内部决定性*
/Tarski_dev/Ch12_parallel_inter_dec.v引理数：30
-
第十三章：1.概述
/Tarski_dev/Ch13_1.v引理数：38
-
第十三章：2.长度
/Tarski_dev/Ch13_2_length.v引理数：22
-
第十三章：3.角度
/Tarski_dev/Ch13_3_angles.v引理数：66
-
第十三章：4.余弦
/Tarski_dev/Ch13_4_cos.v引理数：61
-
第十三章：5.帕普斯-帕斯卡定理
/Tarski_dev/Ch13_5_Pappus_Pascal.v引理数：16
-
第十三章：6.笛卡尔-海森堡定理
/Tarski_dev/Ch13_6_Desargues_Hessenberg.v引理数：12
-
第十四章：1.序*
/Tarski_dev/Ch14_order.v引理数：36
-
第十四章：2.
Prod谓词*/Tarski_dev/Ch14_prod.v引理数：37
-
第十四章：3.
Sum谓词*/Tarski_dev/Ch14_sum.v引理数：95
-
第十五章：1.长度*
/Tarski_dev/Ch15_lengths.v引理数：79
-
第十五章：2.
PythRel谓词*/Tarski_dev/Ch15_pyth_rel.v引理数：5
-
第十六章：1.坐标
/Tarski_dev/Ch16_coordinates.v引理数：27
-
第十六章：2.坐标与函数*
/Tarski_dev/Ch16_coordinates_with_functions.v引理数：96
-
圆
/Tarski_dev/Annexes/circles.v引理数：104
-
共面
/Tarski_dev/Annexes/coplanar.v引理数：68
-
三角形内角和与平角之差（
defect）/Tarski_dev/Annexes/defect.v引理数：18
-
半角
/Tarski_dev/Annexes/half_angles.v引理数：50
-
圆周角*
/Tarski_dev/Annexes/inscribed_angle.v引理数：33
-
中位线
/Tarski_dev/Annexes/midpoint_theorems.v引理数：22
-
中垂线
/Tarski_dev/Annexes/perp_bisect.v引理数：17
-
投影*
/Tarski_dev/Annexes/project.v引理数：42
-
四边形内部决定性*
/Tarski_dev/Annexes/quadrilaterals_inter_dec.v引理数：105
-
四边形
/Tarski_dev/Annexes/quadrilaterals.v引理数：79
-
菱形
/Tarski_dev/Annexes/rhombus.v引理数：11
-
萨凯里四边形
/Tarski_dev/Annexes/saccheri.v引理数：95
-
角度之和
/Tarski_dev/Annexes/suma.v引理数：108
-
长度之和
/Tarski_dev/Annexes/sums.v引理数：39
-
标记谓词*
/Tarski_dev/Annexes/Tagged_predicates.v引理数：25
-
相切圆和相交圆
/Tarski_dev/Annexes/tangency.v引理数：15
-
向量*
/Tarski_dev/Annexes/vectors.v引理数：52
暂时不翻译
暂时不翻译