034 · AI 写的证明通过了，信任消失了吗？Blanc 直接验证已部署的 EVM 字节码，让 AI 参与写证明，由 Lean 内核检查。值得追问的是：不再信任证明生成者以后，哪些判断仍留在证明之外？