«=» - не просто знак: Кевин Баззард переосмысливает основы математики

В новом препринте , который больше напоминает редакционную статью или набор наблюдений, чем теорию или исследование, математик Кевин Баззард рассматривает простую идею из программирования, которая становится «более сложной» при переводе на язык математики: что на самом деле означает знак равенства? И что он не означает?

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

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

«Баззард обнаружил, что каждый студент на курсе программирования быстро усваивает: в кодировании существует несколько видов равенства, и для правильного кодирования необходимо полностью прорабатывать некоторые шаги, которые человеческий разум легко пропускает при выполнении математических операций. «Строка '2 + 2', введенная в компьютерную алгебраическую систему, не равна строке '4', выведенной системой; происходит некоторая обработка», – поясняет Баззард.

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

Важно помнить, что даже если что-то кажется незначительным, это не значит, что это не важно и не стоит обсуждения. Существует множество нюансов, связанных с этим вопросом: должен ли один и тот же знак равенства учитывать термины, округленные вверх или вниз? Означает ли знак равенства одинаковость, если между двумя сторонами проходит время (например, когда две курицы становятся тремя)?

Этот вопрос не касается переопределения чего-либо в математике — речь идет о точности и намерении.

Согласно Баззарду, значение знака равенства оставляет желать лучшего в аспекте «точности и намерения». В своей статье он описывает текущее состояние символа как «нестрогое». «На практике мы используем концепцию равенства довольно небрежно, полагаясь на некое глубокое интуитивное понимание, а не на логическую структуру, в которой, как мы считаем, мы работаем», — пишет он. В выбранной им программе проверки доказательств, известной как система Lean , шаги должны быть определены гораздо более точно.


В наших умах и в «умах» программируемых нами компьютеров происходит больше шагов за кулисами уравнений, чем это кажется на первый взгляд — все зависит от того, как мы их организуем. Некоторые языки программирования, известные как «сильно типизированные» языки, требуют указания типа переменной. Например, 'x' может быть целым числом, длинным десятичным числом или строкой символов, как пароль. Каждый из этих типов сохраняется вместе со значением переменной. Если попытаться выполнить математическую операцию или приравнять переменные разных типов, язык программирования этого не позволит.

В других языках (известных как «слабо типизированные»), а также в большинстве математических практик, «тип» является более контекстуальным понятием. Вместо проверки назначенного типа, язык проверяет, может ли содержимое переменной выполнить требуемую операцию. Например, при вычислении '2+2=4' строка '2+2' преобразуется в целое число 4, и только потом происходит сравнение целых чисел по обе стороны от знака равенства. Для человеческого интуитивного мышления это просто, но компьютерам требуются четкие инструкции.

Проект Lean ставит цель преобразовывать математические доказательства в алгоритмические шаги для компьютера. Баззард приводит пример математика Александра Гротендика , который использовал «слаботипизированную» математику, комбинируя разные дисциплины. Гротендик ввел новый термин «канонически изоморфный» как новый вид равенства, что вызвало бы ошибку в Lean, поскольку он использует = и ≅ ( знак конгруэнтности ) для разных целей.

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

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