数学は幽霊がいる

• Leanは数学を形式化できるよう設計されたプログラミング言語で、数学者が数学の定理をコードのように扱えるようにする
• 利用者は定理、証明、公理などをコードの形で作成し、証明過程は tactic と呼ばれる命令セットを通じて進められる
• 証明が実際に完成していなくても sorry で一時的に差し止めることができるが、これはTypeScriptのanyに似た偽証明である
• 公理を誤って追加すると（例: 2 = 3）、論理的矛盾とすべての命題の証明可能性という危険が生じる
• Leanは論理的に選択した公理と証明体系の上でのみ結論を導くため、数学的妥当性を維持することが重要な意味を持つ

---

Lean: 数学をコードで扱う言語

• Leanは、形式化された数学を記述するために特化したプログラミング言語である
• 数学者はLeanを通じて数学をコードとして表現し、互いの定理と証明を構造化することで協働と共有を可能にする
• 未来的には、人類の膨大な数学知識がコードの形で機械的に検証・組み合わせ可能になる未来を提示している

Lean証明の第一歩

• theorem two_eq_two : 2 = 2 := by sorry の形式で、Leanでは簡単な定理宣言が可能
• 証明が未完成のときは sorry を入れるが、これは一時しのぎにすぎず実際の証明ではない
  • sorry はLeanの証明検証を通過させるが、論理的には信頼できない
• 完全な証明を行うには、rfl（reflexivity）などの tactic を使って、2 = 2 のような自明な等式を証明する
• 既に証明済みの内容は、exact などを使って他の定理で再利用できるため、モジュール性を重視できる

公理と矛盾：数学が“幽霊”に取り憑かれたとき

• もし axiom math_is_haunted : 2 = 3 のような公理を追加すると、Leanはそれを真実として扱う
• この公理は後の証明過程で利用可能となり、数学的に成立しない結論（例: 2 + 2 = 6）までも証明可能になる
• rewrite tacticを使って 2 を 3 に置換し、rfl で等式証明手続きを完了することができる
• 不適切な公理によって矛盾が導入されると、Leanでもすべての命題が証明可能な状態（論理的崩壊）が発生する
• 実際、20世紀初頭にはラッセルのパラドックスなど、公理系内の矛盾が数学の根本的な考察へとつながった
• このように、公理の選択が論理体系の妥当性維持に決定的であることを、Leanはよく示している

証明検証器（proof checker）としてのLean

• 公理が適切に選ばれ、Leanが論理的に正しければ、理論的に信頼できる結論を提示する
• 単純な等式から非常に複雑な定理（例: Fermatの最終定理）まで同じ原理で検証される
• 大規模な定理は、下位構造と定理の反復的な証明積み上げによって全体のツリーが完成する構造である
• 例として、Fermat's Last Theorem（フェルマーの最終定理）をLeanで形式化する大規模プロジェクトが進行中で、最終的には暫定証明（sorry）なしの正式な証明体系が完成する予定だ

Leanを学ぶ楽しさ

• Leanによる証明はコーディングと数学の創造的な融合である
• 始めは簡単な命題を証明する方法から、次第に複雑で深い数学を厳密に積み上げる過程が重要な楽しみとなる
• 公式チュートリアルやコミュニティ資料（例: Natural Numbers Game、Mathematics in Lean など）が、入門に適している
• Leanを使うと、直接ロジックを形式化しながら、巧妙なアイデアと議論の美しさを再発見できる
• 根拠がない場合でも、ある種の人々にとってはLeanが特別な楽しさをもたらすという結論で締めくくられている

[GN⁺]

Hacker News の意見

