diff --git a/404.html b/404.html index 2fd5e4b..800d8cf 100644 --- a/404.html +++ b/404.html @@ -3,7 +3,7 @@ - 404 | PKU BiCMR AI for Math + 404 | PKU BICMR AI for Math @@ -13,8 +13,8 @@ -
PKU BiCMR AI for Math

Appearance

404

PAGE NOT FOUND

But if you don't change your direction, and if you keep looking, you may end up where you are heading.
Take me home
- +
PKU BICMR AI for Math

Appearance

404

PAGE NOT FOUND

But if you don't change your direction, and if you keep looking, you may end up where you are heading.
Take me home
+ \ No newline at end of file diff --git a/about.html b/about.html index bdb21a7..0325ac9 100644 --- a/about.html +++ b/about.html @@ -3,8 +3,8 @@ - About | PKU BiCMR AI for Math - + About | PKU BICMR AI for Math + @@ -16,8 +16,8 @@ -
PKU BiCMR AI for Math

Appearance

On this page

About ​

北京大学北京国际数学研究中心致力于培养有志于从事基础数学和应用数学研究的拔尖人才。 近年来，人工智能赋能科学研究的「AI for Science」新范式蓬勃发展，然而人工智能在数学领域，特别是在定理证明方面仍充满挑战。 传统上数学形式化和定理证明由数学家完成，但是这种方式需要花费大量时间和精力，并且存在人为疏漏和错误的风险。 人工智能的发展给数学形式化和定理证明带来了新的机遇。

- +
PKU BICMR AI for Math

Appearance

On this page

About ​

北京大学北京国际数学研究中心致力于培养有志于从事基础数学和应用数学研究的拔尖人才。 近年来，人工智能赋能科学研究的「AI for Science」新范式蓬勃发展，然而人工智能在数学领域，特别是在定理证明方面仍充满挑战。 传统上数学形式化和定理证明由数学家完成，但是这种方式需要花费大量时间和精力，并且存在人为疏漏和错误的风险。 人工智能的发展给数学形式化和定理证明带来了新的机遇。

+ \ No newline at end of file diff --git a/assets/index.md.abcc0f95.js b/assets/index.md.54d7a111.js similarity index 73% rename from assets/index.md.abcc0f95.js rename to assets/index.md.54d7a111.js index d1ff6d2..13ab995 100644 --- a/assets/index.md.abcc0f95.js +++ b/assets/index.md.54d7a111.js @@ -1 +1 @@ -import{_ as e,v as t,b as a}from"./chunks/framework.3ac7bdc3.js";const x=JSON.parse('{"title":"","description":"","frontmatter":{"layout":"home","hero":{"name":"BiCMR AI for Mathematics","text":"Formalization and Theorem Proving Seminar","tagline":"北京大学北京国际数学研究中心「AI for Mathematics：数学形式化和定理证明」本科生暑期科研培训班","actions":[{"theme":"brand","text":"View Research Projects","link":"/research-projects"},{"theme":"alt","text":"View Team Exercises","link":"/team-exercises"}]}},"headers":[],"relativePath":"index.md","filePath":"index.md"}'),r={name:"index.md"};function i(s,n,o,c,m,d){return t(),a("div")}const p=e(r,[["render",i]]);export{x as __pageData,p as default}; +import{_ as e,v as t,b as a}from"./chunks/framework.3ac7bdc3.js";const x=JSON.parse('{"title":"","description":"","frontmatter":{"layout":"home","hero":{"name":"BICMR AI for Mathematics","text":"Formalization and Theorem Proving Seminar","tagline":"北京大学北京国际数学研究中心「AI for Mathematics：数学形式化和定理证明」本科生暑期科研培训班","actions":[{"theme":"brand","text":"View Research Projects","link":"/research-projects"},{"theme":"alt","text":"View Team Exercises","link":"/team-exercises"}]}},"headers":[],"relativePath":"index.md","filePath":"index.md"}'),r={name:"index.md"};function s(i,n,o,c,m,d){return t(),a("div")}const p=e(r,[["render",s]]);export{x as __pageData,p as default}; diff --git a/assets/index.md.abcc0f95.lean.js b/assets/index.md.54d7a111.lean.js similarity index 73% rename from assets/index.md.abcc0f95.lean.js rename to assets/index.md.54d7a111.lean.js index d1ff6d2..13ab995 100644 --- a/assets/index.md.abcc0f95.lean.js +++ b/assets/index.md.54d7a111.lean.js @@ -1 +1 @@ -import{_ as e,v as t,b as a}from"./chunks/framework.3ac7bdc3.js";const x=JSON.parse('{"title":"","description":"","frontmatter":{"layout":"home","hero":{"name":"BiCMR AI for Mathematics","text":"Formalization and Theorem Proving Seminar","tagline":"北京大学北京国际数学研究中心「AI for Mathematics：数学形式化和定理证明」本科生暑期科研培训班","actions":[{"theme":"brand","text":"View Research Projects","link":"/research-projects"},{"theme":"alt","text":"View Team Exercises","link":"/team-exercises"}]}},"headers":[],"relativePath":"index.md","filePath":"index.md"}'),r={name:"index.md"};function i(s,n,o,c,m,d){return t(),a("div")}const p=e(r,[["render",i]]);export{x as __pageData,p as default}; +import{_ as e,v as t,b as a}from"./chunks/framework.3ac7bdc3.js";const x=JSON.parse('{"title":"","description":"","frontmatter":{"layout":"home","hero":{"name":"BICMR AI for Mathematics","text":"Formalization and Theorem Proving Seminar","tagline":"北京大学北京国际数学研究中心「AI for Mathematics：数学形式化和定理证明」本科生暑期科研培训班","actions":[{"theme":"brand","text":"View Research Projects","link":"/research-projects"},{"theme":"alt","text":"View Team Exercises","link":"/team-exercises"}]}},"headers":[],"relativePath":"index.md","filePath":"index.md"}'),r={name:"index.md"};function s(i,n,o,c,m,d){return t(),a("div")}const p=e(r,[["render",s]]);export{x as __pageData,p as default}; diff --git a/draft/fp/index.html b/draft/fp/index.html index 38ef79c..e594571 100644 --- a/draft/fp/index.html +++ b/draft/fp/index.html @@ -3,8 +3,8 @@ - Hacking Lean in Lean: A Crash Course | PKU BiCMR AI for Math - + Hacking Lean in Lean: A Crash Course | PKU BICMR AI for Math + @@ -16,8 +16,8 @@ -
PKU BiCMR AI for Math

Appearance

On this page

Hacking Lean in Lean: A Crash Course ​

Functional Programming in Lean ​

2023/08/08 revised ​

Metaprogramming in Lean, Part I ​

Metaprogramming in Lean, Part II ​

- +
PKU BICMR AI for Math

Appearance

On this page

Hacking Lean in Lean: A Crash Course ​

Functional Programming in Lean ​

2023/08/08 revised ​

Metaprogramming in Lean, Part I ​

Metaprogramming in Lean, Part II ​

+ \ No newline at end of file diff --git a/draft/fp/l0.html b/draft/fp/l0.html index 524c573..455ac70 100644 --- a/draft/fp/l0.html +++ b/draft/fp/l0.html @@ -3,8 +3,8 @@ - Lean 函数式程序设计 | PKU BiCMR AI for Math - + Lean 函数式程序设计 | PKU BICMR AI for Math + @@ -16,7 +16,7 @@ -
PKU BiCMR AI for Math

Appearance

On this page

Lean 函数式程序设计 ​

动机 ​

  • 许多策略会被翻译成函数式程序设计的常见组分，学习函数式程序设计对读懂这些策略具体如何工作有帮助
Lean4
def id {A : Type _} (x : A) : A := x
+    
PKU BICMR AI for Math
Appearance
On this page
Lean 函数式程序设计 ​
动机 ​
  • 许多策略会被翻译成函数式程序设计的常见组分，学习函数式程序设计对读懂这些策略具体如何工作有帮助
