RW Space

В математике есть довольно туманные понятия, которые сложно уяснить себе, но мы думали, что мы рассмотрели значение слова «равно».

Оказывается, математики действительно могут это понять. Я не согласен с определением того, что делает две вещи равными, и это может вызвать некоторые головные боли у компьютерных программ, которые все чаще используются для проверки математических доказательств.

Эта академическая ссора кипит уже несколько десятилетий, но наконец-то дошло до апогея, поскольку компьютерные программы, используемые для «формализации» или проверки доказательств, должны иметь четкие и конкретные инструкции; недвусмысленные определения математических понятий, которые открыты для интерпретации или полагаются на контекст, которого нет у компьютеров.

Британский математик Кевин Баззард из Имперского колледжа Лондона столкнулся с этой проблемой при сотрудничестве с программистами, и это побудило его вернуться к определениям понятия «это равно тому», «бросить вызов различным разумно звучащим лозунгам о равенстве».

«Шесть лет назад», — пишет Баззард в своем препринте, размещенном на сервере arXiv, — « Я думал, что понимаю математическое равенство. Я думал, что это один четко определенный термин… Затем я начал пытаться получить степень магистра по математике в компьютерном средстве доказательства теорем и обнаружил, что равенство — это довольно сложная концепция, чем я себе представлял».

Знак равенства (=) с двумя параллельными линиями, элегантно обозначающий равенство между объектами, расположенными по обе стороны, был изобретен валлийским математиком Робертом Рекордом в 1557 году.

Он Поначалу это не прижилось, но со временем блестяще интуитивный символ Рекорда заменил латинскую фразу «aequalis» и позже заложил основу для информатики. Ровно через 400 лет после своего изобретения знак равенства был впервые использован как часть языка программирования FORTRAN I в 1957 году.

Однако концепция равенства имеет гораздо более длительную историю, восходящую к Древней Греции. по меньшей мере. А современные математики на практике используют этот термин «довольно широко», пишет Баззард.

При привычном использовании знак равенства устанавливает уравнения, которые описывают различные математические объекты, которые представляют одно и то же значение или значение, что-то, что можно доказать с помощью нескольких переключений и логических преобразований из стороны в сторону. Например, целое число 2 может описать пару объектов, как и 1 + 1.

Но второе определение равенства используется математиками с конца 19 века, когда появилась теория множеств. p>

Теория множеств развивалась, и вместе с ней расширилось и определение равенства математиков. Набор типа {1, 2, 3} можно считать «равным» набору типа {a, b, c} из-за неявного понимания, называемого каноническим изоморфизмом, который сравнивает сходство между структурами групп.

«Эти множества совпадают друг с другом совершенно естественным образом, и математики поняли, что было бы очень удобно, если бы мы просто называли их равными», — сказал Баззард Алексу Уилкинсу из New Scientist. .

Однако, как пишет Баззард, принятие канонического изоморфизма как равенства теперь вызывает «серьёзные проблемы», пишет Баззард, у математиков, пытающихся формализовать доказательства, включая основополагающие концепции десятилетней давности, с помощью компьютеров.

«Ни одна из существующих на данный момент [компьютерных] систем не отражает того, как математики, такие как Гротендик, используют символ равенства», — сказал Баззард Уилкинсу, имея в виду Александра Гротендика, ведущего математика 20-го века, который полагался на теорию множеств для описывают равенство.

Некоторые математики считают, что им следует просто переопределить математические концепции, чтобы формально приравнять канонический изоморфизм к равенству.

Баззард с этим не согласен. Он считает, что несоответствие между математиками и машинами должно побудить математические умы переосмыслить, что именно они означают под такими фундаментальными математическими понятиями, как равенство, чтобы компьютеры могли их понять.

«Когда человека заставляют записывать, что он на самом деле имеет в виду и не может спрятаться за такими неопределенными словами», — пишет Баззард. «Иногда приходится проделать дополнительную работу или даже переосмыслить, как следует представлять определенные идеи».

Исследование было опубликовано на arXiv.