• 最近、Leanのようなシステム（あるいはLeanそのもの）を使ってニュースやノンフィクション記事を書き直すアイデアを考えている。各記述を証明すべき定理とみなし、その証明には引用も含めるという形だ。たとえば「私が承認した3つの情報源が事実だと主張したら、これは事実である」のような合成的な証明として扱うこともできる。そして「証明済み」の主張をハイライトして見られるように、文書全体をマークアップできるのではないかと思う。完璧ではないが、最近のメディアが担っていた厳密さを、もう一度技術で実現してみる試みだ
  • 自然言語の記述を形式化するのは、無数の困難がある領域だ。現実世界と相互作用するコードを書くのが難しいのと似た理由による。私たちが当然視している概念（同一性、時間、因果関係など）をすべて形式の中で細かく扱わなければ、事実同士を結びつけたり表現したりできない。とはいえ、この問題は本当に興味深い。OpenCogはこの分野を徹底的に追求したプロジェクトだったし、知識表現と推論（KRR）という研究分野も学界に存在する。IJCAIのジャーナルも関連研究であふれている。そして哲学者たちは時間・様相・確率などさまざまな議論を形式化しようとして多くの論理を書いてきたが、残念ながらそれらは互いに簡単には結合できない（最近解決されていなければの話だが）
  • ニュースに対して私たちが持つべき最も重要な信念は、多くの場合、絶対的な記述の集合として証明できるものではないと思う。ベイズ確率のように推論の連鎖を計算するツールのほうが適している。こうした数値的推定のためのツールは見たことがある
  • 大学で数学を学んでから、ノンフィクションの文章力が大きく向上した経験がある。SO（恋人）や妹が書いたエッセイを読んで、まるで論理的証明を見るように、「ここではCがBから出ると言っているが、BがAから出る理由が実は欠けている。ならCがAから出るとは言えない」といった具合に厳密さを適用していた。LLMのような道具でこれをプログラム化できそうではあるが、ハルシネーション（実際にはない主張の生成）があるので限界は明確だ
  • 注意が必要だ。こうしたアプローチは、論理的客観性のオーラを、本質的にはどれほど急進的だったり無意味だったりする主張にも容易に与えてしまうおそれがある。近代論理学の父の一人であるGottlob Fregeの政治観を見ると、警告になるかもしれない 関連リンク
  • 特定のテーマに関する議論全体の構造を、地図のように描く方法のほうが面白そうだ。たとえば「神は存在するか？」のような大きな問いから始めて、賛否の論拠、その反論、さらに再反論まで、すべてを階層的に展開して見るのである。各主張には「プラトンがこのような議論をした」といった形で引用を入れるが、それは根拠というより歴史的文脈を与えるためのものだ。勝敗を決めるのではなく、同じ論点の堂々巡りを避けるために議論の地図を作ることが核心だ
• 私たちは最終的に、自明な真理をいくつか出発点にした証明辞書を作り、その上に各種の証明が論理的に積み上がる構造を作っている、ということなのだろうか。そうだとすれば、追加の証明は既存の証明の論理的な組み合わせにすぎない。これをZachtronics風のゲームにしてほしい！ Euclideaというゲームは幾何学の分野でそんな感覚を与えてくれるが、こうして論理の塔を積み上げていくコンセプトはとても魅力的だ。純粋数学とはまさにこういうものなのか、純粋数学の教授たちはこの論理辞書を拡張することに喜びを感じるのか気になる。そして、有名な数学者が基本となる証明のリストを作った記憶があるのだが、それが誰（あるいは何）で、何と呼ばれているのか教えてほしい。たぶんそれは公理（axioms）のことだろう
  • すでに関連するゲームはあるが、完全に望みどおりではないかもしれない（そして数学全体を作るゲームでもない）。実際に遊んだことがあるが、かなり面白かった。この記事で言及されている leanprover-community/nng4 がその例だ
  • 「これをZachtronics風ゲームにしてほしい」への返答としては、数学こそがそのゲームだと言える（半分冗談だが）。ゲーム版も本当に面白いと思う。純粋数学はまさにそういう体系だ。学部レベルではそういう感覚で合っているが、論文研究になると少し違う。ゲームっぽさを求めるなら、Dummit and Footeのような抽象代数の教科書を見てみるのもおすすめだ。証明にはゲーム的な楽しさがある。有名な本なら、詰まったときはオンラインに解説もある
  • ユークリッドの公理（axioms）のことを言っているのかもしれない。点、線、平面、平行線のような概念が定義された体系だ。平面ではなく球面上では、この体系は成り立たない。あるいはZermelo-Fraenkel集合論（ZF/ZFC）のことかもしれないが、現代数学はすべてその上に構築されている
  • Bombeというゲームもある。マインスイーパーの派生で、直接セルを開ける代わりに、「どういうときにフラグを置けるか」というルールを作りながら遊ぶゲームだ。レベルが上がるほど、ルールが補題のように連鎖していく。プレイヤーの熟練度が上がると、ツールセットの制約を外して一般化もできるようになる ゲームリンク
  • 数学は本質的に、公理から出発して結論を導く過程だ。もちろんそれがすべてではないだろうが、私の理解ではそうだ
