今天，基于AI+Lean的形式证明了我的一个计划里的主要定理，其中一部分是之前没考虑过的，整个证明只有两三页，比较简单。不过，这个定理是建立在新的概念上，所以不是靠搜索整合可以直接得到证明。整个过程中AI提供了一种开放性的探索，Lean提供严格检验。
发布于 浙江
运筹士
今天，基于AI+Lean的形式证明了我的一个计划里的主要定理，其中一部分是之前没考虑过的，整个证明只有两三页，比较简单。不过，这个定理是建立在新的概念上，所以不是靠搜索整合可以直接得到证明。整个过程中AI提供了一种开放性的探索，Lean提供严格检验。