top of page
検索

AI企業はなぜLean 4に向かうのか-

AIの答えは今、「説明」から「検査」へ向かいつつあります。

LLMは流暢な文章を生成します。しかし、それが正しいかどうかを保証することはできません。「もっともらしい誤り」——hallucination——は、LLM固有の問題として知られています。

先端的なAI企業・研究組織の一部が、明確に向かい始めている方向があります。

AIが生成した答えを、形式的に機械検査できる命題・証明・仕様に変えること。

その基盤として注目されているのが、定理証明支援システム Lean 4 です。

本稿では、一次資料・研究論文・一部報道をもとに、Lean 4を検証基盤に使い始めているAI企業・研究組織の事例を整理し、Lean 4が何を担い、何を担えないのかを示した上で、責任OSが担う次の層を示します。


▼責任OSに関するプレスリリースはこちら


1. AIの出力を機械検査へ接続する潮流の中で、Lean 4を採用する事例が増えている

Lean 4とは何か

Leanは、Leonardo de Mouraが2013年に開始したオープンソースの定理証明支援システムであり、現在のLean 4はプログラミング言語としての性格も備えた検証基盤です。Lean公式は、Leanを「プログラミング言語かつ証明支援系」として位置づけ、正しく保守可能で形式検証されたコードを可能にするものと説明しています。Lean FROは、数学研究、ソフトウェア・ハードウェア検証、AI支援定理証明への展開を掲げています。

重要なのは、Lean 4の検査は機械的であることです。「人間が納得する説明」ではなく、「Lean kernelが確認した証明」として結果が残ります。

企業・研究組織の事例

Mistral AI / Leanstral

Mistral AIは2026年7月2日、Lean 4向けのモデル「Leanstral 1.5」を公開しました。Leanstral 1.5は、Lean 4の形式証明エンジニアリング、定理証明、autoformalization向けモデルとして位置づけられています。さらに実コード検証やバグ発見も前面に出しており、大手AI企業がLean 4を「検証付きAIエージェント」の方向で使い始めた直接的な証拠です。

Harmonic / Aristotle

HarmonicのAristotle APIは、英語の問題からLean 4で証明・形式化し、Leanプロジェクトやコードリポジトリ内でも作業できると説明されています。Reutersも、HarmonicがAIのhallucination対策として、Lean 4で検証可能なコードを使う方向を取っていると報じています。「AIの信頼性を、自然言語による説明ではなく形式検証で担保する」代表例です。

Axiom Math / AXLE

Axiom MathのAXLEは、Lean 4証明の操作・抽出・検証をクラウドで提供するサービスです。AI数学のRLパイプラインやagentic proving workflowのために、Lean 4 toolingを大規模リクエストに耐える形へ拡張することを目標として説明されています。Lean 4がAI証明ワークフローのインフラ化に向かっている証拠です。

Math Inc. / Gauss

Math Inc.のGaussは、AIによるLean形式化エージェントです。強素数定理のLean形式化を約3週間で完了し、25,000行・1,000超の定理・定義を生成したと説明されています。AIが研究レベルの形式化作業を圧縮し始めている事例です。

Logical Intelligence / Aleph Prover

AlephはLean 4で機械検査可能な証明を生成するAI proverです。Ethereum FoundationのzkEVM暗号ライブラリ検証にも使われていると説明されており、数学証明だけでなく、暗号ライブラリ検証へLean 4が伸びていることを示します。

DeepSeek / DeepSeek-Prover-V2

DeepSeek-Prover-V2は、Lean 4での形式定理証明向けに設計されたオープンソースLLMです。MiniF2FやPutnamBenchで評価されており、DeepSeekのような主要AI研究チームもLean 4形式証明へ向かっていることを示します。Mistralだけでなく、複数の主要プレーヤーが同じ方向に動いています。

Google DeepMind / AlphaProof

DeepMindの発表および関連論文では、AlphaProofがLean theorem prover環境で形式証明を探索するRLエージェントとして説明されています。自然言語アプローチはもっともらしい誤りを出しうるため、Lean 4による形式検証と接続しています。最先端AI研究でも、形式検証が核心に入り始めています。

AWS / Cedar

AWSは認可ポリシー言語Cedarの中核コンポーネントをLeanで形式モデル化し、重要な正しさ・セキュリティ性質を証明し、Rust実装との差分テストで確認しています。Lean公式は、Cedarの新バージョンはモデル・証明・差分テストが最新でなければリリースされないと説明しています。Lean 4は数学AIだけでなく、本番ソフトウェアのセキュリティ検証にも使われています。

Rust-to-Lean verification pipeline

2026年5月の報告では、Rust暗号コードをLean 4へ持ち上げ、AristotleやAlephなどのAI proverで証明義務を閉じ、Lean kernelで検査するパイプラインが示されています。数学証明から実コード検証へ、Lean 4の適用範囲が広がっています。


2. なぜLean 4なのか

これだけ多くのAI企業・研究組織がLean 4に向かう理由は何でしょうか。

Lean 4の中心人物であるLeonardo de Mouraは、「When AI Writes the World's Software, Who Verifies It?」の中で、AIが重要ソフトウェアを書く世界では、検証層はAI生成器から分離されるべきであり、独立検証は哲学ではなくセキュリティアーキテクチャ要件だと述べています。

これが核心です。

AIが生成する層と、AIの出力を検査する層は分けなければならない。

LLMは流暢な文章を生成しますが、その内容が正しいかどうかは自己申告するしかありません。Lean 4のような外部検査器は、生成された命題・証明・コードを、LLMとは独立に機械的に確認します。

「AIが言った」から「検査器が通した」へ。この移行は、主要なAI企業・研究組織の一部で実際に進み始めています。


