Erdős–Straus Bench v0.2

五百萬個精確證人，而且不是證明。

Erdős–Straus bench 是 MMLC 第一個認真的應用：從搜尋證書回收公式、以符號驗證、提升模數，然後把整件事稽核一遍。以下每個數字都是有限驗證。它們沒有一個是猜想的證明 —— 而報告自己第一段就先講了。

問題

Erdős–Straus 猜想說：對每個整數 n ≥ 2，都存在正整數 x、y、z 使得

4/n = 1/x + 1/y + 1/z

一個「證人」就是一組精確的三元組。這個 bench 用兩種方式產生證人：直接從週期公式得到，或在沒有公式覆蓋該剩餘類時去搜尋一個因子證書。

全體證人串流雜湊成單一值，所以整個五百萬整數的執行是一個可比對的物件：

text

e13790fe5d7abcbda27a08433c9e42b640b605dda9f828e3e175f52ed602f160

有意思的結果不是證人的數量，是有多少搜尋案例變成了公式。同一台機器、同一區間、同一搜尋預算：

已確立

21,428 個搜尋案例中有 12,011 個被回收成直接的公式證人 —— 在同一區間、同一預算下，搜尋負擔下降 56.05%。

機制是一條管線，不是一個靈感。把公式外的證書依 (x 偏移, d, a) 聚類、推導週期、建立候選公式、以符號驗證，然後提升模數。

在基底模 840 上的貪婪選擇自己挑出三個候選，而它們與已經凍結在 Runtime 裡的公式完全一致。

候選	觀察數	週期	對模 840 新增的類
`h`=1, `d`=10, `a`=7	913	280	73、193
`h`=1, `d`=5, `a`=7	867	140	433、673
`h`=1, `d`=20, `a`=7	740	280	313、793

已確立

selection_matches_runtime = true。自動選擇器與凍結公式庫在沒有被告知的情況下達成一致。

加入 q = 11、17、23 的質數證書需要提升模數，因為它們的週期 44、68、92 不整除 840。

宣告值

不同模數下的「未覆蓋數量」不可直接相比。這個 bench 在每次提升時，都在同一個新模數下保存加入前／加入後的邊際覆蓋，正是為了讓那個往上長的未覆蓋欄位不會被讀成退步。

公式週期中每一個有效剩餘類都被展開成獨立的符號案例，而不是驗一次抽象恆等式就把整數性條件揮手帶過。

這是這個 bench 找到最有用的一件事，而它關於 MMLC，不關於數論。

在 n = 4565 刻意竄改一個證人 —— 把 z 挪成 z+1 —— 會產生一個極小但不為零的精確殘差。在 numeric_tolerance = 1e-12 之下，稽核漏掉了它。在 exact profile 之下，每次都抓到。

已確立

純數學帳本的數值容忍度必須恰好為 0。「只是很小」的容忍度是一台假陰性產生器，而這個 bench 把那個失敗案例永久保留為負對照。

同一組稽核裡還有：256 個清潔證人全部通過、32 個 z→z+1 竄改以 precision／recall 1.0 定位，以及 32 個有號殘差案例在全域加總為零、但每個局部錯誤仍被找出來。

發現區間與驗證區間是分開的。那不是統計上獨立的測試集；它只防止在大型掃描途中一邊看結果一邊改公式庫。

v0.2 公式庫凍結之後，五百萬範圍內剩下的 12 個模 840 搜尋類，依因子分成三群：

三群都需要提升到模 10,920。那是 v0.3 的優先研究節點，而在那之前，這些類都不能宣稱已被覆蓋。

方法論文件對剩下的形式化缺口說得很直白：週期條件目前是程式內的週期證書。形式證明仍然需要把整除與同餘條件移植到 Lean 或 Coq。