数学家Kevin Buzzard发现“等于”的定义在数学界并不统一，这对计算机验证数学证明造成了困扰。

数学中有些概念相当模糊难懂，但“等于”的意义似乎是我们已经掌握的。然而，数学家们实际上并不完全同意什么构成两个事物的相等，这可能会对日益使用的计算机验证数学证明造成困扰。

这个学术争议已经持续了几十年，但现在终于被提上日程，因为用于“形式化”或验证证明的计算机程序需要明确的、具体的指令，而不是模棱两可的数学概念定义，这些概念定义在计算机缺乏的背景下容易被误解。

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

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

等号(=)由威尔士数学家Robert Recorde于1557年发明，它优雅地用两条平行线表示放在两边的对象之间的对等关系。最初它并没有流行起来，但随着时间的推移，Recorde的直观符号取代了拉丁词组“aequalis”，并为计算机科学奠定了基础。在其发明后的整整400年，等号首次作为计算机编程语言FORTRAN I的一部分被使用。

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

在熟悉的用法中，等号建立了描述不同数学对象代表相同价值或意义的方程，可以通过一些转换和逻辑变换来证明。例如，整数2可以描述一对对象，1 + 1也可以。

但自19世纪末以来，数学家们使用了第二种平等定义，那时集合论出现了。

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

Buzzard告诉《新科学家》的Alex Wilkins：“这些集合以完全自然的方式相互匹配，数学家们意识到，如果我们也称这些为相等会非常方便。”

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

Buzzard告诉Wilkins：“目前存在的任何[计算机]系统都无法捕捉像Grothendieck这样的数学家使用等号的方式，”他指的是20世纪依靠集合论描述平等的领先数学家Alexander Grothendieck。

一些数学家认为他们应该重新定义数学概念，以正式将规范同构等同于平等。

Buzzard不同意。他认为数学家与机器之间的不一致应该促使数学家重新思考他们对像平等这样基础的数学概念的确切定义，以便计算机能够理解它们。

Buzzard写道：“当一个人被迫写下自己的真实意思，不能躲在那些定义不清的词语背后时，有时会发现自己需要做更多的工作，甚至重新思考某些想法应该如何呈现。”

本文译自 ScienceAlert，由 BALI 编辑发布。

PREV : 越南三条海底互联网光缆中断
NEXT : 塑料回收产业是一场骗局