3. Lean 4だけでは、企業判断は完結しない

しかし、Lean 4は万能ではありません。ここが重要です。

形式化された命題しか検査できない

Lean 4は、Lean 4の言語で記述された命題のみを検査します。自然言語の問題を形式命題に落とす翻訳作業は、まだ難しい部分が残っています。

Aristotle APIを使ったケーススタディ（arXiv:2605.20120）では、複数の補助定理は検証された一方、主定理には未解決の sorry（未証明のプレースホルダー）が残ったと報告されています。「部分的に検証済み」と「全体として証明済み」は違います。

AI支援Lean証明の精度はまだ限界がある

FormalProofBenchでは、大学院レベルの数学について、Lean 4形式証明生成において最良モデルでも33.5%の精度にとどまったと報告されています。

SorryDBは、GitHub上の実Leanプロジェクトから未解決証明タスクを集めるベンチマークですが、競技数学だけでは実務的なLean証明能力を測れない問題を示しています。TheoremBenchも、現在のproverが長く依存関係の多い定理ではまだ偏りや非効率があると指摘しています。

未確認条件が残る

Logical IntelligenceのAleph事例でも、Lean 4で検査可能な形式化を作れても、外部の古典定理、問題文の形式化、仕様の置き方、ツールチェーン上の前提が別途確認対象として残る場合があります。

つまり、Lean 4で何かを検査した後でも、何が検証済みで、何が未確認条件として残っているのかを管理する層が別途必要になります。

誰が、どの条件で採用したのかは、Lean 4が扱う問いではない

Lean 4は命題が証明されているかどうかを確認します。しかし、

  • 誰がその証明に基づいてAI判断を正式運用に採用したのか

  • 採用時にどの未確認条件が残っていたのか

  • その採用判断を後から第三者が確かめられるのか

これらはLean 4が扱う問いではありません。これらは、企業の責任情報の問いです。


4. 制度側も同じ方向に動いている

技術側のLean 4の流れと並行して、制度側からも検証可能性への要求が高まっています。

ISO/IEC 42001は、AIを開発・提供・利用する組織がAIマネジメントシステムを確立・運用・改善するための国際標準で、リスク管理、信頼、説明責任を支える枠組みとして説明されています。

EU AI Act（Regulation (EU) 2024/1689）は、2024年8月1日に発効し、段階的に適用されます。高リスクAIシステムに対して、ライフサイクルを通じた自動ログ記録を可能にすること（Article 12）、人間がAI出力を理解・監視し、必要に応じて採用しない判断ができる監督状態（Article 14）を求めています。

技術側ではLean 4が「検査可能なAI」を押し上げています。制度側ではISO 42001やEU AI Actが「記録・監査・説明責任」を求めています。


5. 責任OSが担う次の層

ここで責任OSが登場します。

責任OSは、形式検証、来歴、監査証跡、AI assuranceと無関係な新語ではありません。むしろ、それらの既存系譜を前提にしています。独自性は、AIモデルそのものではなく、AI判断を企業が正式運用で採用する際の責任状態を第一対象に置く点にあります。形式検証も、モデルの性能や安全性だけでなく、責任情報・未確認条件・判断順序・採用状態が後から確認可能に保持されることを確かめるために使われます。この点で責任OSは、既存のAI assuranceやaudit trailを置き換えるものではなく、それらを企業判断の採用状態へ接続する責任情報レイヤーです。

具体的には、責任OSは次の問いに答えます。

  • AIはどの情報を見て判断したのか（来歴）

  • どの条件を満たしていたのか（採用条件）

  • 何が未確認条件として残っていたのか（未確認条件）

  • 誰がどこまで確認したのか（確認主体・確認状態）

  • どの順序で判断が行われたのか（状態遷移）

  • 後から第三者が確かめられるのか（検証可能性）

責任情報（Accountability-Relevant Information）は、AI判断について、結果だけでなく、来歴、監査証跡、追跡可能性、確認済み条件、未確認条件、関与主体、判断の順序を含めて、後から責任状態を確かめられるようにする情報です。

ADIC（Advanced Data Integrity by Ledger of Computation）は、この責任情報を後から検査できる証跡として固定する技術基盤です。単なる説明文ではなく、再検査可能な記録にします。

ALS（Algorithmic Legitimacy Shift）は、「人間が確認したから安心」という前提だけでは構造的に限界が生じる局面を扱う理論です。

Lean 4は、証明できた部分を明確にします。責任OSは、証明できていない部分を未確認条件として残し、そのAI判断を企業が正式運用で採用できる状態かを管理します。

Lean 4は責任OSの競合ではありません。Lean 4が広がるほど、責任OSの必要性は強まります。


まとめ

世界のAI企業・研究組織は、AIの出力を「自然言語でもっともらしく説明するもの」から「形式化され、機械検査できるもの」へ移そうとしています。Mistral、Harmonic、Axiom Math、Math Inc.、Logical Intelligence、DeepSeek、DeepMind、AWSの事例は、この潮流を明確に示しています。

しかし、Lean 4で何かを検査した後でも、何が検証済みで何が未確認条件として残っているのかを管理し、誰がどの条件でそのAI判断を企業として正式運用に採用したのかを後から確かめられる形にする層が別途必要になります。

責任OSは、その層を担います。技術側のLean 4の流れと制度側のISO 42001・EU AI Actの流れを、企業実務の採用状態へ接続する責任情報レイヤーです。

検査済みの命題を、企業が採用できる責任状態へ接続すること。これが責任OSの役割です。


参考資料・一次資料

Lean 4本体

AI企業・研究組織の事例

限界・ベンチマーク

制度・標準

責任OS


株式会社GhostDrift数理研究所 https://www.ghostdriftresearch.com

 
 
 

コメント

bottom of page