AI与数学

ChatGPT Plus的代码解析器功能强大，能快速解析数据、绘制图表，且无需输入数据即可绘制公共数据图，同时具有调试代码、绘制复杂数学函数图表等功能。此外，还能清理数据、提取颜色、将文本数据可视化等。随着GPT-4的推出，该功能将进一步增强， handle更多的文件、数据集和代码。

"本文介绍了ChatGPT的基本知识，包括其发展历程、技术原理和应用领域等方面，旨在帮助读者全面了解这一人工智能技术。"

这篇文章讲述了一位名为陶哲轩的数学家，利用人工智能助手GPT-4成功解决了数学难题，并在MathOverflow上分享了答案和经验。GPT-4为他提供了多种解题思路，帮助他更深入地进行研究和理解问题。此外，陶哲轩还分享了自己与GPT-4的对话记录，展示了如何在研究中正确使用AI。

编辑：编辑部 【新智元导读】尽管许多人并不愿意承认，但是很可能，AI会在十年内赶超人类数学家。 前几天，一篇加州理工和MIT研究者用ChatGPT证明数学定理的论文爆火，在数学圈引发了极大关注。 英伟达首席科学家Jim Fan激动转发，称AI数学Copilot已经到来，下一个发现新定理的，就是全自动AI数学家了！ 纽约时报近日也发文，称数学家们做好准备，AI将在十年内赶上甚至超过最优秀的人类数学家。 而陶哲轩本人，也转发了此文。 Siobhan Roberts参加了今年Machine Assisted Proofs举办的IPAM研讨会，随后她根据自己的经历和采访，写下了这篇关于AI和数学的文章 AI也来颠覆数学界了！ 如今，数学家们不得不正视一股最新的革命性力量——AI。 2019年，谷歌前雇员、现任湾区初创公司员工的计算机科学家Christian Szegedy预测，计算机系统将在十年内赶上或超过最优秀的人类数学家解决问题的能力。而去年，他把目标日期修改为2026年。 卡内基梅隆大学的逻辑学家Jeremy Avigad（蓝衣服），与学生在形式化数学暑期学校中 2018年菲尔兹奖得主、普林斯顿高等研究院的数学家Akshay Venkatesh目前还对使用AI不感兴趣，但他十分热衷于讨论AI相关的话题。 去年的采访中，Venkatesh表示，「我希望我的学生意识到，这个领域会发生非常大的变化。」 而最近他的态度是：「我不反对通过深思熟虑、甚至刻意地使用AI，来辅助人类的理解。但我坚信，对于我们使用它的方式，我们需要保持正念，慎之又慎。」 在今年二月，加州大学洛杉矶分校理论与应用数学研究所，曾举行了一场关于「机器辅助证明」的研讨会。 研讨会的主要组织者，就是2006年的菲尔兹奖得主、在UCLA任职的数学家陶哲轩。 他指出，用AI辅助数学证明，其实是非常值得关注的现象。 直到最近几年，数学家才开始担心AI的潜在威胁，无论是AI对于数学美学的破坏，还是对于数学家本身的威胁。 而杰出的社区成员们，正在把这些问题摆上台面，开始探索如何「打破禁忌」。 暑期学校的组织者，自左至右：Avigad，Patrick Massot和Heather Macbeth 从欧几里得几何原本到计算机代码 几千年来，数学家已经早已适应了逻辑和推理的最新进展。不过，他们准备好迎接人工智能了吗？ 洛杉矶盖蒂博物馆中17世纪古希腊数学家欧几里得的肖像：他衣衫褴褛，举着自己的几何论文《元素》 2000多年来，欧几里得的文本一直是数学论证和推理的范式。 卡内基梅隆大学逻辑学家Jeremy Avigad说，欧几里得以近乎诗意的「定义」开始，在此基础上建立了当时的数学——使用基本概念、定义和先前的定理，每个连续的步骤都「清楚地遵循」以前的步骤，以这样一种方式证明事物。 有人抱怨说，欧几里得的一些「明显」的步骤，其实不太明显，但Avigad博士说，但这个系统奏效了。 但是到20世纪以后，数学家们不愿意再将数学建立在这种直观的几何基础上了。 相反，他们开发了正式的系统，这个系统中有着精确的符号表示和机械的规则。 https://kilthub.cmu.edu/articles/journal_contribution/A_Formal_System_for_Euclid_s_Elements/6490703 最终，在这种系统下，数学可以被翻译为计算机代码。 1976年，四色定理成为第一个在暴力计算的帮助下被证明的主要定理。 四色定理：四种颜色足以填充地图，使得没有两个相邻区域颜色相同 会抱怨的AI：抱歉，我看不懂你们的定理 有这样一个数学小工具，被称为证明助手，或交互式定理证明器。 数学家会一步一步地将证明转换为代码，然后用软件程序检查推理是否正确。 验证过程会累积在一个动态规范参考库中，其他人都可以查阅。...