青蛙与蟾蜍梗图讽刺形式验证:没读过的正确性证明等于什么都能证

banteg · x · 2026-11-11

一张「青蛙与蟾蜍」绘本风格的梗图在 AI/安全圈刷屏:Frog 宣称「现在程序有了正确性证明」,Toad 反问「可我们没读过这个证明,它什么都可能『证明』过」,Frog 承认说得对。被引用的推文调侃:早知道就不折腾论文和符号模型了,直接写 600 万行 Lean 来形式化验证 Signal 就好。梗图精准戳中形式验证的痛点——生成证明容易,人是否真正理解证明才是关键。