Yuren Tang 用 Lean 4 给出了 Erdős #306 的完整、机器验证证明（sorry-free，仅两条经典公理），但没有配套论文。
本站从约 21,000 行 Lean 里把这台“机器”逆向成人能读的数学，并按阅读深度分成三条平行轨道。下面挑一条开始。
一个公式都不碰。用「分数积木」「旋转指针对齐」「主音压过杂音」三个画面，把整条证明的核心思路讲成人话。
每一步都从头推导，不跳步。七章讲义：从计数到 Fourier 反演、主弧高斯下界、次弧字符衰减、拍频收口、构造、能量–熵，直到两条底层公理。所有积分、余项、常数都摊开算。
三层机器的依赖图 + 逐引理陈述与 Lean 行号定位（圆法引擎 / R2 构造 / minor-arc·SBEE / 公理）。只陈述不推导，供快速核对结构与出处。
没接触过就从人人能懂版开始；想真正学懂证明、又不怕算式，直接读完整细节讲义（推荐先看它的总纲了解全局地图）；只是来核对某个引理或 Lean 位置，去技术总览。三条轨道彼此互链，随时可跳。
sorry-free；整棵证明树仅依赖两条 Rosser–Schoenfeld (1962) 命名公理。