2006年，吴文俊和Munford一起分享了邵逸夫数学奖，值得回味的是：Mumford用概型语言写出了其代表作《几何不变量理论》，但吴文俊却认为代数几何的概型语言已经过时了，其获奖原因是因为他所提出的数学机械化。
1977年，吴文俊提出了他的数学机械化思想，但就在其前一年，数学界出现了一个惊人的消息，四色猜想被计算机证明了，这是第一个依赖机器证明的数学定理。这是一个纯粹的巧合，还是故意蹭大猜想的流量呢？这个问题并不是很重要，重要的是吴文俊所谓的数学机械化与机器证明有什么差别。一般的解释是数学机械化是让计算机自动做数学，不像机器证明需要人脑针对专门的问题来编程。
如果数学机械化能够自动处理各种数学问题，那么自然是更加优越，但吴文俊的数学机械化远没那么神奇，主要就是处理平面几何的问题，通过众所周知的坐标法，把它转化成线性方程组的形式消元硬算。一般中学平面解析几何都会放几个引例，说明解析法可以处理平面几何问题，但这样的例子是精心设计的，其他例子理论上可能还能算出来，但实际计算则是非常麻烦，所以就要需要借助计算机来实现。由此看来，数学机械化这个名称过于托大了，应该叫平面几何机械化或初等几何机械化，也就是专门处理这一类问题的数学程序。后来的数学机械化有所发展，能够处理微分几何中的一些问题，但这个发展意味着程序有更新，那就不是机器自动完成的，本质上还是在人工编程做机器证明啊！
综上所述，想要机器能够自动完成，就是针对某一类问题编好的程序；想要处理更多的问题，就需要牺牲机械化进行人工编程。当然，我们可以把所有编好的数学程序放到一起封装起来，这样好像就看不出人工编程的痕迹，同时也可以解决一大类的数学问题，不知道DeepSeek能不能品味出这里讽刺的意思。
加载中，请稍候......
喜欢
加载中…