• ちょっと揚げ足取り気味ではあるが、two_eq_two定理が関数のように見えると言うのは変だ。引数がないのだから、むしろ定数に近い（もちろん定数も引数なし関数だとはわかっている）。むしろ下のようにx_eq_xを使って、2_eq_2で関数のように適用する形のほうが説得力があると思う

  theorem x_eq_x (x:nat) : x = x := by
    rfl
  
  theorem 2_eq_2 : 2 = 2 := by
    exact (x_eq_x 2)
  

  ここではx_eq_xは関数のように見え、2_eq_2で実際にそのように使われている
  • その指摘はもっともだ！ 私がそうしなかったのは、Leanの引数処理（特にdependent typesのような概念――xを与えるとx = xの証明を返す）が自分にはやや馴染みがなく、別途扱うべきテーマだったからだ。次の記事で扱う予定だ
• Leanを学んでいて感じた難しさは、tactics（rflのようなもの）が過度に包括的で、チュートリアルでも正確な意味を把握しにくい点だ。たとえばC言語ならビット単位まで状態変化を追えるが、Leanは何となく不明瞭だ。そしてrewrite（rw）タクティクの文法も自然ではないように感じる
  • Coq（現在のRocq）でも、tacticsへの順応はいつも難しかった。たとえば「A = B」と「P(A,A)」があるときに「P(A,B)」へ移したいのに、説明しづらい理由でrewriteが効かなかった経験がある（中間構造の定義の問題だった気がする）。一方、Metamathとset.mmデータベースは、そもそもtacticなしで具体的な推論だけを使って証明させる（ax-mpのような推論規則だけを使う）。ただ、これはこれで役に立つユーティリティ補題を全部覚えなければならず、簡単ではない
  • それがAgdaをより好む理由の一つだ。Agdaには実質的にtacticがほとんどなく、Curry-Howard correspondenceを使って関数型プログラミング言語として証明termを直接書く。その代わり、抽象化や関数作りを怠ると、些細なことでも途方もなく面倒になるので規律が重要だ
  • 少なくともLeanでは、tacticsの定義に「定義へ移動（go to definition）」して内部動作を見られるという点がある。学ぶ段階では量が多くて圧倒されるが、最終的には全部見ることができる（基礎型理論まで行くと直感がつかみにくいが）。それとrewriteの文法が自然でないと言っていたが、では自然なrewrite構文とはどんなものなのか気になる
  • 興味深かったのは、tacticsがすべて「ユーザーレベル」のコードで、証明の中核（kernel）の外にあるという事実だ。小さく検証済みのカーネルを変えずに保ちたいのだから理にかなっている。しかしこれは、tacticsがバージョンアップや修正で変わると既存の証明が壊れる可能性があるということでもある。実際のところ、それがどれほど問題になるのか気になる
  • 私の予想に反して、Leanではreflectionやrewriteのほうがadditionより根本的なのだと思っていた。Leanはadditionは最初から備えているのに、rflやrewriteは毎回明示しなければならないように見える。Leanにはおそらくpreludeのようなものがあって、それを自動でやってくれる版もあるのかもしれない