Lean4
def id {A : Type _} (x : A) : A := x
 
 def id : {A : Type _} -> (x : A) -> A := fun x => x
 
@@ -97,7 +97,7 @@
     | .bind xs k =>
         let ⟨x, st⟩ := runState init xs
         runState st (k x)
  • Identity
  • StateT
Intuitionistic Logic ​
Further Reading ​

-    
+    
     
   
 
\ No newline at end of file
diff --git a/draft/fp/l0/23-08-08.html b/draft/fp/l0/23-08-08.html
index 5276c76..f58ab5d 100644
--- a/draft/fp/l0/23-08-08.html
+++ b/draft/fp/l0/23-08-08.html
@@ -3,8 +3,8 @@
   
     
     
-    2023/08/08 revised | PKU BiCMR AI for Math
-    
+    2023/08/08 revised | PKU BICMR AI for Math
+    
     
     
     
@@ -16,7 +16,7 @@
     
   
   
-    
PKU BiCMR AI for Math
Appearance
On this page
2023/08/08 revised ​
Lean4
import Mathlib.Init.Logic
+    
PKU BICMR AI for Math
Appearance
On this page
2023/08/08 revised ​
Lean4
import Mathlib.Init.Logic
 
 inductive ℕ where
   | zero : ℕ
@@ -159,7 +159,7 @@
   bind [0, 1, 2, 3, 4, 5] fun x =>
     bind [0, 1, 2, 3, 4, 5] fun y =>
       pure ⟨x, y⟩

-    
+    
     
   
 
\ No newline at end of file
diff --git a/draft/impl.html b/draft/impl.html
index 986a4fa..c6aa864 100644
--- a/draft/impl.html
+++ b/draft/impl.html
@@ -3,8 +3,8 @@
   
     
     
-    基于依赖类型论的定理证明器实现简介 | PKU BiCMR AI for Math
-    
+    基于依赖类型论的定理证明器实现简介 | PKU BICMR AI for Math
+    
     
     
     
@@ -16,8 +16,8 @@
     
   
   
-    
PKU BiCMR AI for Math
Appearance
On this page
基于依赖类型论的定理证明器实现简介 ​
本文旨在介绍一些有关基于依赖类型论的定理证明器实现的经典技术、问题、定义与例子。 由于编写时间与篇幅受限，且存在相关材料已经给出了经典的论述，定义与例子的叙述会相对不详细与形式化。此时需要从所引用的文本中阅读对应的内容。 依赖类型论为实现更接近日常数学所用的定理证明器提供了新的基础。「命题即类型，证明即程序，证明化简即程序求值」的对应为数学语言与计算机语言的合一化提供了自然的形式化思路。Propositions as Types
从而，检查证明步骤的正确性的问题便转化为了检查程序类型的工作。
依赖类型论的程序类型检查并不容易，需要相对较久的时间：
  • 类型检查中涉及求值操作
  • 应当允许用户在一些地方不将类型写完全或省略类型
  • 无处不在的依赖类型模式匹配
  • 常使用 ad-hoc 多态
  • 常使用 tactics 来生成 terms
  • 较为复杂的类型论（如同伦类型论的可计算解释的实现）有关原始对象的操作是非平凡的 A new “Brunerie number”, might be easier to calculate?
也有一些在数学上较为成功的定理证明器是基于非依赖类型论的，或者说，相对「简单」的类型论。Formalising Mathematics In Simple Type Theory
由于它们的实现关注点与基于依赖类型论的定理证明器有较大差别，在本文中我们不会介绍。 另外，一些比较经典的编译器议题虽然会影响定理证明器的性能与运行速度，但由于太通用或已经被研究较深（如 parsing），在本文中也不会加以介绍。
本文对技术的介绍有一定的选择性，能达到同样目的的多个手段可能只会介绍一个。本文关注技术手段在当下流行的定理证明器中的具体实现。 基于各种依赖类型论变体的 Coq、Agda、Lean 都是当下相对流行，且在数学上取得一定成就的定理证明器。效率与表达能力也是它们关心的主要议题之一。 在下面的介绍中，或多或少会出现它们发展的轨迹。
主要环节 ​
我们在这里使用「环节」而不是「流程」，是因为这些概念可能是同时或重叠发生的。由于文本总是线性的叙述，我们从「不清楚类型检查是什么」的设定开始介绍。
我们所讨论的的技术主要适用于实现 Martin-Löf type theory（MLTT）及变体。有关介绍 MLTT 的内容浩如烟海，可以参考主流的一些类型论教材。在实现更为复杂的类型论，如 Cubical Type Theory 时，虽然本文介绍的内容仍然有相当大一部分能适用，但一些额外的实现需求与策略也需要注意。cctt
此外，有一些关于 MLTT 及变体实现相关性能研究的资料：
Typing ​
类型检查关注一个给定的项 xx 在给定的上下文 Γ\Gamma 中是否属于一个给定的类型 AA，计作 Γ⊢x:A\Gamma \vdash x : A。 类型检查是通过将推演规则（derivation rules）应用到语法上，得到完整推演过程的机械化操作，可以使用算法进行描述。 最简陋的类型检查算法只关心推演规则中每个类型的形成规则、引入规则与消去规则（与必要的逻辑规则，如上下文有关的操作）。简单的类型检查的例子参见 Type Theory and Formal Proof, Ch2 Sec8 Type Checking in λ→\lambda_{\to} 与 Programming Language Foundations in Agda: Lambda； 较为先进的类型检查算法除了能自动插入一些隐式参数与根据上下文求解用户没有显式写出的内容。 因此，除了每个类型的形成规则、引入规则与消去规则外，较为先进的类型检查算法还关心推演规则中的一些有关类型的其他性质。
非形式化地讲，在相对简单的类型理论 —— 如 λ→×N\lambda_{\to \times \mathbb N}（即有函数类型、Cartesian 积与自然数的类型论）—— 中，去描述类型检查的过程是相对容易的。 例如，对于项 f:=λ(x,y).(y,0)f := \lambda (x, y) . (y, 0)，要检查 Γ,x:N,y:N⊢f:N×N→N×N\Gamma, x : \mathbb N, y : \mathbb N \vdash f : \mathbb N \times \mathbb N \to \mathbb N \times \mathbb N，即写出它的完整推演：
  • 对于 00，考虑 N\mathbb N 的引入规则，有 ∅⊢0:N\empty \vdash 0 : \mathbb N
  • 对于 yy，由于上下文中有 y:Ny : \mathbb N，有 y:N⊢y:Ny : \mathbb N \vdash y : \mathbb N
  • 对于 (y,0)(y, 0)，考虑 ×\times 的引入规则 (_,_)(\_,\_)，有 y:N⊢(y,_):N×_y : \mathbb N \vdash (y, \_) : \mathbb N \times \_，进一步有 y:N⊢(y,0):N×Ny : \mathbb N \vdash (y, 0) : \mathbb N \times \mathbb N
  • 对于 λ(x,y).(y,0)\lambda (x, y) . (y, 0)，由于 y:N⊢(y,0):N×Ny : \mathbb N \vdash (y, 0) : \mathbb N \times \mathbb N，考虑 →\to 的引入规则 λ\lambda 与 ×\times 的引入规则 (_,_)(\_,\_)，有 x:N,y:N⊢(x,y):N×Nx : \mathbb N, y : \mathbb N \vdash (x, y) : \mathbb N \times \mathbb N，进一步 x:N,y:N⊢λ(x,y)._:N×N→_x : \mathbb N, y : \mathbb N \vdash \lambda (x, y) . \_ : \mathbb N \times \mathbb N \to \_，进一步有 Γ,x:N,y:N⊢f:N×N→N×N\Gamma, x : \mathbb N, y : \mathbb N \vdash f : \mathbb N \times \mathbb N \to \mathbb N \times \mathbb N
