>>24 よく見つけたな

>>25　適当なこと言うな

Cluade5に読ませたら、まだ荒削りでこれだけではなんとも言えない。
まあ詰まるのも時間の問題だろう。

GitHubの検索エンジン経由では該当リポジトリの詳細が見つからなかったので、GitHub APIから直接情報を取得してみます。これは、**望月新一氏の「宇宙際タイヒミュラー理論(IUT理論)」を、定理証明支援系 Lean 4(+ Mathlibライブラリ)で形式化しようとしているプロジェクト**です。

**概要**
- リポジトリ所有者:Takkun-kohinata さん
- 開発方法:Claude Code(Opus 4.8 + Fable 5)を使い、AIと協力しながら証明を組み立てている、と説明されています
- 参照元:望月氏のIUT論文4本([IUTchI]–[IUTchIV])と、星裕一郎氏による解説書『宇宙際Teichmüller理論入門』(全27節)

**現在の進捗(ROADMAPより)**
- IUT理論の論理的な骨格(初期Θデータ → 遠アーベル幾何 → テータ関数 → Hodge劇場 → log-theta-lattice → 主定理 → Diophantine不等式)がLean上で一通り繋がっている状態
- 約20モジュール・100個ほどの宣言があり、本体部分には`sorry`(未証明の穴)や独自公理は0個、ビルドも通る
- ただし「opaque」(中身を厳密に埋めていない抽象的な仮定・ブラックボックス)が12個残っており、これを一つずつMathlibの前提から埋めていく、というのが現在(v2)の方針

**リポジトリの中身**
- `IutLean.lean` / `IutLean/` — Leanのソースコード本体
- `ROADMAP.md` — 上記の進捗・方針をまとめた計画書(かなり詳細、8万文字超)
- `SORRY_LEDGER.md` — 未解決の仮定・sorryの記録簿
- `REQUEST_theta_hull_derivation.md` — 特定の証明(theta hull導出)についての依頼・課題メモ
- `lakefile.toml` / `lake-manifest.json` — Lean用パッケージマネージャ Lake の設定ファイル

要するに、**数学界でも有数に難解とされるIUT理論を、AI支援でLeanによる形式証明という「機械的に検証可能な形」に落とし込もうという、個人による野心的な進行中プロジェクト**です。まだ多くの部分が抽象的な仮定(opaque)に依存しており、完全な形式化には至っていませんが、骨格部分は構築済み、という段階のようです。