• Leanでproofを対話なしのnoninteractiveな形で読む方法があるのか気になる。natural number gameをやっていると、proofが「rw [x]」という命令の羅列にしか見えず、とても読みづらかった。エディタで各行の状態は見られるが、そのたびにクリックしなければならず流れが切れてしまう。Pythonでも、インデントがなくブロック構造だけを見てクリックしないと流れがわからないなら同じことだろう。私の感覚はゲーム序盤で使える命令が限られているせいかもしれないが、実際のフル機能のLean環境ではこの流れがもっとましなのか気になる

  • Leanで証明をnoninteractiveに読む方法はある？
    私も最近気になって調べてみた。lean-in-latexブログ が、クリックなしでエディタ外からその流れを追える方法を提供しているし、Leanコミュニティがこれにどう取り組んでいるかも見られる

  • Rocqには以前「数学的証明言語」というものがあった。実際の使用例は見つけにくいが、こんな感じだ

    Lemma foo:
      forall b: bool, b = true -> (if b then 0 else 1) = 0.
    proof.
      let b : bool.
      per cases on b.
        suppose it is true. thus thesis.
        suppose it is false. thus thesis.
      end cases.
    end proof.
    Qed.
    

    こうしたアプローチは、論文における「手書きの証明」のように読めるようにしていた。ただ、ほとんど使われず消えていった。IsabelleのIsar proof言語も似ていて、むしろ標準的な方式に近い。例:

    lemma "map f xs = map f ys ==> length xs = length ys"
    proof (induct ys arbitrary: xs)
      case Nil thus ?case by simp
    next
      case (Cons y ys) note Asm = Cons
      show ?case
      proof (cases xs)
        case Nil
        hence False using Asm(2) by simp
        thus ?thesis ..
      next
        case (Cons x xs’)
        with Asm(2) have "map f xs’ = map f ys" by simp
        from Asm(1)[OF this] ‘xs = x#xs’‘ show ?thesis by simp
      qed
    qed
    

    全体の論理構造と中間結果を明確に書いておき、細部が重要な箇所でだけ「by ...」でtacticを短く書ける。Leanにもこういうものがあるかはわからないが、少なくとも検索キーワードやLeanフォーラムで質問するときの題材にはなると思う
  • とても良い質問だ！ まだ初心者なので全面的に信頼してほしいとは言えないが、自分の感覚を共有する。Leanを2か月ほど使ってみた結果、証明コードを読むことはプログラミングコードを読むのとは違い、「スキャンする」感覚に近い。議論全体の構造、どのtacticを使っているか、どのlemmaを使っているかに注目する。実際のLeanコードのスタイルでは、新しいgoalごとにインデントし、goalが終わるとまた戻す。だから議論の形（「shape」）が重要になる。私のPRの例 を見てほしい。tacticに慣れると、「intro」があれば量化子の中に入ること、「constructor」はgoalの分割だといったことがわかるようになる。結局のところ、tacticsは証明木（term tree）を作るためのマクロ／DSLなのだ。私は証明コードを見るとき、木の操作（分割する、順番に埋める、など）のように感じる。それでも、証明コード中のassertionを正確に知るにはクリックが必要な点は残る。良いアイデアに基づく証明は、論文の論理展開のように明快に読める。だから意図を伝えたい人は、読みやすい名前、明確な展開、小さなlemmaの切り出し、仮定を先に書いて短い証明コードで片づける、といった書き方をする。一方で、機械的には面倒だが数学者には明らかな部分は「golfing」（最短コード化）で済ませることもある。ゴルフ風のスタイルは、しばしばコードを短くする代わりに、人間が直感的にわかる部分だけを扱う。要するに、Leanで読む構造は暗黙的だが、もっと明示的にする方法もあり、tacticに習熟するほどクリックなしでも構造を把握しやすくなる。lemma名をざっと追うだけでも大まかな流れはつかめるし、順序も再構成しやすい
• 内容が本当に良かった。こういうことを消化しやすい形で説明できる人はめったにいないと思う。専門家が当然とみなして飛ばしがちな細かな段階を、全部見せてくれるのが秘訣だ
  • ありがとう！
