质疑 Harmonic 电路证明：产物不含真实证明，$63 就能用 Claude 复现验证

thomasahle · x · 2026-10-29

thomasahle 对 Harmonic 的电路证明结果提出两点质疑：一是生成的文件里并不包含实际的证明，也没有从 Verilog 转译到 Lean 的版本，外界无法用 Lean 自行验证其正确性；二是系统在" supposedly 证明电路正确"之后才运行仿真，而仿真本身快得多——为什么不先跑仿真？他认为如果让 Claude 来做 Verilog 到 Lean 的转译并给出证明，代码和证明两者都能拿到，成本远低于 $63。这暴露了自动化定理证明产品在可验证性透明度上的短板。