AI写代码越狂野，程序员越需要数学

量化巨头Jane Street打破了坚持25年的态度，突然重仓“形式化方法”（用数学逻辑去证明代码无Bug）。这背后的转变，恰恰是被AI逼出来的。

现在AI写代码快如流水，但也留下了大量难以排查的“代码垃圾”。人类根本审不过来，传统测试也无法穷尽所有漏洞。既然如此，出路就变成了用硬核的数学定理给AI代码拉红线。

最妙的是，人类以前最讨厌写繁琐的形式化证明，但AI却有无限耐心。AI负责写代码，顺便把“数学证明步骤”也写好，最后交给100%客观的编译器去校验。只要数学逻辑通过，代码哪怕写得再乱，也绝不可能出错。

编程的终局变了。未来程序员的真正价值，从“写代码”变成了“下定义”。把具体的实现和证明扔给AI，人类只需用数学语言告诉机器：什么才是对的。

blog.janestreet.com/formal-methods-at-jane-street-index