Математики не могут прийти к единому мнению о том, что означает «равно».

Что означает «равно»? Для математиков у этого простого вопроса есть несколько ответов, и это создаёт проблемы при использовании компьютеров для проверки доказательств. Возможно, решение заключается в том, чтобы пересмотреть основы математики

Когда вы видите «2 + 2 = 4», что означает знак «=»? Оказывается, это сложный вопрос, потому что математики не могут прийти к единому мнению о том, что делает две величины равными.

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

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

Первое определение равенства вам знакомо. Большинство математиков считают, что каждая сторона уравнения представляет собой один и тот же математический объект, что можно доказать с помощью ряда логических преобразований, переходящих от одной стороны к другой. Хотя знак равенства появился только в XVI веке, само понятие равенства уходит корнями в глубокую древность.

Всё начало меняться в конце XIX века с развитием теории множеств, которая обеспечивает логическую основу для большей части современной математики. Теория множеств имеет дело с коллекциями, или множествами, математических объектов и предлагает другое определение равенства: если два множества содержат одинаковые элементы, то они равны, как и в первоначальном математическом определении. Например, множества {1, 2, 3} и {3, 2, 1} равны, потому что порядок элементов в множестве не имеет значения.

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

Чтобы понять почему, возьмём множества {1, 2, 3} и {a, b, c}. Очевидно, что элементы каждого множества различны, поэтому множества не равны. Но между этими двумя множествами можно установить соответствие, отождествив каждую букву с числом. Математики называют это изоморфизмом. В данном случае существует несколько изоморфизмов, потому что у вас есть выбор, какое число присвоить каждой букве, но во многих случаях есть только один очевидный выбор, который называется каноническим изоморфизмом.

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

Наличие двух определений равенства не вызывает особого беспокойства у математиков, когда они пишут статьи или читают лекции, поскольку смысл всегда ясен из контекста. Однако это создаёт проблемы для компьютерных программ, которым нужны строгие и чёткие инструкции, говорит Крис Биркбек из Университета Восточной Англии, Великобритания. «Мы понимаем, что всё это время были немного небрежны и, возможно, нам стоит кое-что исправить».

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

В частности, работу Александра Гротендика, одного из ведущих математиков XX века, в настоящее время крайне сложно формализовать. «Ни одна из существующих систем не отражает того, как математики вроде Гротендика используют знак равенства», — говорит Баззард.

Проблема уходит корнями в то, как математики выстраивают доказательства. Чтобы начать что-то доказывать, нужно сначала сделать допущения, называемые аксиомами, которые принимаются за истину без доказательств и служат логической основой для построения доказательств. С начала XXго века математики остановились на наборе аксиом в рамках теории множеств, которые обеспечивают прочную основу. Это значит, что им, как правило, не нужно напрямую использовать аксиомы в своей повседневной работе, потому что можно предположить, что стандартные инструменты работают правильно. Точно так же вы, скорее всего, не задумываетесь о том, как устроена ваша кухня, прежде чем приступить к приготовлению блюда.

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

Чтобы решить эту проблему, некоторые математики предлагают переосмыслить основы математики и сделать так, чтобы канонические изоморфизмы и равенство считались одним и тем же. Тогда мы сможем заставить компьютерные программы работать с этим. «Изоморфизм — это равенство, — говорит Торстен Альтенкирх из Ноттингемского университета, Великобритания. — Я имею в виду, а что ещё? Если вы не можете отличить два изоморфных объекта, что это ещё может быть? Как ещё можно назвать это соотношение?»

В математической области под названием «теория гомотопических типов», в которой традиционное равенство и канонический изоморфизм определяются одинаково, уже предпринимаются попытки сделать это. По словам Альтенкирха, вместо того чтобы пытаться адаптировать существующие системы доказательства под канонический изоморфизм, математикам следует принять теорию типов и использовать альтернативные системы доказательства, которые работают напрямую с теорией типов.

Канюк не является поклонником этого предложения, поскольку уже потратил значительные усилия, используя современные инструменты для формализации математических доказательств, необходимых для проверки более сложных работ, таких как доказательство последней теоремы Ферма. Аксиомы математики следует оставить такими, какие они есть, вместо того, чтобы принимать теорию типов, а вместо этого следует доработать существующие системы, говорит он. “Вероятно, способ исправить это - просто оставить математиков такими, какие они есть”, - говорит Баззард. “Математиков очень трудно изменить. Вы должны усовершенствовать компьютерные системы