How's it work

· Lean · ツール

Lean を対訳で読む：Taiyak を作りました

英語版 Reading Lean Side by Side: Introducing Taiyak
古い本の見開き。左の欄にラテン語の『De Amicitia』、右の欄にその英訳『Of Friendship』が段落ごとに並ぶ

Taiyak を作りました

Lean 4 のソースを宣言ごとに区切り、その隣に自然言語の数学として訳を並べるブラウザツール「Taiyak」を作りました。名前は「対訳（taiyaku）」から取っています。

GitHub の URL（プライベートリポジトリも可）、ZIP、フォルダのどれからでも開けます。ソースを読むだけで Lean は実行しないので、手元に Lean の環境は要りません。URL を指定せずに開くと、私が CRuby で試した形式化がデモとして表示されます。

Taiyak の画面。デモの Statements.lean を開き、左に Lean のコード、右に日本語訳を並べている。命題 P1 の ∀ をクリックすると「全称量化」の説明がポップアップで出る。
記号 ∀ をクリックすると用語の説明が出る

きっかけは CPython の形式化

David Andrews さんと Chao Zhang さんの「Formalizing CPython」を読んだのが始まりです。Claude Opus 5.5 を主に使って CPython 3.15.2 の関数を Lean に写し取り、関数ごとに次の4段階で確かめていく取り組みです。

  1. 写す: C や Python のソースを、エラーメッセージや端のケースまで保ったまま Lean で書き直す
  2. 試す: Lean の写しと本物の CPython を、関数ごとに5万件以上の生成入力で突き合わせる
  3. 証明する: 性質を述べて機械で検査する。偽なら反例を残す
  4. 見直す: 写しを書いていない別のエージェントが、壊れた実装でもこの証明を通れてしまわないかを問う

これまでに書かれた Lean は 613,318 行で、その過程で Python に対して 418 件のバグ報告が出ています。

面白そうなので中身を読もうとしたのですが、Lean に不慣れな私には定理の一つ一つがなかなか頭に入ってきません。その後、同じ手法を CRuby の range.c（範囲を正規化する rb_range_component_beg_len）で試す実験も始めました。Taiyak のデモはその実験の Lean ファイルです。

対訳で読めばいい

Lean を一から学ぶ前に、隣に数学の文章が並んでいれば読めるのではないか。語学の対訳本と同じ発想です。

Lean は対訳に向いていると考えました。普通のプログラムを日本語にすると「何をするか」の説明になり、書き手によって言い回しが揺れます。Lean の定理はそれ自体が命題で、定義は数学的な対象です。∀ x, P x は「任意の x について P x」としか訳しようがありません。訳の正解が数学としてほぼ一つに定まるので、訳と Lean を突き合わせれば誤訳も見つけやすくなります。

例として、デモの Spec.lean にある始点の正規化を示します。

def specBeg (i : Input) : Int :=
  let b := i.b.getD 0
  if b < 0 then b + i.n else b

Taiyak では、この隣に「定義: 正規化した始点 B」という見出しと、次の式が並びます（b₀ は始点で、nil なら 0）。式は KaTeX で表示します。