对于项 xs:N×N\mathrm{xs} : \mathbb N \times \mathbb N，要检查 Γ⊢f xs:N×N\Gamma \vdash f\ \mathrm{xs} : \mathbb N \times \mathbb N，只需要考虑 →\to 的消去规则。
从上面的例子，我们可以注意到：
  • 在简单的类型系统中，复杂的类型是由基础类型（此处为 N\mathbb N）、类型构造子（此处为分别接受两个参数的 →\to 与 ×\times），通过有限次应用组合而成。对应的类型检查也跟随组合的风格，首先对 subterm 进行检查，再应用推演规则来组合成完整的推演过程。
  • 一些项即使不标注类型，我们也能合成出它所属于的类型。这样的操作被称为类型合成。考虑这样的表述：对于 Γ⊢x:A\Gamma \vdash x : A，如果三元组 (Γ,x,A)(\Gamma, x, A) 的所有元素都被给出，写出完整推演过程被称为类型检查；如果缺失类型 (Γ,x,_)(\Gamma, x, \_)，写出合成缺失类型的推演过程被称为类型合成。类型检查与类型合成合称 typing。在这一领域有优秀的综述 Bidirectional Typing。有关 typing 理论的一个重要推论是，易用定理证明器的 typing 能力需要满足用户只需要显式为 top-level 的定义与引入规则消除规则相接出现的定义标注类型，其他部分项定义的类型可以不用被标注。
综述 Bidirectional Typing 与同名的 typing 策略指出，一些项的类型是适合被检查的，一些项的类型是适合被合成的。当需要检查 Γ⊢x:A\Gamma \vdash x : A 时，如果其中的 xx 是适合类型合成的项，则会采取首先合成一个类型 A′A'，再比较 AA 与 A′A' 是否相等。于是，我们需要定义类型的相等。在简单的类型系统中，类型的相等定义跟随之前所描述的类型检查相同的组合风格，即结构化的比较是否是由相同的类型构造子所构造，递归比较参数是否相等。在依赖类型论的定理证明器中，情况变得复杂：由于我们有对类型做语法抽象操作的能力（Π\Pi-types），我们需要处理非 closed term；由于在依赖类型论中，常常有形如 A:UA : \mathcal U 的设定，我们在推演系统中无需为类型的相等添加新的 judgement，我们也可以定义类型上的函数，通过函数应用获得输出的类型。类型的相等定义变得非平凡，一个朴素的想法是我们可以比较已经被充分做 reduction 后的类型，或者说，进行 normalise 后的结果。
Evaluation ​
论文 A simple type-theoretic language: Mini-TT 为一般的依赖类型论语言/定理证明器提供了定义判断类型相等算法的思路，即 Normalisation by Evaluation（NbE）：语法域与语义域被分离，语法上的 open term 在语义中也有了对应的表示；操作 eval\mathtt{eval} 在给定的环境下将语法域元素映射到语义域，操作 readback\mathtt{readback} 将给定的自由变元集与语义域元素映射到语法域。求语法域元素的 normal form 即操作 eval\mathtt{eval} 与 readback\mathtt{readback} 的组合。注意这些操作都允许非 closed term 存在，由于我们有对类型做语法抽象操作的能力，比较 open terms 是否可相互转换是不可避免的。现在，我们可以定义一般的依赖类型论语言/定理证明器中类型的判断相等操作 conv\mathtt{conv}。注意 conv\mathtt{conv} 不需要一个 term 达到 normal form，而只需要结构化地比较语义域元素元素是否相等。
一个立方类型论的实现 cubicaltt 正是基于 Mini-TT 而作。
NbE 的语义基础参见 Normalization by Evaluation Dependent: Types and Impredicativity。也有许多优秀的 NbE 实现教程，如 Checking Dependent Types with Normalization by Evaluation、Elaboration Zoo。
值的表示 ​
依赖类型论语言/定理证明器的 core terms 求值过程往往接近 untyped λ\lambda-calculus 的求值过程。 这是由于在通过类型检查后，类型的形成规则、引入规则、消除规则的出现都是符合类型系统规则的；且求值时，类型的形成规则、引入规则被翻译成语义域值的构造器，类型的消除规则被翻译为在被消除的项是值时计算出符合语义的结果、在被消除的项是 neutral terms 时构造更大的 neutral terms 的过程。从而，此处 core terms 的求值过程与 untyped λ\lambda-calculus 是接近的，但是如果要达到 normal form，在 readback\mathtt{readback} 时还需要按照类型信息将项变换到 canonical form。
而 λ\lambda-calculus 演算的各种求值策略与概念也被广泛研究。 在描述 λ\lambda-calculus 的语义域时需要注意 λ\lambda term 的 body 是可能且常常出现捕获情况的，常用的处理如： 使用高阶抽象语法（HOAS）实现 λ\lambda-calculus 将 λ\lambda terms 直接翻译为 host language 的函数对象（如匿名函数），higher-order 即是这里 host language 的函数；使用 closure 实现将 λ\lambda terms 翻译为携带环境的 open term。对应的函数应用的实现是自然的。
理论基础：A Functional Correspondence between Evaluators and Abstract Machines
参考实现：Elaboration Zoo
目前依赖类型定理语言/证明器中较为标准的实现是 closure 表示的变体，这是由于
  • object language 中函数相等的定义更容易表达
  • 常用 host languages 中的函数对象无法序列化或打印
  • closure 实现更容易实现一些传统的编译器优化技术
等原因。
Unification ​
易用的定理证明器应当允许用户省略一些类型标注、实例标注并提供自动参数和自动证明 absurd pattern 等功能。Typing、Unification、Pattern Matching、Typeclass Resolution 等环节都实现了一定的相关功能。
最简单的 unification 问题可以从这样的需求出发：我们希望用类型来引导程序的设计，未完成的程序被称为洞、有时我们想要省略一些类型标注、有时我们希望能使用策略来让定理证明的语言更加贴近自然的思维模式。Type-Driven Development with Idris
最简单的 unification 的问题是 pattern unification。考虑这样的例子：要求解等式 ?α spine=RHS?\alpha\ \mathrm{spine} = \mathrm{RHS}，如果有
  • spine\mathrm{spine} 由不同的受约变元组成
  • RHS\mathrm{RHS} 中的自由变元都在 spine\mathrm{spine} 中
  • 元变元 ?α?\alpha 不在 RHS\mathrm{RHS} 出现
这样的 unification 问题求解相对较为简单，能求解的问题类别也相对受限。Elaboration Zoo
更复杂的 unification 问题往往是不可判定的，如 higher-order unification。论文 Unification of Simply Typed Lambda-Terms as Logic Programming 指出了一些可判定的部分（也是 pattern unification 中 pattern 一词的来源，pattern fragment），并且陈述：
The unification of simply typed λ-terms modulo the rules of β- and η-conversions is often called “higher-order” unification because of the possible presence of variables of functional type.
In order to avoid using the very vague and over used adjective “higher-order”, we shall refer to the problem of unifying simply typed λ-terms modulo β- and η-conversion as βη-unification.
有关这类更复杂的 unification 问题参见 Higher-Order Dynamic Pattern Unification for Dependent Types and Records。同时它也是 Agda 实现 unification 的理论参考。此外，一个有趣的原型参见 Functional Pearl: Dependent type inference via free higher-order unification。
Pattern Matching ​
当我们要归纳地去引入一个类型时 Homotopy Type Theory, Remark 1.5.1. There is a general pattern for introduction of a new kind of type in type theory，定义这个类型，也就是说：
  1. formation rules
  2. introduction rules
  3. elimination rules
  4. computation rule
  5. (optional) uniqueness principle
