mathmatic_in_elementary_number_th

初等数论讲义的形式化证明 by lean

版本

使用的 lean4 版本为 v4.24.0-rc1 以及相对应版本的 mathlib

Contents

Ch1_Greatest_Common_Divisor

• Ch1_1_Excat_Division
• Ch1_2_Division_with_remainder
• Ch1_3_Greatest_Common_Divisor
• ch1_4_Bezout_Identity

Ch2_Prime_Numbers

• ch2_1_Prime_numbers
• Ch2_2_Prime_Number_Theorem
• Ch2_3_Fundamental _theoem_of_arithmetic
• Ch2_4_p-adic_valuation

Ch3_Congruences

• Ch3_1_congruences
• Ch3_2_Wilson's_theorem
• Ch3_3_Euler's_theorem

Ch4_Linear_Congruence_Equation

• Ch4_1_Algebraic_Congruence_Equation
• Ch4_2_Linear_Congruence_Equation
• Ch4_3_Chinese_Remainder_Theorem

Ch5_Quardratic_Congruence_Equation_Modulo_A_Prime

• Ch5_1_Quadratic_Residues
• Ch5_2_Legendre_Symbol
• Ch5_2_Legendre_Symbol
• Ch5_2_Legendre_Symbol
• Ch5_2_Legendre_Symbol

形式化证明目标

证明目标选用 青岛大学 刘奎,杨炯老师的英文讲义

结构

1. 证明的主体部分在 MathmaticInElementaryNumberTh 中, 按照章节 ch 分类

细节

1. 讲义中使用的 Definition, 通常用 def 表示

2. 因为lean中用来陈述和证明数学命题的关键词 仅有 theorem, lemma, example 无法满足讲义中所使用的 Proposition Corollary Theorem 等需求, 故在证明过程中均用 theorem 表示. 而讲义中的 Lemma,以及讲义中未出现但是为了方便后续证明的小命题, 在证明过程中使用同名 lemma 表示

3. 在 mathlib 中 已有的部分基础命题, 统一使用 mathlib 中给的证明或命题表示

4. 我们省略了讲义中部分简单的 example

环境

我们在以下系统上运行良好:

1. ubuntu 24.04
2. windows10
3. macos 26

事实上本项目并不大,只要您的设备支持 lean4 ,都是可以运行

如果您的设备上没有 mathlib 建议为安装mathlib至少预留 8 G

快速开始

参见 Install Lean.

小工具

为了将 MathmaticInElementaryNumberTh 中文件转为json

可以使用 lean_to_json.py

遇到问题?

如果您关于本项目有任何疑惑或问题,请通过以下联系我: