數學家揭示“等于”在數學中具有多種含義

有一些漂亮的模糊的概念在數學中，這可能很難理解，但“等于”的含義是我們認為我們已經涵蓋的含義。

事實證明，數學家實際上無法就兩個事物相等的定義達成一致，這可能會給越來越多地用于檢查數學證明的計算機程序帶來一些麻煩。

這場學術爭吵已經持續了幾十年，但最終達到了頂峰，因為用于“形式化”或檢查證明的計算機程序需要有明確、具體的指令;不是對數學概念的模棱兩可的定義，這些概念可以解釋或依賴于計算機所沒有的上下文。

倫敦帝國理工學院的英國數學家凱文·巴扎德（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（阿爾希夫酒店）.

寶寶起名 起名