例如，考虑我们如何定义自然数类型，并且使用这里定义的类型来定义新操作与证明操作相关的性质。(可以观察在 Coq 中 inductive 地声明一个 type 后，它自动生成了哪些定义)
Symmetry, 2.4 The type of natural numbers
直接使用 induction principle 来写定义与作证明相对比较繁琐，许多简明的形式也无法展现。 在 Homotopy Type Theory,, 1.10 Pattern matching and recursion 描述了一种简洁的记法，即模式匹配。
模式匹配是一系列机械化的方法，将定义等式翻译为类型的消除规则。但在实现上有多种候选，如 case tree 等。 在翻译定义等式的过程中也有一系列重要问题，如
等。
理论基础：Dependent pattern matching and proof-relevant unification
参考实现：Tiny Idris
Typeclass Resolution ​
理论基础：Tabled Typeclass Resolution
Tactics and Metaprogramming ​
论文 Idris, a General Purpose Dependently Typed Programming Language: Design and Implementation 中描述了依赖类型定理语言/证明器的 IR 分层与基础 tactics 的实现。论文 Elaborator Reflection: Extending Idris in Idris 是前篇论文的后续工作，此外在 Related Work 一节给出了有关 Tactics and Metaprogramming 相关其他工作的论述。
经典的优化手段 ​
Erasure ​
有些 term 在运行时不需要具体的表示。一个经典的例子是 Inductive Families Need Not Store Their Indices。
Idris 1 的编译器有判断 term 是否可以被 erasure 的机制 Erasure By Usage Analysis。Idris 2 的类型系统加入了一些新的原语 Idris 2: Quantitative Type Theory in Practice。Agda 也提供了类似的标记机制 Run-time Irrelevance。
Incremental Reparse ​
实现增量语法解析需要语法设计本身具有一些不变量，保证语法在一定单元内修改不会影响全局状态的合法性与解析结果不变。此外，选择合适的数据结构来表示语法树能使得修改操作相对低复杂度。rowan
在定理证明器中常常出现 macros 或其他元编程类似物，在实现增量语法解析式也需要加以考虑。Macros vs incremental parsing
Incremental Computation ​
许多传统语言编译器编译器被设计为 pass 构成的 pipeline。 交互式定理证明器有着编辑器交互性强、需要提供交互工具、常常需要增量计算修改、类型检查相对困难等特点。 在设计交互式定理证明器架构时就需要充分考虑到这些特点与困难。
Query-based compiler architectures
Durable Incrementality
Builtin ​
Agda Built-ins
Lean Builtin Types
FBIP ​
Functional but in-place 是纯函数式语言在保持纯函数式的同时，为了高效表示状态的一种优化。同时，reuse analysis 也降低了模式匹配等操作的开销。
Perceus: Garbage Free Reference Counting with Reuse
FP² : Fully in-Place Functional Programming
Glued Evaluation ​
Compiling with Continuations ​
Typeclass Organisation ​
Algebra Tactics Optimisation ​
理论基础：Reflexive Tactics for Algebra, Revisited
参考实现：Algebra Tactics
实现细节的技术选择 ​
Variable ​
Universe ​
Proof Irrelevance ​

-    
+    
PKU BICMR AI for Math
Appearance
On this page
基于依赖类型论的定理证明器实现简介 ​
本文旨在介绍一些有关基于依赖类型论的定理证明器实现的经典技术、问题、定义与例子。 由于编写时间与篇幅受限，且存在相关材料已经给出了经典的论述，定义与例子的叙述会相对不详细与形式化。此时需要从所引用的文本中阅读对应的内容。 依赖类型论为实现更接近日常数学所用的定理证明器提供了新的基础。「命题即类型，证明即程序，证明化简即程序求值」的对应为数学语言与计算机语言的合一化提供了自然的形式化思路。Propositions as Types
从而，检查证明步骤的正确性的问题便转化为了检查程序类型的工作。
依赖类型论的程序类型检查并不容易，需要相对较久的时间：
  • 类型检查中涉及求值操作
  • 应当允许用户在一些地方不将类型写完全或省略类型
  • 无处不在的依赖类型模式匹配
  • 常使用 ad-hoc 多态
  • 常使用 tactics 来生成 terms
  • 较为复杂的类型论（如同伦类型论的可计算解释的实现）有关原始对象的操作是非平凡的 A new “Brunerie number”, might be easier to calculate?
也有一些在数学上较为成功的定理证明器是基于非依赖类型论的，或者说，相对「简单」的类型论。Formalising Mathematics In Simple Type Theory
由于它们的实现关注点与基于依赖类型论的定理证明器有较大差别，在本文中我们不会介绍。 另外，一些比较经典的编译器议题虽然会影响定理证明器的性能与运行速度，但由于太通用或已经被研究较深（如 parsing），在本文中也不会加以介绍。
本文对技术的介绍有一定的选择性，能达到同样目的的多个手段可能只会介绍一个。本文关注技术手段在当下流行的定理证明器中的具体实现。 基于各种依赖类型论变体的 Coq、Agda、Lean 都是当下相对流行，且在数学上取得一定成就的定理证明器。效率与表达能力也是它们关心的主要议题之一。 在下面的介绍中，或多或少会出现它们发展的轨迹。
主要环节 ​
我们在这里使用「环节」而不是「流程」，是因为这些概念可能是同时或重叠发生的。由于文本总是线性的叙述，我们从「不清楚类型检查是什么」的设定开始介绍。
我们所讨论的的技术主要适用于实现 Martin-Löf type theory（MLTT）及变体。有关介绍 MLTT 的内容浩如烟海，可以参考主流的一些类型论教材。在实现更为复杂的类型论，如 Cubical Type Theory 时，虽然本文介绍的内容仍然有相当大一部分能适用，但一些额外的实现需求与策略也需要注意。cctt
此外，有一些关于 MLTT 及变体实现相关性能研究的资料：
Typing ​
类型检查关注一个给定的项 xx 在给定的上下文 Γ\Gamma 中是否属于一个给定的类型 AA，计作 Γ⊢x:A\Gamma \vdash x : A。 类型检查是通过将推演规则（derivation rules）应用到语法上，得到完整推演过程的机械化操作，可以使用算法进行描述。 最简陋的类型检查算法只关心推演规则中每个类型的形成规则、引入规则与消去规则（与必要的逻辑规则，如上下文有关的操作）。简单的类型检查的例子参见 Type Theory and Formal Proof, Ch2 Sec8 Type Checking in λ→\lambda_{\to} 与 Programming Language Foundations in Agda: Lambda； 较为先进的类型检查算法除了能自动插入一些隐式参数与根据上下文求解用户没有显式写出的内容。 因此，除了每个类型的形成规则、引入规则与消去规则外，较为先进的类型检查算法还关心推演规则中的一些有关类型的其他性质。
非形式化地讲，在相对简单的类型理论 —— 如 λ→×N\lambda_{\to \times \mathbb N}（即有函数类型、Cartesian 积与自然数的类型论）—— 中，去描述类型检查的过程是相对容易的。 例如，对于项 f:=λ(x,y).(y,0)f := \lambda (x, y) . (y, 0)，要检查 Γ,x:N,y:N⊢f:N×N→N×N\Gamma, x : \mathbb N, y : \mathbb N \vdash f : \mathbb N \times \mathbb N \to \mathbb N \times \mathbb N，即写出它的完整推演：
  • 对于 00，考虑 N\mathbb N 的引入规则，有 ∅⊢0:N\empty \vdash 0 : \mathbb N
  • 对于 yy，由于上下文中有 y:Ny : \mathbb N，有 y:N⊢y:Ny : \mathbb N \vdash y : \mathbb N
  • 对于 (y,0)(y, 0)，考虑 ×\times 的引入规则 (_,_)(\_,\_)，有 y:N⊢(y,_):N×_y : \mathbb N \vdash (y, \_) : \mathbb N \times \_，进一步有 y:N⊢(y,0):N×Ny : \mathbb N \vdash (y, 0) : \mathbb N \times \mathbb N
  • 对于 λ(x,y).(y,0)\lambda (x, y) . (y, 0)，由于 y:N⊢(y,0):N×Ny : \mathbb N \vdash (y, 0) : \mathbb N \times \mathbb N，考虑 →\to 的引入规则 λ\lambda 与 ×\times 的引入规则 (_,_)(\_,\_)，有 x:N,y:N⊢(x,y):N×Nx : \mathbb N, y : \mathbb N \vdash (x, y) : \mathbb N \times \mathbb N，进一步 x:N,y:N⊢λ(x,y)._:N×N→_x : \mathbb N, y : \mathbb N \vdash \lambda (x, y) . \_ : \mathbb N \times \mathbb N \to \_，进一步有 Γ,x:N,y:N⊢f:N×N→N×N\Gamma, x : \mathbb N, y : \mathbb N \vdash f : \mathbb N \times \mathbb N \to \mathbb N \times \mathbb N
