The Nomura Institute of Glycosciece Blog

話題の証明支援システム　LEANについての本やサイトの紹介です。
望月先生のABC予想の証明の正しさをチェックするプロジェクトが使っているLEANについての本が評判になっています。The Proof in the Codeという本です。
https://www.quantabooks.org/books/the-proof-in-the-code/

もともとLEANはMicrosoftのLeo de Mouraによって開発されたプログラムです。Microsoft WordやWindowsなどのプログラムのコードにバグがないか、セキュリティ脆弱性がないか、そして設計どおりに動作するかをチェックするプログラムとして開発されました。LEANはあまり使われていなかったようですが、数学者がこれが数学の証明のチェックに使えるのに気付き、現在の証明支援システムに育て上げたのだそうです。ものすごく面白い本のようで多くの人の賛辞が上のサイトにのっています。

このLEANの公式サイトはこちらです。https://lean-lang.org/

無料のエディタであるVS Codeの機能拡張としてインストールしてセットアップして使うようです。
日本語で参考になるサイトがありました。
https://aconite-ac.github.io/
こちらはLEAN関連の、日本語の情報を中心にまとめてくださっているサイトです。ご自身の哲学探究サイト『束跡』をホストしているサイトでもあるのでとても興味のもてる内容のようです。LEAN関係の部分を以下に引用しておきます。

・Theorem Proving in Lean 4 日本語訳 : Leanのチュートリアルドキュメント「Theorem Proving in Lean 4」の非公式日本語訳です。
・Leanのインストール方法・elanとLakeの使い方 : Leanのインストール方法・elanとLakeの使い方をまとめた非公式資料です。

外部リンク
日本語情報

LEAN JA : Lean言語の日本語コミュニティです。豊富なリンク集が掲載されています。Discordサーバーもあります。
Lean by Example : LEAN JA管理者の北窓氏による、Lean言語とその主要なライブラリの使い方を豊富なコード例とともに解説した日本語資料です。

英語情報もまとまっているので役立ちます。是非参考になさってください。

今日のKindleの日替わりセールに広中平祐さんの「学問の発見」
があって499円で売っていたので購入しました。これはブルーバックス版で2018年の広中先生の序文が新しく付け加わっています。ちょうどAIの勃興する前にでたブルーバックス版です。この本の文庫版は昔読んで持っていたのですが蔵書整理で捨てました。今Kindle版であらためて読んでみると、AI時代の今だからこそ、読んでおきたい本だと思います。今日中は499円で購入できるのでよかったら買ってみてください。他に面白い話満載ですが、岡潔先生の神がかりてきな講演会の話や岡先生が、フィールズ賞を受賞することになった研究テーマの解決につながる示唆を与えてくれた話などもあります。

あと、国立国会図書館デジタルコレクションで読める広中先生の本をいくつかあげておきます。番号は前に紹介した時のものです。他の本も紹介したのですが、例の4・22事変で館内限定化されて読めなくなっています。今読める本をいくつか追加していますので読んでみてください。

368) 江崎玲於奈, 広中平祐 著『日本を語る』,毎日新聞社,1977.3. 国立国会図書館デジタルコレクション https://dl.ndl.go.jp/pid/12589479 (参照 2025-07-25)

82) 同じくフィールズ賞受賞者の広中平祐さんの発想法についての本です。
広中平祐 著『「可変思考」で創造しよう : 頭にカツを入れる超発想法』,光文社,1987.3. 国立国会図書館デジタルコレクション https://dl.ndl.go.jp/pid/12675364

536) 広中平祐 著『湧源国家論 : 豊かさの後に何を創造するのか』,PHP研究所,1988.2. 国立国会図書館デジタルコレクション https://dl.ndl.go.jp/pid/13067283 (参照 2026-08-06)

537) 広中平祐 著『雲の如く』,旺文社,1986.1. 国立国会図書館デジタルコレクション https://dl.ndl.go.jp/pid/12256638 (参照 2026-08-06) 広中先生のお母さんについての本です。

538) 広中平祐 著『広中平祐の数学教室 : 誰でも数学が好きになれる』上,サンケイ出版,1985.10. 国立国会図書館デジタルコレクション https://dl.ndl.go.jp/pid/12608171 (参照 2026-08-06)

539) 広中平祐 著『広中平祐の数学教室 : 誰でも数学が好きになれる』下,サンケイ出版,1985.11. 国立国会図書館デジタルコレクション https://dl.ndl.go.jp/pid/12608169 (参照 2026-08-06)

東大の先生たちが、高校生向けに研究を紹介してくれるオープンキャンパスの講演会の動画が今年も公開されはじめました。いくつか紹介します。

東京大学理学部オープンキャンパス2026 オンデマンド講演会「宇宙と重力の謎に挑む-理論物理学の最前線-」高橋 卓弥 特任研究員
https://youtu.be/gzt6_n0ITzI

東京大学理学部オープンキャンパス2026 オンデマンド講演会「時空を聴く、宇宙を知るー重力波でたどる宇宙論ー」度會 大貴 特任研究員
https://youtu.be/fq1p8FToSNs

あと、今日と明日開催のオープンキャンパスの講演も面白そうです。
https://www.s.u-tokyo.ac.jp/ja/event/open-campus/2026/
こちらから視聴できます。
明日のライブ配信はこちらから視聴できます。
https://www.youtube.com/live/iQSTVmWbYj4
今日のライブ配信はこちら。
https://www.youtube.com/live/cvcy-oDXfeQ

