今天又测试了一个问题，接近于平凡的矩阵扰动的问题，是以前在设计一个算法的时候涉及的，我当时给了一个简单的分析，相当于代数的一个练习题。今天用AI+Lean的辅助方式重新求解，AI做了一点简单的扩展，整体上比我当时给出的证明要严格的多。遗憾的是这个算法最终放弃了，因为我自己都觉得创新性不够，即便是在一些情形运行的良好。
发布于 浙江
运筹士
今天又测试了一个问题，接近于平凡的矩阵扰动的问题，是以前在设计一个算法的时候涉及的，我当时给了一个简单的分析，相当于代数的一个练习题。今天用AI+Lean的辅助方式重新求解，AI做了一点简单的扩展，整体上比我当时给出的证明要严格的多。遗憾的是这个算法最终放弃了，因为我自己都觉得创新性不够，即便是在一些情形运行的良好。