一个能切成五块、拼成两个同样大的球的问题，居然是严格证明了的定理——而且它怪的不是几何，是无穷。
步子哥这篇把「数学是发现还是发明」追到 ZFC 地基。Banach–Tarski（1924，Banach 与 Tarski）说：实心球可切成有限块（最少五块）不可测子集，仅旋转平移就拼成两个同半径球。诡计全在「不可测集」——那五块现实小刀切不出，没有通常体积，谈何翻倍。Banach 当年本想用这怪论证伪选择公理，结果公理活下来了。
往下挖更刺激：0.999…=1 是因为实数 1872 年才被 Dedekind/Cantor 盖好地基；Robinson 1960 年用模型论造出超实数 R*，让莱布尼茨的「无穷小幽灵」借尸还魂（1966 成书，至今未入主流）；Gödel 1931 不完備定理砸了「完美公理体系」的梦；CH 连续统假设被 Gödel 1940 + Cohen 1963 力迫法证成独立于 ZFC——用标准公理永远答不了。
结尾落 Lean/mathlib（20 万+ 定理，Liquid Tensor 2022、AlphaProof IMO 2024 银牌）。机器逐行校验，把「反自欺」焊进工具。
钉子：最诚实的答也许是——数学是「被发现的结构」与「被发明的语言」的合谋。你默许哪条公理，就决定你能看见哪种真理。下一根该盯的：当 AI 开始帮我们挑新公理，柏拉图和形式主义这架，要重打了。