对于项 xs:N×N\mathrm{xs} : \mathbb N \times \mathbb N，要检查 Γ⊢f xs:N×N\Gamma \vdash f\ \mathrm{xs} : \mathbb N \times \mathbb N，只需要考虑 →\to 的消去规则。
从上面的例子，我们可以注意到：
  • 在简单的类型系统中，复杂的类型是由基础类型（此处为 N\mathbb N）、类型构造子（此处为分别接受两个参数的 →\to 与 ×\times），通过有限次应用组合而成。对应的类型检查也跟随组合的风格，首先对 subterm 进行检查，再应用推演规则来组合成完整的推演过程。
  • 一些项即使不标注类型，我们也能合成出它所属于的类型。这样的操作被称为类型合成。考虑这样的表述：对于 Γ⊢x:A\Gamma \vdash x : A，如果三元组 (Γ,x,A)(\Gamma, x, A) 的所有元素都被给出，写出完整推演过程被称为类型检查；如果缺失类型 (Γ,x,_)(\Gamma, x, \_)，写出合成缺失类型的推演过程被称为类型合成。类型检查与类型合成合称 typing。在这一领域有优秀的综述 Bidirectional Typing。有关 typing 理论的一个重要推论是，易用定理证明器的 typing 能力需要满足用户只需要显式为 top-level 的定义与引入规则消除规则相接出现的定义标注类型，其他部分项定义的类型可以不用被标注。
综述 Bidirectional Typing 与同名的 typing 策略指出，一些项的类型是适合被检查的，一些项的类型是适合被合成的。当需要检查 Γ⊢x:A\Gamma \vdash x : A 时，如果其中的 xx 是适合类型合成的项，则会采取首先合成一个类型 A′A'，再比较 AA 与 A′A' 是否相等。于是，我们需要定义类型的相等。在简单的类型系统中，类型的相等定义跟随之前所描述的类型检查相同的组合风格，即结构化的比较是否是由相同的类型构造子所构造，递归比较参数是否相等。在依赖类型论的定理证明器中，情况变得复杂：由于我们有对类型做语法抽象操作的能力（Π\Pi-types），我们需要处理非 closed term；由于在依赖类型论中，常常有形如 A:UA : \mathcal U 的设定，我们在推演系统中无需为类型的相等添加新的 judgement，我们也可以定义类型上的函数，通过函数应用获得输出的类型。类型的相等定义变得非平凡，一个朴素的想法是我们可以比较已经被充分做 reduction 后的类型，或者说，进行 normalise 后的结果。
Evaluation ​
论文 A simple type-theoretic language: Mini-TT 为一般的依赖类型论语言/定理证明器提供了定义判断类型相等算法的思路，即 Normalisation by Evaluation（NbE）：语法域与语义域被分离，语法上的 open term 在语义中也有了对应的表示；操作 eval\mathtt{eval} 在给定的环境下将语法域元素映射到语义域，操作 readback\mathtt{readback} 将给定的自由变元集与语义域元素映射到语法域。求语法域元素的 normal form 即操作 eval\mathtt{eval} 与 readback\mathtt{readback} 的组合。注意这些操作都允许非 closed term 存在，由于我们有对类型做语法抽象操作的能力，比较 open terms 是否可相互转换是不可避免的。现在，我们可以定义一般的依赖类型论语言/定理证明器中类型的判断相等操作 conv\mathtt{conv}。注意 conv\mathtt{conv} 不需要一个 term 达到 normal form，而只需要结构化地比较语义域元素元素是否相等。
一个立方类型论的实现 cubicaltt 正是基于 Mini-TT 而作。
NbE 的语义基础参见 Normalization by Evaluation Dependent: Types and Impredicativity。也有许多优秀的 NbE 实现教程，如 Checking Dependent Types with Normalization by Evaluation、Elaboration Zoo。
值的表示 ​
依赖类型论语言/定理证明器的 core terms 求值过程往往接近 untyped λ\lambda-calculus 的求值过程。 这是由于在通过类型检查后，类型的形成规则、引入规则、消除规则的出现都是符合类型系统规则的；且求值时，类型的形成规则、引入规则被翻译成语义域值的构造器，类型的消除规则被翻译为在被消除的项是值时计算出符合语义的结果、在被消除的项是 neutral terms 时构造更大的 neutral terms 的过程。从而，此处 core terms 的求值过程与 untyped λ\lambda-calculus 是接近的，但是如果要达到 normal form，在 readback\mathtt{readback} 时还需要按照类型信息将项变换到 canonical form。
而 λ\lambda-calculus 演算的各种求值策略与概念也被广泛研究。 在描述 λ\lambda-calculus 的语义域时需要注意 λ\lambda term 的 body 是可能且常常出现捕获情况的，常用的处理如： 使用高阶抽象语法（HOAS）实现 λ\lambda-calculus 将 λ\lambda terms 直接翻译为 host language 的函数对象（如匿名函数），higher-order 即是这里 host language 的函数；使用 closure 实现将 λ\lambda terms 翻译为携带环境的 open term。对应的函数应用的实现是自然的。
理论基础：A Functional Correspondence between Evaluators and Abstract Machines
参考实现：Elaboration Zoo
目前依赖类型定理语言/证明器中较为标准的实现是 closure 表示的变体，这是由于
  • object language 中函数相等的定义更容易表达
  • 常用 host languages 中的函数对象无法序列化或打印
  • closure 实现更容易实现一些传统的编译器优化技术
等原因。
Unification ​
易用的定理证明器应当允许用户省略一些类型标注、实例标注并提供自动参数和自动证明 absurd pattern 等功能。Typing、Unification、Pattern Matching、Typeclass Resolution 等环节都实现了一定的相关功能。
最简单的 unification 问题可以从这样的需求出发：我们希望用类型来引导程序的设计，未完成的程序被称为洞、有时我们想要省略一些类型标注、有时我们希望能使用策略来让定理证明的语言更加贴近自然的思维模式。Type-Driven Development with Idris
最简单的 unification 的问题是 pattern unification。考虑这样的例子：要求解等式 ?α spine=RHS?\alpha\ \mathrm{spine} = \mathrm{RHS}，如果有
  • spine\mathrm{spine} 由不同的受约变元组成
  • RHS\mathrm{RHS} 中的自由变元都在 spine\mathrm{spine} 中
  • 元变元 ?α?\alpha 不在 RHS\mathrm{RHS} 出现
这样的 unification 问题求解相对较为简单，能求解的问题类别也相对受限。Elaboration Zoo
更复杂的 unification 问题往往是不可判定的，如 higher-order unification。论文 Unification of Simply Typed Lambda-Terms as Logic Programming 指出了一些可判定的部分（也是 pattern unification 中 pattern 一词的来源，pattern fragment），并且陈述：
The unification of simply typed λ-terms modulo the rules of β- and η-conversions is often called “higher-order” unification because of the possible presence of variables of functional type.
In order to avoid using the very vague and over used adjective “higher-order”, we shall refer to the problem of unifying simply typed λ-terms modulo β- and η-conversion as βη-unification.
有关这类更复杂的 unification 问题参见 Higher-Order Dynamic Pattern Unification for Dependent Types and Records。同时它也是 Agda 实现 unification 的理论参考。此外，一个有趣的原型参见 Functional Pearl: Dependent type inference via free higher-order unification。
Pattern Matching ​
当我们要归纳地去引入一个类型时 Homotopy Type Theory, Remark 1.5.1. There is a general pattern for introduction of a new kind of type in type theory，定义这个类型，也就是说：
  1. formation rules
  2. introduction rules
  3. elimination rules
  4. computation rule
  5. (optional) uniqueness principle
