数学家揭示“等于”在数学中具有多种含义

有一些漂亮的模糊的概念在数学中，这可能很难理解，但“等于”的含义是我们认为我们已经涵盖的含义。

事实证明，数学家实际上无法就两个事物相等的定义达成一致，这可能会给越来越多地用于检查数学证明的计算机程序带来一些麻烦。

这场学术争吵已经持续了几十年，但最终达到了顶峰，因为用于“形式化”或检查证明的计算机程序需要有明确、具体的指令;不是对数学概念的模棱两可的定义，这些概念可以解释或依赖于计算机所没有的上下文。

伦敦帝国理工学院的英国数学家凯文·巴扎德（Kevin Buzzard）在与计算机程序员合作时遇到了这个问题，这促使他重新审视定义“这等于那”，“挑战各种关于平等的合理口号”。

“六年前，”Buzzard在他的预印本中写道发布到 arXiv 服务器，“我以为我理解了数学相等。我以为这是一个定义明确的术语......然后我开始尝试在计算机定理证明器中做硕士水平的数学，我发现相等是一个比我想象的更棘手的概念。

等号 （=） 的两条平行线优雅地表示放置在两侧的物体之间的奇偶校验，是由威尔士数学家发明的，罗伯特·雷克雷，在1557年。

它一开始没有流行起来，但随着时间的推移，Recorde 的出色直观符号取代了拉丁语短语“aequalis”和后来奠定了基础用于计算机科学。在发明整整 400 年后，等号于 1957 年首次被用作计算机编程语言 FORTRAN I 的一部分。

平等的概念有一个更长的历史不过，至少可以追溯到古希腊。现代数学家在实践中使用“相当松散”的术语，Buzzard写.

在熟悉的用法中，等号设置了描述代表相同值或含义的不同数学对象的方程式，这可以通过一些开关和左右逻辑转换来证明。例如，整数 2 可以描述一对对象，1 + 1 也可以。

但是，自19世纪末集合论出现以来，数学家们一直在使用相等的第二种定义。

集合论不断发展，数学家对等式的定义也随之扩展。像 {1， 2， 3} 这样的集合可以被认为是与像 {a， b， c} 这样的集合“相等”的，因为有一种称为规范同构的隐式理解，它比较了群结构之间的相似性。

“这些集合以一种完全自然的方式相互匹配，数学家们意识到，如果我们也称它们相等，那将非常方便，”Buzzard说告诉新科学家亚历克斯·威尔金斯。

然而，将规范同构视为平等现在正在造成“一些真正的麻烦”，Buzzard写，对于试图使用计算机形式化证明（包括几十年前的基础概念）的数学家来说。

“到目前为止，没有一个（计算机）系统能捕捉到格罗滕迪克等数学家使用等号的方式，”Buzzard说告诉威尔金斯指的是亚历山大·格罗滕迪克（Alexander Grothendieck），他是20世纪的主要数学家，他依靠集合论来描述相等性。

一些数学家认为他们应该重新定义数学概念，以形式等同于具有相等性的规范同构。

Buzzard不同意。他认为，数学家和机器之间的不一致应该促使数学思维重新思考他们所说的数学概念到底是什么意思，因为数学概念是平等的基础，这样计算机就可以理解它们。

“当一个人被迫写下自己的真正含义，并且无法躲在这些定义不清的词语后面时，”巴扎德说写.“人们有时会发现自己必须做额外的工作，甚至重新思考某些想法应该如何呈现。”

该研究已发布在arXiv（阿尔希夫酒店）.

宝宝起名 起名