コンテンツにスキップ

Chapter 04: Mathlib を用いた証明の書き方

この章では，Mathlib を使って証明を書くときの基本的な読み方・書き方を整理します． 線形代数や微積分の各論は実践編で扱い，ここではそれらに共通する Mathlib の基本的な使い方を見ます．

Mathlib は，Lean の上で通常の数学を形式化するための大規模なライブラリです． 群・環・体・位相空間・測度・多様体などの定義，それらに関する定理，notation，型クラスインスタンス，証明を補助する tactic が含まれています． Lean 本体の小さなカーネルが証明の正しさを検査し，Mathlib はその上に数学の語彙と既存定理を積み上げている，と考えるとよいです． したがって，Mathlib を import しても「証明を信用で通す」わけではなく，最終的な証明項は Lean のカーネルで型検査されます． 前章では，証明とは証明項を構成することであり，tactic はその証明項を組み立てるための書き方だと見ました． この章では tactic そのものの基本説明は繰り返しすぎず，Mathlib の定義・定理・型クラスインスタンスをどう読み，既存の証明項としてどう使うかに重心を置きます．

この章では，まず Mathlib の定義や定理を読むための一般的な道具を確認し，次に Set，Finset，実数系の型，不等式という具体的な対象を見ます． 最後に，Mathlib で証明を書くときによく使う tactic や検索の考え方を整理します．

特に次の内容を扱います．

  • import Mathlib と名前空間・スコープつき notation
  • 型クラスで一般化された定理の読み方
  • bundled structure，morphism，subobject，coercion
  • Set，Finset，Real，NNReal，EReal，ENNReal
  • 不等式の型と証明パターン
  • Mathlib でよく使う tactic と検索支援
  • Mathlib の命名規則

なお，Set α，Finset α，Real，NNReal，EReal，ENNReal は「クラス」ではなく型です． ただし，それらの型には LinearOrder，TopologicalSpace，CompleteLinearOrder などの型クラスインスタンスが登録されており，そのインスタンスによって一般定理を適用したり，tactic が必要な構造を見つけたりできるようになります． Mathlib を読むときは，「対象そのものの型」と「その型に入っている構造」を分けて見ることが重要です．

参考:

import Mathlib

namespace Chapter04