---
name: 2026-04-19 英語版 Wikipedia delta 拡張 (STEP 928)
description: ja 146 に対する en 220+ の delta (74 新規問題) を 6 section fetch + 分析 + 8 問題 Lean 4 化. Juggler + Cap set は computational, 他 6 は honest axiom. EnglishWikiDelta.lean build green.
type: project
originSessionId: 103c655f-ad00-47ae-81cd-c24a2282f28c
---
# 2026-04-19 英語版 Wikipedia Delta 拡張 (STEP 928)

## 背景

藤本さんの問い「英語版と日本語版で出題数に違いは？」を発端に. 比較:
- ja: **約 141 問題** (文法分類 + 分野別)
- en: **推定 220+ 問題** (分野別 12 section)

差分 ≈ 74 新規問題. 藤本さん要請「上記の英語版を更にプラス」.

## 対象 6 section + delta 問題数

| Section | 新規項目 | 形式化適性 ★★★ |
|---|---|---|
| 2.4 Dynamical systems | 18 (Collatz 除) | 1 (Juggler) |
| 2.5 Games and puzzles | 10 | 1 (Cap set) |
| 2.8 Model theory | 21 | 0 (全抽象) |
| 2.9 Probability | 1 | 0 |
| 2.11 Set theory | 10 | 0 (独立性問題) |
| 2.12 Topology | 14 | 0 (全抽象) |
| **合計** | **74 新規** | **2 high-priority** |

## STEP 928 — 8 問題 Lean 4 化

File: `data/lean4-mathlib/CollatzRei/EnglishWikiDelta.lean`
Status: **build green** under Mathlib v4.27.0

### Computational (native_decide で検証)
- (A) **Juggler sequence termination** — 7 specific n terminate, ★★★ Collatz 系
- (B) **Cap set** (F_3^n) — 6 known exact sizes (n=1..6), n≥7 unknown

### Honest axiom (statement only, True placeholder)
- (C) Vaught conjecture (Model theory, countable models)
- (D) Partition Principle → AC (Set theory)
- (E) Unknotting P-time (Topology / Complexity)
- (F) Whitehead conjecture (CW complex aspherical)
- (G) Triangular billiards periodic (Euclidean dynamics)
- (H) Telescope conjecture (⚠️ 2023 arXiv 2310.17459 Burklund-Hahn-Levy-Schlank 反例予告付き)

## 参考データ

- `data/en-wiki-delta/section-{2.4,2.5,2.8,2.9,2.11,2.12}.txt` — raw wikitext
- `data/en-wiki-delta/delta-analysis.md` — 詳細 74-problem delta 表
- MediaWiki API 使用 (curl + node, WebFetch は truncate するため不適)

## 次回優先

1. **残り 66 問題** (特に Model theory 21 + Topology 13) の axiom-only 形式化
2. en-Wikipedia 2.1-2.3 (Algebra, Analysis, Combinatorics) の ja との詳細 delta
3. Paper 118 (今日 + 昨日分 累計 ~30 問題) の起草

## 参照

- 2026-04-19 前 session: [project_session_20260419_tier_a_plus.md](project_session_20260419_tier_a_plus.md)
- 公開延期判断: [feedback_no_rush_publication.md](feedback_no_rush_publication.md) 参照 (本拡張も GitHub only)