例如，考虑我们如何定义自然数类型，并且使用这里定义的类型来定义新操作与证明操作相关的性质。(可以观察在 Coq 中 inductive 地声明一个 type 后，它自动生成了哪些定义)
Symmetry, 2.4 The type of natural numbers
直接使用 induction principle 来写定义与作证明相对比较繁琐，许多简明的形式也无法展现。 在 Homotopy Type Theory,, 1.10 Pattern matching and recursion 描述了一种简洁的记法，即模式匹配。
模式匹配是一系列机械化的方法，将定义等式翻译为类型的消除规则。但在实现上有多种候选，如 case tree 等。 在翻译定义等式的过程中也有一系列重要问题，如
等。
理论基础：Dependent pattern matching and proof-relevant unification
参考实现：Tiny Idris
Typeclass Resolution ​
理论基础：Tabled Typeclass Resolution
Tactics and Metaprogramming ​
论文 Idris, a General Purpose Dependently Typed Programming Language: Design and Implementation 中描述了依赖类型定理语言/证明器的 IR 分层与基础 tactics 的实现。论文 Elaborator Reflection: Extending Idris in Idris 是前篇论文的后续工作，此外在 Related Work 一节给出了有关 Tactics and Metaprogramming 相关其他工作的论述。
经典的优化手段 ​
Erasure ​
有些 term 在运行时不需要具体的表示。一个经典的例子是 Inductive Families Need Not Store Their Indices。
Idris 1 的编译器有判断 term 是否可以被 erasure 的机制 Erasure By Usage Analysis。Idris 2 的类型系统加入了一些新的原语 Idris 2: Quantitative Type Theory in Practice。Agda 也提供了类似的标记机制 Run-time Irrelevance。
Incremental Reparse ​
实现增量语法解析需要语法设计本身具有一些不变量，保证语法在一定单元内修改不会影响全局状态的合法性与解析结果不变。此外，选择合适的数据结构来表示语法树能使得修改操作相对低复杂度。rowan
在定理证明器中常常出现 macros 或其他元编程类似物，在实现增量语法解析式也需要加以考虑。Macros vs incremental parsing
Incremental Computation ​
许多传统语言编译器编译器被设计为 pass 构成的 pipeline。 交互式定理证明器有着编辑器交互性强、需要提供交互工具、常常需要增量计算修改、类型检查相对困难等特点。 在设计交互式定理证明器架构时就需要充分考虑到这些特点与困难。
Query-based compiler architectures
Durable Incrementality
Builtin ​
Agda Built-ins
Lean Builtin Types
FBIP ​
Functional but in-place 是纯函数式语言在保持纯函数式的同时，为了高效表示状态的一种优化。同时，reuse analysis 也降低了模式匹配等操作的开销。
Perceus: Garbage Free Reference Counting with Reuse
FP² : Fully in-Place Functional Programming
Glued Evaluation ​
Compiling with Continuations ​
Typeclass Organisation ​
Algebra Tactics Optimisation ​
理论基础：Reflexive Tactics for Algebra, Revisited
参考实现：Algebra Tactics
实现细节的技术选择 ​
Variable ​
Universe ​
Proof Irrelevance ​

+    
     
   
 
\ No newline at end of file
diff --git a/draft/misc/setup.html b/draft/misc/setup.html
index cf13f39..1329068 100644
--- a/draft/misc/setup.html
+++ b/draft/misc/setup.html
@@ -3,8 +3,8 @@
   
     
     
-    常见的准备工作 | PKU BiCMR AI for Math
-    
+    常见的准备工作 | PKU BICMR AI for Math
+    
     
     
     
@@ -16,7 +16,7 @@
     
   
   
-    
PKU BiCMR AI for Math
Appearance
On this page
常见的准备工作 ​
请确保在知道每一条命令/每一个选项的意思都被完全理解后再进行这一步操作。
环境变量 ​
your_proxy_url 的形式为
http://127.0.0.1:7890
+    
PKU BICMR AI for Math
Appearance
On this page
常见的准备工作 ​
请确保在知道每一条命令/每一个选项的意思都被完全理解后再进行这一步操作。
环境变量 ​
your_proxy_url 的形式为
http://127.0.0.1:7890
 ^协议  |         |
        ^本地服务器地址
                  |
@@ -26,7 +26,7 @@
 which lean
Windows
PowerShell
where elan
 where lake
 where lean
其他参见 ​
代理 ​
如果成功让浏览器访问网页被代理，但是本地软件无法使用代理 ​
找到代理服务商所提供的「订阅」，使用一个能解析订阅的本地代理服务器软件，如 Clash Verge 或 Clash for Windows。请找到官方 GitHub 的 releases。
在启动软件后，找到对应的选项，查看自己的协议、地址、端口号。尽量使用 http 而不是 socks5。（如果你使用 https 作为协议（不出现在是变量名中的 https_proxy），请确保真的在使用 https 作为本地代理服务协议，大部分情况应该使用 http）
若无必要，不要开启本地代理服务器的 LAN。 在使用 WSL2 的某些版本时可能需要通过 cat /etc/resolv.conf 来获取代理服务器地址，此时需要开启本地代理服务器的 allow LAN/允许局域网连接选项。
如果成功让一些软件被代理，但无法使用 Elan/Lake/Lean 仍然无法使用代理 ​
配置对应的 proxy 环境变量。可以使用 curl 测试环境变量是否妥当。
关闭终端重新打开后/在别的程序中 代理失效？ ​
根据自己使用的 shell，搜索学习对应的 shell init scripts（bashrc、zshrc、$PSHOME\Profile.ps1、…）的相关资料。
应该使用什么 toolchain 版本？ ​
如果在使用 mathlib4 作为依赖创建项目 ​
如果在阅读（可能包含完成习题）现有的项目，如 Mathematics in Lean ​
  • 不要运行 lake update
使用 mathlib4 作为依赖创建项目 ​
在 macOS 上使用 Nix 安装的 Elan ​

-    
+    
     
   
 
\ No newline at end of file
diff --git a/hashmap.json b/hashmap.json
index 14e43a6..23d3408 100644
--- a/hashmap.json
+++ b/hashmap.json
@@ -1 +1 @@
-{"draft_fp_index.md":"ab54b40a","draft_fp_l0.md":"f4e926dd","draft_fp_l0_23-08-08.md":"a515a2a9","draft_misc_setup.md":"e399fb2a","about.md":"c6568d7a","research-projects_convex-optimization.md":"4d22f884","draft_impl.md":"a5f1a1dc","index.md":"abcc0f95","lean4-qa.md":"aef91948","research-projects.md":"9a1215f8","research-projects_number-theory.md":"38122f71","research-projects_spectral-sequence.md":"09816e54","team-exercises.md":"b0fe7d48"}
+{"draft_fp_l0.md":"f4e926dd","about.md":"c6568d7a","draft_fp_l0_23-08-08.md":"a515a2a9","index.md":"54d7a111","lean4-qa.md":"aef91948","research-projects.md":"9a1215f8","draft_fp_index.md":"ab54b40a","draft_misc_setup.md":"e399fb2a","research-projects_number-theory.md":"38122f71","research-projects_convex-optimization.md":"4d22f884","research-projects_spectral-sequence.md":"09816e54","draft_impl.md":"a5f1a1dc","team-exercises.md":"b0fe7d48"}
diff --git a/index.html b/index.html
index dc44ee2..e7ed60b 100644
--- a/index.html
+++ b/index.html
@@ -3,21 +3,21 @@
   
     
     
-    PKU BiCMR AI for Math | PKU BiCMR AI for Math
-    
+    PKU BICMR AI for Math | PKU BICMR AI for Math
+    
     
     
     
     
     
     
-    
+    
     
     
   
   
-    
PKU BiCMR AI for Math
Appearance
BiCMR AI for Mathematics
Formalization and Theorem Proving Seminar
北京大学北京国际数学研究中心「AI for Mathematics：数学形式化和定理证明」本科生暑期科研培训班
View Research Projects
View Team Exercises

