证明

形式化证明系统能够检查代码中的逻辑，却无法自行判断它是否忠实于原始研究目标。

为回答这个问题，他们提出TCSExam，用100项理论计算机科学科研任务，测试前沿AIAgent能否证明定理、开发Solver、构造数学对象，甚至挑战长期未解决的猜想。

提供中间引理与证明思路后，模型的完成数量明显增加，说明困难往往集中在关键引理的发现，以及如何将分散的推导组织成完整证明。