computo ergo sumEnglish

Lean の説明 — 入口

Lean は、数学の証明を機械に検査させる道具です。ここには、Lean とは何か・手元での使い方・小さな例での組み方・そして検査が通っても言いたいことが言えているかを確かめる手順を、14 ページに分けて置いています。

関連：自然哲学（記事の一覧）／Lean 検証一式（検査済みの定理の台帳と、ソースの配布）

01

ページの一覧

この説明の全体

入口（このページ）

  1. Lean とは何か — 命題が型に、証明が項になる。kernel と tactic、公理、そして Lean が保証しないもの
  2. 使い方の入口 — 手元に入れて、一つのファイルを検査するまで。エラーの読み方と補題の探し方
  3. 有限の判定を decide に載せる — 「数えれば分かる」ことを kernel の計算に変える
  4. 数え上げを Finset で書く — 有限集合の要素数を、証明できる形で数える
  5. 単射一本で上界を出す — 紙で二行の議論が Lean でも二行で済む場合
  6. 級数と不等式 — 無限和の評価を、係数の正負と収束の道具で閉じる
  7. 証明書を Lean に検査させる — 探索は外で行い、見つかった答えだけを機械に確かめさせる形
  8. 通っても、言いたいことが言えているか — 定義の強弱・定理名が言っている範囲・仮定の一覧
  9. 言明を読む手順 — 他人の証明を受け取った側が、何をどの順で確かめるか
  10. Lean では現実的に厳しいもの — 計算量・在庫の無い理論・型の付かない完全性。紙に残すと決める基準
  11. よくある罠 — 止まる場所と、そのときに打つ手
  12. 用語集 — この説明に出てくる語を 43 語、各 1〜3 行で
  13. Lean の仕組み — 機械検査という考えの来歴、Lean 自身の組み立て、そして検査のあいだに何が起きているか
02

読む順

Lean を初めて見る

01 → 02 → 03 の順に読み、03 の例を手元で一度検査してみてください。そのあとは 04〜07 を興味の順に。用語で詰まったら 12 に戻ります。

01 のあとに 13 の後半（検証の仕組み）を読むと、検査のあいだに何が起きているかを実物で追えます。01 も 13 も、手元に何も入れなくても読めます。

「Lean が通った」という結果を、どう読めばよいか知りたい

08 → 09 → 01 の最後の節。この三つで足ります。機械検査が何を保証して何を保証しないかは 01 の末尾に、保証の外にあるものが具体的にどこに出るかは 08 に、受け取った側の手順は 09 にあります。

実際の検査結果そのものは Lean 検証一式 にあります。定理名・依拠する公理・ソースの配布はそちらです。

Lean で書くかどうか迷っている問題がある

10 → 11。10 は「書かないと決めた理由」を三種類（計算量・在庫・完全性）に分けています。11 は書き始めてから止まる場所の一覧です。

03

札の凡例

このサイトの記事は、主張ごとに四つの札のどれかを付けています。Lean の話が関わるのは一つ目です。

Lean機械検査済み。Lean 4 と mathlib で検査が通り、依拠する公理が標準の三つ以下で、sorry による穴も native_decide も無いもの。定理名を添えます

紙証明はあるが、機械検査は済んでいないもの

計算手元の計算で確かめた範囲。外に出す主張にはしません

既知言い換え・既知の定理・外の文献の確認

この四つの区別が要る理由は 01 の末尾にあります。Leanの札は「この言明が公理から導ける」ことだけを言い、「この言明が言いたかったことである」ことは言いません。

改訂 2026-09-20：初版。14 ページの枠と読む順を置いた。