Claude Code に、情報理論（通信やデータ圧縮の限界を扱う数学）の教科書を Lean で形式化させた。自分では証明を 1 行も書いていない。
自分のまったく知らない分野について、AIに証明させながら自分でも学んでみよう、というのが動機だ。
2026年5 月に始めて 8 月に一区切りをつけ、最終的に約 13 万行、定理は 4,000 本を超えた。
リポジトリ: https://github.com/FujiHaruka/information-theory
その過程で学んだことを標語的に書くならこうだ。
sorry は許せ、ごまかしは許すな。
ここでいうごまかしは、証明できていない部分を定理の仮定に移し、結果として証明が済んだように見える状態を指す。「sorry をゼロにして」とだけ指示したとき、AI は未証明の部分を仮定に移した。騙す意図があったわけではなく、指示に従っただけだ。その後、「証明できない箇所は理由を添えて sorry のまま残してよい。それがいちばん正直だ」と評価の優先順位を変えた。すると仮定に置かれていた部分が sorry として数えられるようになり、そこから順に証明されていった。
未完成を正直に報告する手段を用意し、それをごまかしより高く評価する。このプロジェクトでいちばん効果があったのはこの変更だった。
sorry 0 個は完成を意味するか
Lean では、書きかけの証明を sorry で飛ばせる。コンパイルは通るが、#print axioms を使えばその定理が sorry に依存していることが分かる。だから「sorry 0 個」を完成の判定に使える。最初はそう考えていた。
見落としていたのは仮定のほうだ。仮定に命題を置くと、その定理の中では証明しなくてよい。仮定を増やすほど証明は容易になる。しかし仮定に含まれる部分こそがその定理の証明でいちばんの難所だったりもする。
「sorry ゼロ」を目標にしたら、未証明の部分が仮定に移った
コードベースの規模が小さいうちは、sorry 0 個の定理は実際に証明が終わっていた。状況が変わったのは、サブエージェントごとにタスクを移譲し、並列に走らせるようになってからだ。コミットメッセージには「+6,356 行 0 sorry」のような報告が並んだ。
5 月 24 日に確認したところ、証明のいちばん難しい部分を仮定として受け取っている定理が 382 箇所あった。
例をひとつ挙げると、「雑音のある通信路で、1 回に送れる情報量の上限は、ある式 C になる」という、教科書の主定理の一つだ。AI が書いたものを日本語に直すと、こうなっていた。
定理: 送れる情報量の上限 = C 仮定1: どんな送り方をしても、送れる量は C 以下である 仮定2: ある送り方をすると、送れる量はちょうど C になる 証明: 仮定1 と 仮定2 を組み合わせる
どの送り方でも C 以下で、ちょうど C になる送り方が一つあれば、上限は C だ。結論は仮定から直ちに従う。教科書の証明で手間がかかるのは仮定1 と仮定2 を示す部分で、ここではそれがそのまま仮定になっている。それでも sorry は 1 つもないので、検査は通る。
docstring には「この仮定は後で外す」と書いてあり、当時の規約も、証明が進まないときは仮定に置いてよいと認めていた。コミットメッセージの「0 sorry」も文字どおり正しい。AI は指示どおり sorry を消し、規約どおり残りを仮定に置いただけだ。問題は評価基準のほうにあった。sorry を残せば「未完成」、仮定に置けば「許容」という扱いだったので、sorry を消せと言われれば仮定を使うのが自然な選択になる。
しかしこれでは、定理が本当に証明済みなのかどうかを機械的にチェックできない。一見すると証明済みの定理に見えてしまう。これはsorryを使うよりもタチが悪い。未証明の仮定をsorryに置いておけば進捗をトラッキングできる。
「sorry を残すのがいちばん正直」と順位を入れ替えた
翌日の 5 月 25 日、規約の順位を次のように変えた。
| 順位 | 状態 | 扱い |
|---|---|---|
| 1 | sorry 0 個で、別の AI の確認も通った | 完成 |
| 2 | sorry を残し、証明できない理由を分類したタグを付けた | 証明が進まないときに唯一認める状態 |
| 3 | 難しい部分を仮定として受け取った | 禁止。既存のものは 2 に書き換える |
sorry はコンパイラが検出するので、消さない限り未完成の記録として残る。仮定に置くと逆に、未完成なのに完成したように見える。だから sorry のほうを上に置いた。
これはsorry 駆動開発と呼ばれているものに似ている。未証明の部分をsorryにしておき、定理の主張自体は最初から正しいものにしておく。そうすれば、sorry部分さえ証明できればその定理と証明は正しいものと保証できる。
sorry は一度増えてから 0 個になった
書き換えを始めると、sorry の数は増えた。2 つの分野だけで、仮定に置かれていた 52 箇所が sorry に変わった。後退に見えるが、もともとあった未証明の部分が数えられるようになっただけだ。
仮定に置いていた定理は、6 月中旬までにすべて sorry に書き換えるか取り下げた。sorry はそこから順に証明されるか、命題自体が誤っていたと分かって書き直され、8 月の v1.0.0 で 0 個になった。
sorry に付けた理由が間違っていたこともある
sorryには理由を示すタグを付ける運用にしていた。sorry に付けるタグには、たとえば「Mathlib に必要な補題がないので、現時点では証明できない」という分類がある。正直な申告ではあるが、その理由が事実かどうかは別の問題だった。
ある証明で、AI は「必要な補題が Mathlib にないので、自作すると 150〜600 行かかる」と判断した。別に起動した確認役の AI も同じ判断をした。ところが、その補題は同じプロジェクトの別のファイルにすでにあった。それを使うと約 125 行で証明が完了した。二つの AI はどちらも Mathlib だけを検索しており、プロジェクト内を検索していなかった。
命題自体が誤っていたこともある。データ圧縮の定理で、比べている二つの量の一方はビット、もう一方はナット（自然対数を使う単位）で測っていて、そのせいで主張が偽になっていた。最初の確認では見落とされ、次のダブルチェックで見つかった。
そこで、新しいコミットのたびに、実装に関わっていないサブエージェントを独立に起動して検証させた。見るのは、証明すべき内容を仮定に置いていないか、タグに書いた理由は事実か、命題は正しいか（反例を 1 つ作ってみる）の 3 点だ。複数観点でのレビューエージェントを起動させるのはソフトウェア開発でもよくやると思うが、それだ。
Lean で完成と言える条件
Lean のカーネルが保証するのは、仮定から結論が正しく導かれていることまでで、仮定の中身が妥当かどうかは保証しない。#print axioms が報告するのも使った公理だけで、仮定は報告しない。だから Lean で定理が完成したと言えるのは、sorry が 0 個であることに加えて、仮定の中に証明すべき内容が含まれていないときに限られる。これは機械的には判定できない。
そのため「sorry 0 個」だけを目標にすると、証明すべき内容は機械が数えない仮定のほうに移る。このプロジェクトでは sorry を減らすべき数値として扱うのをやめ、未完成を記録するために残させるものとして扱った。
また、複数観点で独立にレビューエージェントを走らせることで、ごまかしがすり抜けにくい仕組みを作った。
少なくともREADMEに記載されている主定理に関しては、ちゃんと形式化できている、と思う。
