Copilot上大分，仅数天，陶哲轩的估计验证工具卷到2.0！

陶哲轩迅速升级其数学估计验证工具至2.0版本，将其改造为更灵活的证明助手，支持Python符号代数包sympy，并重点关注半自动交互式证明；新版本能处理命题逻辑、渐近估计等多种数学任务，陶哲轩在开发过程中大量依赖Github Copilot辅助编程；陶哲轩还发布数学形式化证明实验视频，展示如何在33分钟内借助Copilot和Lean证明助手完成一页纸数学证明的形式化，开创了新的工作方式。