Lean4

发表于 更新于 阅读次数： Waline： 本文字数： 359 阅读时长 ≈ 1 分钟

Lean4：被称为交互式定理证明器（interactive theorem-proving system）的计算机系统（也称为证明助手或形式化系统）提供了另一种表达数学论证的方法。
mathlib(Lean mathematical library)是一项由社区推动的工作，旨在建立一个以lean proof assistant形式化的统一数学库。
a proof assistant：(一个软件，提供规范语言，依照规范语言定义对象和性质，证明定理，系统检查定理的正确性，直至逻辑基础)
Formalization: 我们将用一种规范的语言（如编程语言）来书写数学定义、定理和证明，让 Lean 能够理解。 作为回报，Lean 会提供反馈和信息，解释表达式并保证其格式正确，并最终认证我们证明的正确性。

Lean 是一个工具将复杂表达式转换成形式化语言(dependent type theory)

Syntax Model

sytax model
Lean’s parser produces a concrete syntax tree,of type Lean.Syntax(is an inductive type that represents all of Lean’s syntax,including commands,terms,tactics , and any custom extensions)all of those are basic building blocks: Atoms(fundamental terminals),Identifiers,Nodes(the parsing of nonterminals,contain a syntax kind), Missing Syntax(error mess)
Constructors of Lean.Syntax:missing,node,atom,ident

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
/-
Copyright (c) 2023 Eric Wieser. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Eric Wieser
-/
syntax (name := eqns) "eqns" ident* : attr

initialize eqnsAttribute : NameMapExtension (Array Name) ←
  registerNameMapAttribute {
    name  := `eqns
    descr := "Overrides the equation lemmas for a declation to the provided list"
    add   :=  fun
    | _, `(attr| eqns $[$names]*) => -- 这里面的第二个参数是模式匹配，捕获了eqns关键字后面的所有标识符
      pure <| names.map (fun n => n.getId)
    | _, _ => Lean.Elab.throwUnsupportedSyntax }

initialize Lean.Meta.registerGetEqnsFn (fun name => do
  pure (eqnsAttribute.find? (← getEnv) name))

本来是def M : ℕ → Matrix m n ℕ
def M : ℕ → Matrix (Fin 3) (Fin 3) ℕ – 类型不匹配的原因之一：没有指定矩阵的具体维数
| 0 => Matrix.of (fun i j => if (i = j) then 1 else 0)
| 1 => Matrix.of (fun i j => if (i = j) then 2 else 0)
| _ => Matrix.of (fun i j => 3)