物理学に使える新しい画期的なAIが登場したそうです。Lanyon AIというものです。宣伝の文章が以下にのっています。このLanyon AIというのはMathematicaで有名なWolframの共同研究者でWolframと「新しい物理学」の研究を進めていた一般相対性理論などの研究者Jonathan Gorard(プリンストン大学）がCEOをつとめる会社が開発したものです。Lanyon AIの登場を告げる宣伝文はこちらから読むことができます。https://lanyon.ai/blog/welcome/　
この宣伝文では、Lanyon AIという新しく開発されたAIが、科学、エンジニアリング、ミッションクリティカルなタスク（航空宇宙や原子力など）に向けた、数学的に証明された「絶対に間違えない」新世代のAIであることが強調されています。

今までのAIとの違いはというと：
今までのAIもコードやその正しさを証明するプログラムを書くことはできましたが、「実装したコード」と「正しさの証明」を別々に生成するため、両者に矛盾が生じるリスク（例：コードは「＋」なのに証明は「－」になっている等のミス）がありました。Lanyon AIは、「構築段階から正しい（Correctness by Construction）」というアプローチをとっています。AIが不完全な人間の言葉でコードを書くのではなく、後述する独自の単一言語（DSL）で「仕様」を書き出し、そこから「コード」と「証明」を同時に自動生成します。もし仕様が厳密に証明できない場合は、そもそもコードが生成されないため、構造的にエラーや矛盾を起こすことが不可能になっています。

Lanyon AIの特徴は100%の構文的正確性です。
生成されるコードとデータは数学的に正しいことが証明されており、文法や仕様と実装の不一致といったミスを犯すことが「数学的に不可能」です。そのため少しの計算ミスも許されない宇宙開発、航空宇宙工学、クリーンエネルギーなどの分野において、信頼できる物理シミュレーションや計算基盤を提供できます。また、圧倒的なスピードと低コストも大きな特徴です。従来の最先端AIモデルと比べて、ほんのわずかな計算コストとトークン数で動作します。AIは数十行の仕様を書くだけでよく、それをシステムが一瞬で数万行のコードや証明に拡張するため、1秒間に数千行の正しい数学的証明を書くほどの超高速処理が可能です。
この宣伝文での Neurosymbolic approach（ニューロシンボリック・アプローチ）というのは、「ニューラルネットワーク（昨今のAI）」と「シンボリックAI（昔からの記号的・論理的AI）」のいいとこ取りをしたハイブリッド方式のことです。これまでのLLM（AI）は、アイデアを出したり文章を作ったりする「創造性」は豊かですが、計算や論理的思考においては嘘（ハルシネーション）をつくことがありました。一方、昔ながらのプログラム（シンボリック）は「創造性」はゼロですが、決められた計算や論理ルールは「絶対に間違えない」という特徴があります。Lanyonはこの両方を組み合わせ、「AI（LLM）がクリエイティブにアイデアや仕様を提案し、それをルールベースのアルゴリズム（シンボリック）が厳格に計算・証明して形にする」という仕組みを実現しています。LEANやRocq, Agdaなどという証明支援システムを利用してチェックするようです。

また、この宣伝文にあるDomain Specific Language (DSL：ドメイン特化言語)というのは、何でもできる汎用的なプログラミング言語（PythonやC++など）ではなく、「特定の分野（ドメイン）の目的を達成するためだけに作られた専用の言語」のことです。Lanyon AIは、数学や物理学を記述するためだけに特化した独自の言語（DSL）を持っています。この言語は非常に洗練され、情報が凝縮されているため、AIはこのDSLを使ってたった「数十行」の短い指示（仕様）を書くだけで済みます。汎用言語でダラダラと長いコードを書く必要がないため、AIが処理を間違える隙がなくなり、結果として超高速かつ低コストな処理が可能になっています。注意点としては、宣伝文の注釈にもある通り、Lanyon AIが保証しているのは「仕様と実装が100%一致する（構文的な正確性）」という点であり、「人間の曖昧な意図を完璧に汲み取れるか（意味的な正確性）」については現在も研究中とのことです。

こちらのGitHubには６つほど、Lanyon AIの応用例がのっています。
https://github.com/lanyonai

たとえば以下のツイートをご覧ください。
オイラー方程式の研究例ですが、「人間なら数ヶ月から数年かかるであろう『完璧に証明されたプログラムと数学的証明』の構築を、たった3分弱で終わらせたそうです。
1次元（1D）、2次元（2D）、3次元（3D）の空間における「等温オイラー方程式」と「完全な圧縮性オイラー方程式」を解くプログラムを、すべて合わせて約179秒で生成しました。1つの条件につき、わずか13秒〜54秒しかかかっていません。また単に動くコードを書いただけではなく、そのコードが物理法則に対して「絶対に間違っていない」ことを証明するためのコード（Lean 4という定理証明言語）を10,750行も生成しました。これには270の定義と156の定理が含まれています。さらに証明だけでなく、実際にシミュレーションを動かすためのC言語のコードを6,876行生成しました。このC言語コードは上記のLean 4によって「端から端まで正しさが証明（End-to-end formally verified）」されているものです。
つまり、「超高速・大ボリューム・バグ率0%」という、従来のプログラミングやAIでは到底不可能な離れ業をやってのけたという例のようです。

Euler’s equations of compressible hydrodynamics are a special case of the full compressible Navier-Stokes equations in the limit of zero viscosity. They admit shock waves, rarefaction fans, contact discontinuities, and complex thermodynamic interactions that necessitate subtle… https://t.co/A8DPR2QGXL

— Jonathan Gorard (@getjonwithit) July 30, 2026