B={b0+n(b0<0)b0(b0≥0) B = \begin{cases} b_0 + n & (b_0 < 0) \\ b_0 & (b_0 \ge 0) \end{cases}

添えられるのは「負の値は末尾から数える」の一文だけです。Lean の3行と見比べれば、訳が合っているかどうかはすぐに分かります。

Lean の証明はなぜ信じられるのか

Lean の証明が信用されるのは、検査する部分が小さく、しかも別の実装で検査し直せるからです。

  • 命題は型、証明はその型をもつ項です。証明が正しいかどうかは、項が型に合うかという機械的な検査に帰着します。
  • 検査するのは小さなカーネルだけです。タクティクなどの自動化は証明項を組み立てるだけで、結果はカーネルが改めて検査します。タクティクにバグがあっても、誤った定理が通ることはありません（Lean リファレンス）。
  • カーネルは別実装で検査し直せます。公式の lean4checker、Lean で書かれた Lean4Lean、Rust で書かれた Nanoda などがあり、Lean 本体の実装を丸ごと信じる必要はありません（Lean FAQ）。
  • 証明が頼った公理は記録されます。#print axioms で標準の propext・Classical.choice・Quot.sound だけが出れば問題ありません。sorry は sorryAx として、native_decide はコンパイラ全体を信じる Lean.trustCompiler として現れるので、抜け道も隠れません（Validating a Lean Proof）。

ただし、これで保証されるのは「証明が正しい」ところまでです。定理の文が何を意味するかは別の問題で、これは後で話します。

なぜ Rocq ではなく Lean なのか（推測）

AI で定理証明に取り組む会社の多くは Lean を使っています。OpenAI も 2018 年の GamePad では Coq（現 Rocq）を使っていましたが、その後 Lean に移り（経緯のまとめ）、2026年に公開した openai/math も Lean 4 と Mathlib で形式化されています（データセットの説明）。理由は公表されていないので、以下は私の推測です。

  • Mathlib がある。 一つの巨大な数学ライブラリで、学習データとしても、問題を書く語彙としても効きます。CSLib の論文も、Mathlib が数学推論 AI の学習で大きな役割を果たしたと書いています（CSLib）。
  • 普通の数学がそのまま書ける。 Mathlib は排中律や背理法を気兼ねなく使う文化です。Paulson は、Rocq 界隈の構成的証明へのこだわりが数学への応用を妨げ、その場所を Lean が取ったと見ています（Why not just use Lean?）。
  • プログラミング言語でもある。 Lean の定義はコンパイルして実行できます。CPython の形式化の「試す」段は、Lean の写しを実際に走らせて CPython と比べることで成り立っています。
  • エージェントから扱いやすい。 elan と lake で環境が一つに揃い、導入で迷いません。
  • 合否がはっきりしている。 カーネルが通すか通さないかが、そのまま強化学習の報酬になります。

ただし Rocq が退いたわけではありません。Anthropic と Theorem 社は2026年10月、123 のライブラリについて RISC-V の機械語レベルでクラッシュしないことを Rocq で証明しました（報道）。数学や言語の意味づけは Lean、機械の意味論の蓄積がある検証は Rocq、という棲み分けなのかもしれません。

生成された Lean は人が読まなければならない

カーネルが保証するのは「この文はこの証明で示された」ところまでで、その文が意図どおりかは保証しません。Lean のリファレンスも、証明が正しいかと定理の文が何を意味するかを別の問いとして区別しています。さらに、誰もレビューしていない AI 生成の証明を、悪意ある証明と同じ慎重さで扱う対象に入れています（Validating a Lean Proof）。

よくある落とし穴は次の三つです。

  • 前提が満たせず、定理が空虚に真になっている
  • 定義の写し間違い。実装とずれた定義について、正しく証明している
  • 示したい性質より弱い命題を証明している

Formalizing CPython の「見直す」段は、まさにこれを確かめる工程です。私の CRuby の実験でも、命題と前提は AI に提案させ、私が確認してから証明に進めました。各定理の前提を満たす具体的な入力を NonVacuity.lean に置き、空虚でないことも示しています。

つまり、人が読むべきは証明ではなく定義と定理の文です。証明はカーネルの仕事、文は人の仕事です。Taiyak が長い証明を最初から畳んであるのも、まず文を読んでほしいからです。

そして Taiyak の訳も LLM の出力なので、間違うことがあります。訳で Lean を置き換えず、隣に並べて突き合わせられる形にしたのはそのためです。

使い方

  1. Web 版を開き、GitHub の URL を入れて「開く」を押す
  2. 「設定」で API キーを入れる（Anthropic、OpenAI、Google、OpenRouter のいずれか）。プライベートリポジトリなら GitHub トークンも入れる。設定画面のリンクから、読み取り専用・有効期限30日を入力済みの状態で GitHub のトークン作成ページが開きます
  3. 「このファイルを訳す」か、ブロックごとの「訳す」を押す

読むときの助けとして、次のものを用意しました。

  • Lean のコードをクリックするとヒントが出ます。 識別子なら定義の要約と、その定義へのジャンプ。∀ のような記号や omega、rcases のようなタクティクには短い説明が出ます
  • 「この箇所について Claude に聞く」で、宣言の文脈ごと質問できます
  • 訳すときは import をたどり、参照している定義も文脈として一緒に送ります
  • 訳はブラウザに保存されます。JSON に書き出してリポジトリの .taiyak/ にコミットすれば、誰でも API キーなしで訳つきで読めます
  • アドレスバーの URL がそのまま共有リンクになります。宣言の行番号を押すと、その宣言へのリンクをコピーできます

設計で気をつけたこと

送信先はヘッダで縛る

Taiyak は API キーと、ときにはプライベートなソースを扱います。「余計なところには送っていません」とコードで説明するより、ブラウザに強制させるほうが確かめやすいと考えました。

Web 版は Cloudflare Pages の _headers で Content-Security-Policy を返しています。connect-src に GitHub API と4つの LLM API だけを並べたので、ページがそれ以外に何かを送ろうとしてもブラウザが拒否します。

connect-src https://api.github.com https://api.anthropic.com https://api.openai.com https://generativelanguage.googleapis.com https://openrouter.ai

インラインスクリプトは sha256 で固定し、default-src 'none'、form-action 'none'、frame-ancestors 'none'、Referrer-Policy: no-referrer も付けています。ビルド結果もリポジトリにコミットし、ソースと一致するかを CI で確かめているので、配信されているものを GitHub 上でそのまま読めます。

パスワード欄を使わない伏せ字

API キーの入力欄を type="password" にすると、Chrome や Safari のパスワードマネージャが反応し、このサイトのログインパスワードとして保存しようとします。API キーはこのサイトにログインするためのものではないので、これは困ります。

そこで欄は普通のテキスト入力にして、CSS の -webkit-text-security: disc で伏せ字にしました。目のボタンで表示を切り替えられます。この CSS に対応しないブラウザでだけ type="password" に戻します。1Password や Bitwarden などにも、この欄を無視させる属性を付けています。キーはブラウザの中でだけ使い、「このブラウザに記憶」を選んだときだけ localStorage に保存します。

ただ、正直なところ迷っています。API キーこそパスワードマネージャで管理したいものです。ログイン用パスワードとしてではなく、トークンの保管庫として働いてくれるのが理想です。うまいやり方をご存じの方は教えてください。

UI の言語を訳の言語に合わせる

訳だけ韓国語で画面は日本語、というのは不格好です。そこで言語の選択を一つにまとめ、訳・画面・用語集・Claude の説明をすべてその言語にしました。画面の文言は10言語（日本語、英語、中国語の簡体字と繁体字、韓国語、フランス語、ドイツ語、スペイン語、ポルトガル語、ロシア語）を組み込み、それ以外は英語で表示します。画面の言語だけを固定する設定もあります。

アラビア語やヘブライ語のような右から左に書く言語は試していません。言語名を自由入力すれば訳は出せるはずですが、私には読めないので、表示が正しいか判断できないためです。試してくださる方がいれば歓迎です。

残念なところ

訳すには LLM の API キーが要ります。Claude Pro や ChatGPT Plus のような定額プランの枠は、今の Taiyak では使えません。普段使っている定額プランでそのまま訳せれば一番手軽なのですが、そうはなっていません。

回り道はいくつか用意しました。

  • dist/claude-artifact.html を claude.ai のアーティファクトとして公開すると、見る人自身の Claude アカウントで訳せます（API キー不要）。ただし claude.ai の中のページからは GitHub に届かないので、リポジトリを ZIP でダウンロードして読み込む必要があります
  • OpenRouter の無料モデルも選べます
  • Google の Gemini API には無料枠があります。ただ混んでいて、ブロック1つの訳が届くまでに3分ほどかかりました。Gemini 4 Argon は無料枠では使えません
  • 訳を .taiyak/ にコミットしておけば、読む人はキーなしで読めます

ChatGPT については、9月に Sign in with ChatGPT が出て、Plus や Pro の枠を API キーなしで外部のツールに持ち込めるようになりました。ただ対象は参加している提携先の製品で、開始時点で 16 個です（itbrief）。個人のサイトが自由に組み込める形は見つからなかったので、今後の候補として見ています。

Chrome に内蔵された Gemini Nano（Prompt API）にも対応させてみました。キーが要らず、コードが端末の外に出ないのは魅力です。ただ小さなモデルなので、Lean を数学に訳すには荷が重いようです。訳の質は API のモデルに及ばず、長い宣言は入力の上限に収まらないことがあります。

おわりに

AI が書く Lean はこれから急速に増えていくでしょう。証明はカーネルが検査してくれるので、人に残るのは「この文で本当にいいのか」を読む仕事です。Taiyak が、Lean に慣れていない人がその仕事に加わる入口になればうれしいです。

参考

100%