AI人工智能|计算机距离数学推理自动化有多近？( 二 )
克莱帕拉说：“您可以采用任何一种数学参数 ， 并使用一个工具对其进行编码 ， 然后将您的参数连接在一起以创建安全性证明 。”
在数学中 ， 定理证明者帮助产生了复杂的 ， 计算繁重的证明 ， 否则这些证明将占用数以百计的数学家的生命 。开普勒猜想描述了堆叠球体（或从历史上说是橘子或炮弹）的最佳方法 ， 它提供了一个很好的例子 。1998年 ， 托马斯·海尔斯（Thomas Hales）和他的学生山姆·弗格森（Sam Ferguson）一起使用各种计算机数学技术完成了证明 。结果是如此繁琐（结果占用了3 GB） ， 以至于12位数学家对它进行了长达数年的分析 ， 然后才宣布99％的观点是正确的 。
文章图片
文章图片
开普勒猜想并不是机器可以解决的唯一著名问题 。四色定理说 ， 您只需要用四种颜色就可以对任何二维图进行着色 ， 这样就不会有两个相邻的区域共享一种颜色 。数学家于1977年使用计算机程序对四色定理进行了定理 ， 该程序通过五色图进行显示 。都可以减少到四个 。在2016年 ， 三位数学家使用计算机程序来证明长期存在的公开挑战（称为布尔毕达哥拉斯三元组问题） ， 但该证明的初始版本为200 TB 。有了高速互联网连接 ， 如果你要下载它需要三周多的时间 。复杂的感觉
这些例子通常被称为成功 ， 但它们也增加了争论 。证明四色定理的计算机代码已经有40多年的历史了 ， 人类无法自行检查 。哥伦比亚大学的数学家迈克尔·哈里斯（Michael Harris）说：“从那以后 ， 数学家们一直在争论 ， 这是否是一个证明 。”
文章图片
文章图片
另一个困扰是 ， 如果他们想使用定理证明 ， 数学家必须首先学习编码 ， 然后弄清楚如何用计算机友好的语言表达他们的问题 ， 这是不利于进行数学运算的活动 。哈里斯说：“当我将问题重新组织成适合该技术的形式时 ， 我自己就会解决问题 。”
许多人只是认为他们的工作中不需要定理求解器 。伦敦帝国理工学院的数学家凯文·巴扎德（Kevin Buzzard）说：“它们有一个系统 ， 它可以用铅笔和纸书写 ， 并且可以工作 。”三年前 ， 他将工作从纯粹的数学转向了定理证明和形式证明 。“计算机为我们做了惊人的计算 ， 但它们从来没有独自解决难题 。”他说 ， “直到他们这样做 ， 数学家们才不会购买这种东西 。”
【AI人工智能|计算机距离数学推理自动化有多近？】但是巴扎德和其他人认为也许他们应该这样做 。一方面 ， “计算机证明可能不像我们想象的那样陌生 ， ” 德迪奥说 。最近 ， 他与现在斯坦福大学的计算机科学家斯科特·维特里（Scott Viteri）进行了逆向工程 ， 对少数著名的经典证明（包括Euclid's Elements的其中之一）和数十个使用定理证明器Coq编写的机器生成的证明进行了查找 。为了共同点 。他们发现 ， 机器证明的网络结构与人们制作的证明的结构非常相似 。他说 ， 这种共有的特征可能会帮助研究人员找到一种方法 ， 从某种意义上说来证明自己的助手 。
文章图片
文章图片
德迪奥说：“机器证据可能并不像看起来那样神秘 。”
还有人说 ， 定理证明者可以是计算机科学和数学领域中有用的教学工具 。在约翰霍普金斯大学 ， 数学家艾米丽·里尔（Emily Riehl）开发了一些课程 ， 学生可以使用定理证明者来编写证明 。“这迫使您组织得井井有条 ， 思路清晰 。”她说 ， “第一次写证明的学生可能很难知道他们需要什么并理解逻辑结构 。”
推荐阅读
- 新科技嗅|人工智能可以应用在哪些方面
- 技术编程|人工智能在大视频运维中如何实现CDN硬盘故障预测？
- 天问|点火480余秒！天问一号探测器完成深空机动 距离地球约2940万千米
- 新加坡|新加坡大学生人工智能创新大赛开幕式举行 星环科技提供建模平台
- 情感|异地恋如何维持感情? 坚持这3点, 才能战胜距离
- AI人工智能|“眼健康黑科技” AI智能眼科检测仪来了！展锐虎贲T710开发板等你来盘！
- AI人工智能|非接触式测谎分析系统应用
- AI人工智能|错题打印机喵喵机P1彩色版，学习的多种打开方式
- AI人工智能,智能电视|康佳KKTV智能语音电视，找回自己的专属乐趣
- AI人工智能|人工智能技术助力民族语言保护大有可为