Hack VC 宣布投资 Math Inc.，押注 AI 自动形式化验证基础设施

Hack VC 宣布投资 Math Inc.，后者正在构建工业级自动形式化能力，用 AI 智能体结合 Lean 等定理证明器把真实输入转化为机器可验证的证明。其旗舰智能体 Gauss 在三周算力内自主完成了 8 维和 24 维球堆积的形式化，约 20 万行代码，且无人类介入。