编译
绿萝
在洛杉矶盖蒂博物馆的藏品中，有一幅17世纪古希腊数学家欧几里得的肖像：衣衫褴褛、蓬头垢面，双手沾满污垢，举着他的几何学著作《几何原本》。
欧几里得肖像。
两千多年来，欧几里得的著作一直是数学论证和推理的典范。
卡内基梅隆大学逻辑学家JeremyAvigad说：「众所周知，欧几里得以近乎诗意的[定义]开始。然后，他在此基础上建立了当时的数学，使用基本概念、定义和先验定理，以这样一种方式证明事物，即每一步都[清晰地遵循]前一步。」
Avigad博士说，有人抱怨欧几里得的一些「明显」步骤并不明显，但该系统仍然有效。
但到了20世纪，数学家不再愿意将数学建立在这种直观的几何基础上。相反，他们开发了正式的系统——精确的符号表示、机械规则。最终，这种形式化使得数学能够转化为计算机代码。
年，四色定理（该定理指出四种颜色足以填充地图，因此没有两个相邻区域具有相同的颜色）成为第一个借助计算强力证明的主要定理。
现在，数学家们正在努力应对最新的变革力量：人工智能。
年，曾在谷歌工作、现就职于旧金山湾区一家初创企业的计算机科学家ChristianSzegedy预测，计算机系统将在十年内赶上或超过人类最优秀数学家解决问题的能力。去年他将目标日期修改为年。
普林斯顿高等研究院数学家、年菲尔兹奖获得者AkshayVenkatesh目前对使用人工智能不感兴趣，但他热衷于谈论它。「我希望我的学生意识到他们所处的领域将会发生很大的变化，」他在去年的一次采访中说道。他最近补充道：「我并不反对深思熟虑和刻意地使用技术来支持我们人类的理解。但我坚信，注意我们使用它的方式是至关重要的。」
二月，Avigad博士参加了在加州大学洛杉矶分校纯粹与应用数学研究所举办的「机器辅助证明」研讨会。这次聚会吸引了数学家和计算机科学家的非典型组合。「这感觉很重要，」该大学数学家、年菲尔兹奖获得者、研讨会的主要组织者TerenceTao说。
暑期学校组织者（左起）：Dr.Avigad,PatrickMassotofParis-SaclayUniversityandHeatherMacbethofFordham。
Tao博士指出，直到最近几年，数学家们才开始担心人工智能的潜在威胁，无论是对数学美学还是对他们自己。他说，著名的社区成员现在正在提出这些问题并探索潜在的「打破禁忌」。一位引人注目的研讨会参与者坐在前排：一个名为「举手机器人」的梯形盒子，每当在线参与者提出问题时，它就会发出机械的低语并举起手。「如果机器人可爱且不具有威胁性，那就很有帮助，」Tao博士说。
学生们在该学院数学形式化暑期学校期间开展了一个小组项目。
带来「证明抱怨者」
如今，优化我们生活的小工具并不缺乏——饮食、睡眠、锻炼。威斯康星大学麦迪逊分校数学家JordanEllenberg在研讨会休息期间说：「我们喜欢给自己附加一些东西，以便更容易把事情做好。」他补充说，人工智能设备可能也会对数学产生同样的影响。「很明显，问题是，机器能为我们做什么，而不是机器会对我们做什么。」
一种数学小工具称为证明助手，或交互式定理证明器。（「自动化」是20世纪60年代的早期化身。）数学家一步步将证明转化为代码；然后软件程序检查推理是否正确。验证积累在一个库中，这是其他人可以查阅的动态规范参考。霍斯金森形式数学中心（由加密货币企业家CharlesHoskinson资助）主任Avigad博士说，这种形式化为当今的数学奠定了基础，「就像欧几里得试图编纂和整理数学一样。为他那个时代的数学奠定了基础。」
最近，开源证明辅助系统Lean备受