Alex Kontorovich (@AlexKontorovich)：“我明天在牛顿研究所@NewtonInstitute 的演讲预览（欢迎评论）我的主要兴趣是研究数学：解决问题、证明定理。
在 2019 年之前，我习惯于使用 Mathematica 检查论文中繁琐且容易出错的代数。
做一次，就再也不用浪费时间检查了。
如果我有一个引理，在一篇 60 页的论文中，我可能有 20 个参数，其中十几个参数都在不同的范围内移动，并且需要在最后完美排列，那么即使是一个杂散的负号也可能毁掉整篇论文。
（我所描述的内容在现代研究数学的许多领域中都很常见。
）但是我参与形式化的最初动机很简单：我希望它会加快我的工作流程。
来源：HackerNews New