-    
+    
PKU BICMR AI for Math
Appearance
BICMR AI for Mathematics
Formalization and Theorem Proving Seminar
北京大学北京国际数学研究中心「AI for Mathematics：数学形式化和定理证明」本科生暑期科研培训班
View Research Projects
View Team Exercises

+    
     
   
 
\ No newline at end of file
diff --git a/lean4-qa.html b/lean4-qa.html
index 55761e3..a3765d1 100644
--- a/lean4-qa.html
+++ b/lean4-qa.html
@@ -3,8 +3,8 @@
   
     
     
-    PKU BiCMR AI for Math | PKU BiCMR AI for Math
-    
+    PKU BICMR AI for Math | PKU BICMR AI for Math
+    
     
     
     
@@ -16,8 +16,8 @@
     
   
   
-    
-    
+    
+    
     
   
 
\ No newline at end of file
diff --git a/research-projects.html b/research-projects.html
index bda56b4..f7eeb6a 100644
--- a/research-projects.html
+++ b/research-projects.html
@@ -3,8 +3,8 @@
   
     
     
-    研究方向 | PKU BiCMR AI for Math
-    
+    研究方向 | PKU BICMR AI for Math
+    
     
     
     
@@ -16,8 +16,8 @@
     
   
   
-    
-    
+    
+    
     
   
 
\ No newline at end of file
diff --git a/research-projects/convex-optimization.html b/research-projects/convex-optimization.html
index f3d1203..d7509b9 100644
--- a/research-projects/convex-optimization.html
+++ b/research-projects/convex-optimization.html
@@ -3,8 +3,8 @@
   
     
     
-    PKU BiCMR AI for Math | PKU BiCMR AI for Math
-    
+    PKU BICMR AI for Math | PKU BICMR AI for Math
+    
     
     
     
@@ -16,8 +16,8 @@
     
   
   
-    
-    
+    
+    
     
   
 
\ No newline at end of file
diff --git a/research-projects/number-theory.html b/research-projects/number-theory.html
index 01cdfd4..9f925db 100644
--- a/research-projects/number-theory.html
+++ b/research-projects/number-theory.html
@@ -3,8 +3,8 @@
   
     
     
-    PKU BiCMR AI for Math | PKU BiCMR AI for Math
-    
+    PKU BICMR AI for Math | PKU BICMR AI for Math
+    
     
     
     
@@ -16,8 +16,8 @@
     
   
   
-    
-    
+    
+    
     
   
 
\ No newline at end of file
diff --git a/research-projects/spectral-sequence.html b/research-projects/spectral-sequence.html
index 527b0d4..e1549c0 100644
--- a/research-projects/spectral-sequence.html
+++ b/research-projects/spectral-sequence.html
@@ -3,8 +3,8 @@
   
     
     
-    PKU BiCMR AI for Math | PKU BiCMR AI for Math
-    
+    PKU BICMR AI for Math | PKU BICMR AI for Math
+    
     
     
     
@@ -16,8 +16,8 @@
     
   
   
-    
-    
+    
+    
     
   
 
\ No newline at end of file
diff --git a/team-exercises.html b/team-exercises.html
index 61bdcc0..7c1def4 100644
--- a/team-exercises.html
+++ b/team-exercises.html
@@ -3,8 +3,8 @@
   
     
     
-    AI4Math 练习项目说明 | PKU BiCMR AI for Math
-    
+    AI4Math 练习项目说明 | PKU BICMR AI for Math
+    
     
     
     
@@ -16,7 +16,7 @@
     
   
   
-    
PKU BiCMR AI for Math
Appearance
On this page
AI4Math 练习项目说明 ​
2023 年 7 月
项目要求 ​
  • 我们将按照基础数学方向和应用数学方向将全体同学分成项目小组，3-4 位同一方向的同学构成一组。
  • 根据小组成员的方向，请参考「选题样例」一节确定小组选题。你可以选择样例中的题目，也可以自选与之难度类似的其他题目。请使用 Lean4 完成所选择的定理叙述的形式化，并完成其证明。
  • 确认选题后，请每组派一位同学与助教沟通确认所选的题目，确认选题难度是否适中，并协调不同组之间的选题尽量互不重复。基础数学选题的小组请与姜杰东联系，应用数学选题的小组请与李晨毅或王子彧联系。
  • 项目将于 2023.07.25-2023.07.29 每天下午进行展示。请在展示前，将编译通过的 .lean 文件，提前发给助教。请在文件开头的注释中注明小组成员的构成。
  • 完成本项目时，你可以使用包括搜索引擎在内的任意电子工具。我们也推荐你在 Lean 社群上将你遇到的问题大胆提问，或与其他同学或助教讨论。但我们仍要求小组成员在获得必要的帮助后，独立地写下整个形式化证明。
  • 本项目的目的，在于训练大家查找 Mathlib 的能力，与有条理的形式化数学定理的能力。因此后文中所列出的题目，对于有该领域基础知识的同学相对简单。搜索引擎亦能很好地帮助你得到相关问题的正确数学证明。
  • 在完成项目的过程中，请注意以下诸点：
    1. 请首先查找并阅读 Mathlib 中与选题相关的内容，若小组选题在 Mathlib 上已经有较完善的基础，请尽量避免重复造轮子。
    2. 若小组选题在 Mathlib 上没有完善的基础，你可能需要自行写下相关定义，及前续定理。
    3. 对于需要自选具体形式化定理内容的小组，你所选的定理可以是教科书的课后习题、经典推论、或者其他定理，但请检索该命题是否在 Mathlib 中已经有相似命题，如果确有类似的，请更换命题。（请注意，有些看似简单的定理在 Lean 中的证明是较为困难的，请谨慎选择并与助教交流你想证明的题目）我们希望大家主要展示 Mathlib 定理与 tactics 的使用，不要求大家攻克难题。
  • 在进行项目展示时，请注意以下诸点：
    1. 若小组所研究的题目在 Mathlib 上已经有较完善的基础，请在展示时首先大致讲解课题相关定理在 Lean 中的实现与使用。
    2. 若小组选题在 Mathlib 上没有完善的基础，请在展示时首先讲解相关定义及前续定理在 Lean 中的实现及使用。
    3. 如果你所证明的定理不是大一大二基础课程所含内容，建议大家在展示时先讲解该定理使用自然数学语言的证明。
    4. 欢迎大家分享（吐槽）一部分使用 Lean 的经验，可以是选 Lean 实现过程中与实际的数学工作中不太一致的地方。如果可以的话，可以分享你认为对研究领域的后续知识形式化会遇到哪些难点。
    5. 课堂展示时请展示你的代码，语言为 Lean4，可以使用幻灯片辅助展示但并非必要，展示的主要目的是为其他同学讲清楚 Lean 在数学研究的不同分支上如何使用。
选题样例 ​
基础数学相关 ​
  • 以下列出数十个问题，它们被分为几个板块: 线性代数、抽象代数、 交换代数、数论、基础分析、点集拓扑、泛函. 每个板块大致有几个小题。你可以从中选择你喜欢的板块和问题或是选择其他难度相似的问题。带 ⋆\star 标记的问题相较于其他问题可能更具形式化方面的难度。
  • 你也可以选择其他数学分支的定理进行形式化，例如：组合恒等式。
  • 如果你认为完成一道题目过于简单，可以选择多道题目完成。
  • 如果你觉得某问题的叙述有误， 则你可以解释错误并按照你的想法更正，并形式化更正后的定理。