• このスレッドで、Leanとidris/coq/agdaの将来についての意見を聞けないだろうか。知識表現を勉強したいのだが、何か一つに深く入る前にコミュニティの規模や将来的なリスクが気になっている。以前、clojure core.logicに時間を投資して、関心の低さやコミュニティの小ささで痛い目を見たので、なかなか踏み出せない
  • 実体験では、LeanとCoq/RocqはIdrisやAgdaよりずっと広く使われており、ライブラリやコミュニティも大きいと感じる。Rocqは主にプログラム検証でよく使われているが、それは歴史が長いからだと思うし、独特な点も多いので、Leanが近いうちに追いつくかもしれない。Leanは数学の定理証明で最も一般的に使われている。Rocqの有名プロジェクトにはCompCert、CertiCoq、sel4があり、実際に航空機ソフトウェアの検証に使われている例もある（まとまった プロジェクト一覧 を参照）。Leanにはmathlib（数学証明の集積）、フェルマーの最終定理（FLT証明プロジェクト）、PFR などの大規模プロジェクトがある。IdrisやAgdaには、実際の「現実世界」のプロジェクトはないと認識しているが、間違っているかもしれない。もっとも、どれもC++やJavaScriptのような言語・コミュニティに比べれば規模は非常に小さい。そして実際、プログラム検証は非常に遅く退屈な作業だ。AIの発展などによる根本的な変化はいずれ来る気もするが、それでも身につけた技能は十分役に立つだろう
  • この分野に賭けるという発想自体、あまりしないほうがいいと思う。実際、大半の数学者はformalization（形式化）にあまり関心がない。手書きの証明と、コンピュータが要求する厳密な構文との隔たりが大きいからだ。単に学んで実践する面白さとして向き合うべきで、将来性という点ではLeanが最近もっとも活発ではあるが、それぞれ長く使っている層があるので、断定は難しい
• 特別なテクニックや裏技なしに、ただLeanにランダムなものを投げ込んで、それが通るかどうかで面白い発見ができるのか気になる。あるいは、こういうことを自動化システムやllmで回して、難解な証明や理論を片っ端から試して成功するか見ることは可能なのか？ 変な質問かもしれないが、プロローグもやっと理解できる程度だ
  • 私はcertfied programmingを仕事にしている立場だが、生成AIと形式手法は最高の組み合わせだと思う。今後プログラマがLLMに置き換えられるかどうかも、AIがcertified programmingと組合せ論的推論をどれだけうまく扱えるかにかかっていると思う

    ランダムに投げたら面白い発見はあるのか？
    既存のAIは、チェッカーのように場合の数が少ない問題ではよく機能する。チェスは少し難しく、囲碁は機械学習なしの非伝統的AIでは不可能なほどだ。形式言語は、場合の数や探索可能な状態数が想像を絶するほど多い。問題の性質が明確なら、SMT solverで総当たりできる。もともとSMT solverとproof assistantは別々の形式手法分野だったが、今では互いを補完する時代になっている（Sledgehammer、Lean-SMT参照）
    llmや自動化システムに任意の証明・理論を試させるとしたら？
    この方向はまだ主流研究ではないが、多くの研究が試みられている。LLMブーム以前から何年も大きな資金提供があり、「Learning to Find Proofs and Theorems by Learning to Refine Search Strategies」のような過去の試みや、DeepSeek-Proverのような最近の研究もある。どう学習させるべきか、将来性がどこまであるかはまだ完全に開かれている。
    現実のLLMはRocqやLeanの言語ではまだ不十分で、しかも誤答が出たときに直すのが非常につらい。それでも、時間がたてばAIツールの水準は大きく上がるだろうと期待している

  • これは本当に活発な研究・実験分野だ！
    Leanコミュニティの多くはZulipに集まっていて、Machine-Learning-for-Theorem-Provingチャンネル でさまざまな参考スレッドを確認できる
• alphaproofを見てLeanに初めて興味を持った立場からすると、入門記事としてとても良かった。よければ、Leanで何をしているのか紹介してもらえないだろうか？
  • 今のところは、Leanで数学を勉強しているだけだ。具体的には TaoのLean教材 に沿って、練習問題の空欄になっている sorry を自分で埋める形で学んでいる（私の解答は ここ にある）
• Leanには、信頼できない証明（"sorry" を使ったproof）や追加公理（axiom）の増殖を自動で防ぐ検証モードのようなものがあるのだろうか。たとえば「proofがいかなる形でもsorryを使っていない」「固定された公理集合の証明力に依存している」を確認できるのか？
  • 記事の後半で触れられていた #print axioms some_theorem が、その例になるのではないかと思う。これで、その証明が直接または間接的に sorry や未検証の公理に依存しているかどうかわかる
  • print axioms で追加された公理がないか確認できるし、warningやerrorなしでコンパイルされるかを見ることもできる。SafeVerifyユーティリティは、RLシステムが見つけた一部のトリックも検出してくれる
  • マクロでも可能だという話が ここ にある