寻找算法
它能做什么：在一个定义清楚的数学问题里，搜索可能的算法构造。
接下来要做什么：由人或检查工具确认构造正确，并与合适的旧结果比较。
它不能证明什么：不能证明所有算法问题现在都变简单了。
从这里开始 · 5 分钟
AI 如何改变理论计算机科学
AI 正在一些边界清楚的任务里成为有用的研究工具。但它不是一台会自动发现并证明所有真理的神奇机器。 这篇指南会用尽量简单的话，把两者的区别讲清楚。
先说结论：
目前证据最能支持的，是 AI 可以帮助搜索、生成候选答案、写形式化证明，以及检查一个大论证中的某一部分。
要问什么问题、结果是什么意思、更大的结论是否成立，仍然需要人来判断。
先认识四个词
不了解这个专业，也能看懂讨论。
理论计算机科学关心：计算机能做什么、一个问题需要多少时间和内存，以及我们怎样证明这些答案。
- 算法
- 可以理解成“做事的菜谱”：一步一步解决问题的方法。即使两种方法最后都能算出答案，更快的方法仍可能很重要。
- 证明
- 一步步说明“为什么这个结论一定成立”的论证。形式化证明可以让计算机逐行检查。
- 复杂度
- 研究问题变大以后，需要的时间和内存会怎样增加。一个问题理论上能解，不代表实际中能便宜地解。
- 形式化证明
- 用精确语言写出的证明。Lean 这类软件可以检查每一步，而不是只靠读起来“很像对”的解释。
已经改变的到底是什么
四个领域，四种不同强度的证据。
关键问题不是简单的“AI 能不能做”，而是“它在什么设定里做了哪一步，结果由谁检查”。
搜索证明
它能做什么：在证明助手中搜索形式化证明，由助手逐步检查。
接下来要做什么：研究者仍然要选问题、设定形式化范围，并判断什么才算成功。
它不能证明什么：解决几个范围很窄的例子，不等于能解决开放研究问题。
补上一块证明拼图
它能做什么：找到一个有限对象，放进人类设计好的更大证明框架里。
接下来要做什么：检查这个对象，再确认已有框架确实能推出完整结论。
它不能证明什么：不能因为补上了一块拼图，就说整个复杂度问题已经解决。
改变科研工作
已经能看到：工具可以协助检索资料、写代码、做形式化，以及检查项目中的一部分。
仍然不确定：这些任务层面的变化，会怎样影响岗位总数、职业路线和科研质量。
我们不会做：把几个案例直接夸大成“AI 会取代研究者”的无来源预测。
一条硬边界
盒子里的有用结果，仍然只是在盒子里。
很多误导性标题，都是因为偷偷拿掉了下面某个限制：
- 找到一个构造，不等于证明一个普遍定理。成功找到一个对象，不代表知道怎样找到所有对象。
- 测试得分高，不等于证明正确。高分说明它可能擅长某个测试，不说明每个回答都是真的。
- 解决一个例子，不等于完成一个研究方向。系统可能在一个范围清楚的问题上成功，却在下一题失败。
- 检查器检查的是证明，不是新闻标题。形式化写下的命题，必须和标题里真正想说的内容一致。
继续往下看