---
name: Andrica + Erdős-Straus Lean 4 拡張 (2026-04-20 morning)
description: Paper 116 Andrica n=25..50 + Paper 117 Erdős-Straus n=21..50 の Lean 4 拡張. 56 新 zero-sorry theorems. commit c62e69a.
type: project
originSessionId: 79081859-fd56-4821-a0d2-932be27d647a
---
# Andrica + Erdős-Straus Lean 4 拡張 (2026-04-20)

## 対象

- Paper 116 (Andrica's Conjecture Lean 4 Mathlib) の scale 延長
- Paper 117 (Erdős-Straus Lean 4 Small-n) の scale 延長

## 成果物

### Andrica (`AndricaConjecture.lean`)

- **26 new theorems**: `andrica_n25` から `andrica_n50` (consecutive-prime pair 方式)
- `ANDRICA_PAIRS_50 : List (Nat × Nat)` aggregate (50 pairs)
- `ANDRICA_PAIRS_50_all_valid` 単一 native_decide で全 50 pair 検証
- `andrica_n30_margin` 観察: g²=196 vs 4p+1=453, ratio **0.433** (margin 十分)

### Erdős-Straus (`ErdosStraus.lean`)

- **30 new theorems**: `es_n21` から `es_n50` (explicit (a,b,c) witness)
- `es_extended_solvable` 集合 theorem: ∀n ∈ [2, 50] erdosStrausSolvable (旧 es_small_solvable を 20 → 50 に延長)
- 観察: range 内の largest c = **318,660 at n=47** (vs smallest c=2 at n=2, **159,330 倍**)

## 累計

- **56 new zero-sorry theorems** across 2 files
- Mathlib v4.27.0 / Lean 4 v4.29.0 で both build green (~15秒)
- commit: `c62e69a`

## 残り方向性

### Andrica (Paper 74 候補)
- STEP 794 の **A(n)·log(p) ≤ 3.34** 実測則を Lean 4 で形式化
- 最強 Cramér 仮定 g = O((log p)²) を引用して conditional 証明
- mpmath bridge で rigorous interval bound

### Erdős-Straus
- **Mod 840 open residues** {1, 121, 169, 289, 361, 529} の分析
  - n ≤ 1000 でこれらの residue に入る n の witness 探索
  - Mordell 1969 + Terzi 1971 が閉じた residue との gap 特定
- n=51..100 への延長
- Paper 109 Ricci-flow S-category (84.3% S) との接続強化

## D-FUMT₈ 状況

| 項目 | state |
|---|---|
| Andrica n ≤ 50 Lean 4 | TRUE |
| Andrica 全般 (∀n) | NEITHER (OPEN 40年) |
| Erdős-Straus n ≤ 50 Lean 4 | TRUE |
| Erdős-Straus 全般 (∀n ≥ 2) | NEITHER (OPEN 78年) |
| Andrica A(n)·log(p) ≤ 3.34 | FLOWING (empirical 10⁷ 検証, Lean 4 化 pending) |
| Erdős-Straus mod 840 open 6 class | NEITHER |