在数学中，有些概念相当模糊，难以理解，但我们以为已经掌握了“等于”的含义。然而，事实证明，数学家们实际上对什么构成两个事物相等存在分歧，这可能会给越来越多被用于检查数学证明的计算机程序带来一些头痛的问题。
这个学术争论已经持续了几十年，但因为用于“形式化”或检查证明的计算机程序需要明确、具体的指令，而不是依赖计算机没有的上下文的模糊定义，所以这个问题终于变得紧迫起来。
英国数学家凯文·巴扎德（Kevin Buzzard）在与计算机程序员合作时遇到了这个问题，这促使他重新审视“这个等于那个”的定义，以“挑战关于平等的各种合理听起来的口号”。
“六年前，”巴扎德在他发布到arXiv上的预印本中写道，“我以为我理解了数学上的平等。我以为这是一个定义明确的术语……然后我开始尝试在计算机定理证明器中做硕士级别的数学，我发现平等是一个比我想象中更棘手的概念。”
等号（=），其两条平行线优雅地代表了放置在两边的对象之间的平等关系，是由威尔士数学家罗伯特·雷科德（Robert Recorde）于1557年发明的。
最初它并没有流行起来，但随着时间的推移，雷科德那直观的符号取代了拉丁短语“aequalis”，并为计算机科学奠定了基础。发明后的整整400年，等号首次作为计算机编程语言的一部分，在1957年的FORTRAN I中使用。
然而，平等的概念有着更长的历史，至少可以追溯到古希腊。现代数学家在实践中也“相当宽松”地使用这个术语，巴扎德写道。
在常见用法中，等号设置了描述代表相同价值或意义的不同数学对象的方程，这可以通过一些替换和逻辑变换从一边到另一边来证明。例如，整数2可以描述一对对象，同样1 + 1也是。
但自19世纪末集合论出现以来，平等的第二个定义一直被数学家们使用。
集合论已经发展，与之一起，数学家对平等的定义也得到了扩展。像{1, 2, 3}这样的集合可以被认为与像{a, b, c}这样的集合‘相等’，因为存在一种称为规范同构（canonical isomorphism）的隐含理解，它比较群体结构之间的相似性。
“这些集合以一种完全自然的方式匹配，数学家们意识到，如果我们也称这些集合为相等，那将非常方便，”巴扎德告诉《新科学家》记者亚历克斯·威尔金斯（Alex Wilkins）。
然而，将规范同构视为平等现在正在给试图用计算机形式化证明的数学家——包括几十年前的基础概念——带来“一些真正的麻烦”，巴扎德写道。
“目前存在的[计算机]系统都没有捕捉到像格罗滕迪克那样使用等号的数学家们的方法，”巴扎德告诉威尔金斯，提到了20世纪依靠集合论描述平等的领先数学家亚历山大·格罗滕迪克（Alexander Grothendieck）。
一些数学家认为，他们应该重新定义数学概念，以正式将规范同构与平等等同起来。
巴扎德不同意。他认为，数学家与机器之间的不一致应促使数学头脑重新思考他们对像平等这样基础性的数学概念到底是什么意思，以便计算机能够理解它们。
“当一个人被迫写下自己实际意思并且不能躲在这些定义不清的词语背后时，”巴扎德写道。“有时会发现自己需要做额外的工作，甚至重新思考某些想法应该如何呈现。”这项研究已发布在arXiv上。