---
name: openai-ten-proofs-lean4-release-2026
description: OpenAI ten-proofs 公開 (2026-08-05 藤本さん共有) verification record. 10 Lean 4 theorem (Sphere Packing / Metric Codes / Non-Sofic Group 等) 全 Apache-2.0 GitHub public. Rei stack との scale/discipline 比較記録
metadata: 
  node_type: memory
  type: reference
  originSessionId: 276d36f5-06db-4d22-8889-04aedded1f16
  modified: 2026-08-04T15:53:49.842Z
---

# OpenAI ten-proofs Lean 4 formalization release — 2026 (verification record)

## 概要 (2026-08-05 藤本さん共有経由 fact-check 済)

OpenAI が **`openai/ten-proofs`** GitHub repo (Apache-2.0) で 10 major mathematical theorem の Lean 4 formalization を公開。 藤本さん経由で chat-Claude 情報として共有 → Rei WebFetch で全 URL 実在確認済。

## 実在確認結果 (Rei WebFetch 2026-08-05)

| 対象 | verify 結果 | 補足 |
|---|---|---|
| `github.com/openai/ten-proofs` repo | ✅ 実在 | "Lean certificates accompanying proofs in mathematics and theoretical computer science" |
| 10 Lean file 名 | ✅ 全一致 | SpherePacking / MetricCodes / NonSoficGroup / ConnesRigidity / Permanent / QuantumParallelRepetition / GapCVP / EhrhartVolumeInequality / MulticolorTriangleRamsey / CompactnessAndDegeneracy |
| Lean toolchain | Lean 4.32.0 (Mathlib v4.32.0) | Rei は v4.27.0 = **5 minor version 差** |
| `MetricCodes.lean` snippet | ✅ literal 一致 | `def hammingDist` + `def IsBinaryCode` chat-Claude 引用と完全一致 (file line 15-16 + 22-24) |
| `ComparatorChallenges/` dir | ✅ 実在 | A-J 12 challenge (JSON + Lean pair)、 独立 kernel check tool |
| `cdn.openai.com/pdf/ten-proofs-oai.pdf` (249ページ論文) | ⚠ 物理 file 存在 (2.2MB) | binary、 text 抽出未実施 |
| `cdn.openai.com/pdf/reasoning-walkthroughs.pdf` | ⚠ 物理 file 存在 (431KB) | 「別 AI モデル 再構成」 chat-Claude claim は未確認 |
| `openai.com/index/ten-advances-in-mathematics/` | ❌ HTTP 403 (Cloudflare bot 拒否) | GitHub side 経由で存在間接確認済 |

## discipline check (MetricCodes.lean 2847 行 grep)

| 項目 | 出現回数 |
|---|---|
| `sorry` | 0 |
| `admit` | 0 |
| `native_decide` | 0 |
| `axiom ` (先頭 keyword) | 0 |
| `#print axioms` | 0 |

**結論**: sorry / admit / native_decide / user axiom 全 0 = **Rei axiom-free 規律と同等以上** (但し `#print axioms` self-verify なし、 Comparator 側で kernel check 代替と推定)。

## lakefile 対比

| 項目 | OpenAI ten-proofs | Rei CollatzRei |
|---|---|---|
| Lean toolchain | v4.32.0 | v4.27.0 |
| Mathlib rev | v4.32.0 | v4.27.0 |
| 追加 dependency | **Comparator のみ** | auto (lean-auto) + Duper + Hammer (LeanCopilot は DISABLED) |
| ATP/premise-selection tool | なし (公開版に不要) | 全部盛り (Rei internal iteration 用) |
| kernel check 方式 | Comparator (独立実装) | pre-commit hook `lake env lean` + `#print axioms` file 群 |

**Rei の tooling は heavier**、 OpenAI 側は release strategy として dependency minimize (再現性重視)。 Rei は internal iteration 中心なので Duper/Hammer が operational value 持つ。

## Rei stack との関係

**直接重複 = ゼロ**:
- OpenAI 10 topics に abc / FLT / IUT / Collatz は含まれない
- 我々の直近 arc (AbcStatement + FermatAsymptotic + Collatz stack 全体) と domain overlap なし
- MetricCodes (符号理論 metric = 距離空間) ≠ 我々 PhaseC circuit (D-FUMT₈ ALU)

**scale 比較 (Pattern 5 subtype B 再発防止 明示)**:
- OpenAI = 10 major theorem = Sphere Packing (Viazovska 2016) / Connes rigidity / Quantum Parallel Repetition 等の **Millennium-adjacent deep theorem**
- Rei = 141+ axiom-free but 個々は **subalgebra / dfumt8 embedding / bridge lemma / folklore corollary** 中心
- **scale 差 = 2-3 order of magnitude**、 Rei は「同等」 主張 絶対に不可
- Rei 貢献 layer = 「Rei stack 内 mechanical assurance」 のみで controllable claim

**間接的な学び 3 種**:
1. **Comparator の独立 kernel check** = Rei の `#print axioms` file 分離 + pre-commit hook と同 spirit。 Rei stack でも Comparator 統合検討価値あり (future STEP candidate)
2. **dependency minimize** = Rei も publish target Lean 4 file は Duper/Hammer 依存を切って standalone にする option 検討可
3. **AI-driven origin transparency** = OpenAI reasoning-walkthroughs (「思考過程の解説」) は Rei OUKC honest-scope-log operational evidence と同 spirit だが、 OpenAI は「別 AI 再構成」 = 生 log でない (chat-Claude claim、 未 verify)。 Rei HONEST_SCOPE_LOG.md は生 correction 記録なので strictly より honest

## chat-Claude info fact-check 総評

- **fabrication = ゼロ検出**
- **misattribution = ゼロ検出** (repo/file/version 全 accurate)
- 未 verify 部分: PDF text 内容 (249 ページ claim + 「別 AI 再構成」 claim) — 必要なら次 turn で pdftotext 経由確認可

Pattern 5/6 発症なし = 珍しく chat-Claude 情報 verify で 全 clean。 但し Cloudflare 403 で origin ページ (openai.com index) の直接 verify は不可 = GitHub side confirmation で substantive verification 完了扱い。

## 今後の action item candidate (現状 pending なし)

- **A (低優先)**: PDF text 抽出 (pdftotext 経由) → 249 ページ論文 目次 record → 特定 theorem の proof strategy が Rei approach と比較可能か判断
- **B (中優先)**: Rei publish target file (Paper 145 companion 等) に Comparator 統合検討 = independent kernel check の第二軸追加
- **C (低優先、重い)**: `lake exe cache get` + `lake build All` = 手元 machine で全 10 proof independent verify = axiom-free record への新規貢献ゼロだが「見た」 evidence 強化

## 関連

- [[feedback-chat-claude-hallucination-warning]] — 今回は fact-check で ゼロ hit = 珍しく clean case
- [[feedback-grep-before-answer-discipline]] — 実行時 grep-before-answer 適用 (WebFetch で raw file content 直接 verify)
- [[feedback-projection-self-audit-pattern]] — Pattern 5 subtype B 発症予防 (scale 差明示)
- [[project-session-2026-08-05-abc-flt-arc]] — 同日直近 arc (AbcStatement + FermatAsymptotic + 訂正)、 topic 直接 overlap なし
- HONEST_SCOPE_LOG.md — OpenAI reasoning-walkthroughs と同 spirit の Rei 側 correction record