今天上午开始了一个应用导向的项目。整个计划实施起来是我自己喜欢的风格，步骤如下：首先，从一些实际问题抽象出一些基础概念；然后，再在抽象后的概念上建立一般的数学理论；最后，通过一般理论指导启发建立新的不同方向的方法与算法。AI+Lean辅助初步完成了第一个部分，这部分很快的原因是我已经考虑好了基本概念，引导一下再形式化严格检验就可以。在第一部分的起始阶段AI自动填充了几个很小的定理并通过Lean进行严格检验，补充了一个同调理论的雏形——我觉得用处不大。但是，在第三部分，AI出现很多明显的错误，还是需要人纠正并提供合适的洞察。整体而言，实验结果也证明了AI有助于开发新的应用数学理论，不过，目前还是需要人提供最核心最本质的洞察。
发布于 浙江