线性代数 ​
习题 1. 给定特征 00 的域上有限维线性空间 VV. 设 A,B:V→VA,B:V\to V 线性自同态, 证明
AB−BA≠idVAB-BA\ne\mathrm{id}_V 
习题 2. 线性空间 VV 的线性自同态 p:V→Vp:V\to V 满足 p2=pp^2=p, 证明 V=Ker⁡p⊕Im⁡pV=\operatorname{Ker}p\oplus\operatorname{Im}p
习题 3. 给定有限维线性空间 VV 的线性自同构 f:V→Vf:V\to V, 若 VV 的子空间 WW 是 ff-不变的子空间, 则它也是 f−1f^{-1}-不变的子空间.
习题 4 (⋆\star). 基域 R\mathbb R 上的 n×nn\times n 任意矩阵 AA, 证明
Rank⁡A=Rank⁡ATA\operatorname{Rank}A=\operatorname{Rank}A^\text TA 
习题 5 (⋆\star). 线性映射 f:Mn(k)→kf:M_n(k)\to k 满足 f(AB)=f(BA)f(AB)=f(BA), 证明 f=cTr⁡f=c\operatorname{Tr} 对某 c∈kc\in k
抽象代数 ​
习题 6. 对群 GG 的两个子群 H1,H2H_1,H_2 使 H1∪H2H_1\cup H_2 是子群, 证明 H1,H2H_1,H_2 具有互相包含关系
习题 7. 证明有限群到 C×\mathbb C^\times 的同态穿过 S1S^1
习题 8. 证明 pqpq 阶群不是单群, 其中 p,qp,q 是不相同的素数
习题 9. 证明 44 元群总是 Abel 群
习题 10. 证明二次扩张都是 Galois 扩张
习题 11 (⋆\star). 请写出 Abel 群映射正合的定义, 并从你写出的定义出发, 证明 Abel 群的四引理：设 Abel 群 A,B,C,D,A′,B′,C′,D′A,B,C,D,A',B',C',D' 有如下图表
A→B→C→D↓α↓β↓γ↓δA′→B′→C′→D′\begin{CD} A @>>> B @>>> C @>>> D \\ @VV\alpha V @VV\beta V @VV\gamma V @VV\delta V \\ A' @>>> B' @>>> C' @>>> D' \end{CD} 
PKU BICMR AI for Math
Appearance
On this page
AI4Math 练习项目说明 ​
2023 年 7 月
项目要求 ​
  • 我们将按照基础数学方向和应用数学方向将全体同学分成项目小组，3-4 位同一方向的同学构成一组。
  • 根据小组成员的方向，请参考「选题样例」一节确定小组选题。你可以选择样例中的题目，也可以自选与之难度类似的其他题目。请使用 Lean4 完成所选择的定理叙述的形式化，并完成其证明。
  • 确认选题后，请每组派一位同学与助教沟通确认所选的题目，确认选题难度是否适中，并协调不同组之间的选题尽量互不重复。基础数学选题的小组请与姜杰东联系，应用数学选题的小组请与李晨毅或王子彧联系。
  • 项目将于 2023.07.25-2023.07.29 每天下午进行展示。请在展示前，将编译通过的 .lean 文件，提前发给助教。请在文件开头的注释中注明小组成员的构成。
  • 完成本项目时，你可以使用包括搜索引擎在内的任意电子工具。我们也推荐你在 Lean 社群上将你遇到的问题大胆提问，或与其他同学或助教讨论。但我们仍要求小组成员在获得必要的帮助后，独立地写下整个形式化证明。
  • 本项目的目的，在于训练大家查找 Mathlib 的能力，与有条理的形式化数学定理的能力。因此后文中所列出的题目，对于有该领域基础知识的同学相对简单。搜索引擎亦能很好地帮助你得到相关问题的正确数学证明。
  • 在完成项目的过程中，请注意以下诸点：
    1. 请首先查找并阅读 Mathlib 中与选题相关的内容，若小组选题在 Mathlib 上已经有较完善的基础，请尽量避免重复造轮子。
    2. 若小组选题在 Mathlib 上没有完善的基础，你可能需要自行写下相关定义，及前续定理。
    3. 对于需要自选具体形式化定理内容的小组，你所选的定理可以是教科书的课后习题、经典推论、或者其他定理，但请检索该命题是否在 Mathlib 中已经有相似命题，如果确有类似的，请更换命题。（请注意，有些看似简单的定理在 Lean 中的证明是较为困难的，请谨慎选择并与助教交流你想证明的题目）我们希望大家主要展示 Mathlib 定理与 tactics 的使用，不要求大家攻克难题。
  • 在进行项目展示时，请注意以下诸点：
    1. 若小组所研究的题目在 Mathlib 上已经有较完善的基础，请在展示时首先大致讲解课题相关定理在 Lean 中的实现与使用。
    2. 若小组选题在 Mathlib 上没有完善的基础，请在展示时首先讲解相关定义及前续定理在 Lean 中的实现及使用。
    3. 如果你所证明的定理不是大一大二基础课程所含内容，建议大家在展示时先讲解该定理使用自然数学语言的证明。
    4. 欢迎大家分享（吐槽）一部分使用 Lean 的经验，可以是选 Lean 实现过程中与实际的数学工作中不太一致的地方。如果可以的话，可以分享你认为对研究领域的后续知识形式化会遇到哪些难点。
    5. 课堂展示时请展示你的代码，语言为 Lean4，可以使用幻灯片辅助展示但并非必要，展示的主要目的是为其他同学讲清楚 Lean 在数学研究的不同分支上如何使用。
选题样例 ​
基础数学相关 ​
  • 以下列出数十个问题，它们被分为几个板块: 线性代数、抽象代数、 交换代数、数论、基础分析、点集拓扑、泛函. 每个板块大致有几个小题。你可以从中选择你喜欢的板块和问题或是选择其他难度相似的问题。带 ⋆\star 标记的问题相较于其他问题可能更具形式化方面的难度。
  • 你也可以选择其他数学分支的定理进行形式化，例如：组合恒等式。
  • 如果你认为完成一道题目过于简单，可以选择多道题目完成。
  • 如果你觉得某问题的叙述有误， 则你可以解释错误并按照你的想法更正，并形式化更正后的定理。
线性代数 ​
习题 1. 给定特征 00 的域上有限维线性空间 VV. 设 A,B:V→VA,B:V\to V 线性自同态, 证明
AB−BA≠idVAB-BA\ne\mathrm{id}_V 
习题 2. 线性空间 VV 的线性自同态 p:V→Vp:V\to V 满足 p2=pp^2=p, 证明 V=Ker⁡p⊕Im⁡pV=\operatorname{Ker}p\oplus\operatorname{Im}p
习题 3. 给定有限维线性空间 VV 的线性自同构 f:V→Vf:V\to V, 若 VV 的子空间 WW 是 ff-不变的子空间, 则它也是 f−1f^{-1}-不变的子空间.
习题 4 (⋆\star). 基域 R\mathbb R 上的 n×nn\times n 任意矩阵 AA, 证明
Rank⁡A=Rank⁡ATA\operatorname{Rank}A=\operatorname{Rank}A^\text TA 
习题 5 (⋆\star). 线性映射 f:Mn(k)→kf:M_n(k)\to k 满足 f(AB)=f(BA)f(AB)=f(BA), 证明 f=cTr⁡f=c\operatorname{Tr} 对某 c∈kc\in k
抽象代数 ​
习题 6. 对群 GG 的两个子群 H1,H2H_1,H_2 使 H1∪H2H_1\cup H_2 是子群, 证明 H1,H2H_1,H_2 具有互相包含关系
习题 7. 证明有限群到 C×\mathbb C^\times 的同态穿过 S1S^1
习题 8. 证明 pqpq 阶群不是单群, 其中 p,qp,q 是不相同的素数
习题 9. 证明 44 元群总是 Abel 群
习题 10. 证明二次扩张都是 Galois 扩张
习题 11 (⋆\star). 请写出 Abel 群映射正合的定义, 并从你写出的定义出发, 证明 Abel 群的四引理：设 Abel 群 A,B,C,D,A′,B′,C′,D′A,B,C,D,A',B',C',D' 有如下图表
A→B→C→D↓α↓β↓γ↓δA′→B′→C′→D′\begin{CD} A @>>> B @>>> C @>>> D \\ @VV\alpha V @VV\beta V @VV\gamma V @VV\delta V \\ A' @>>> B' @>>> C' @>>> D' \end{CD} 

-    
+    
     
   
 
\ No newline at end of file