Простой символ, который мы знали всегда, может быть в корне ошибочным.
Математики иногда играют быстро и свободно с понятием равенства. В программировании знаки равенства могут означать разные вещи, а переменные имеют разные типы. Превращение интуитивного математического опыта в пошаговые закодированные доказательства требует заполнения некоторых «дыр».
В новом препринте, который не рецензируется и представляет собой скорее редакционную статью или набор наблюдений, чем теорию или исследование, математик Кевин Баззард пытается разобраться с идеей кодирования, которая становится сложной при переводе на математический язык. Что на самом деле означает знак равенства? А что он не значит?
Баззард стал известен благодаря своим попыткам превратить классические математические доказательства в код, который может быть проверен компьютером, включая Великую теорему Ферма. Для него мир компьютерных кодов преподносит сюрпризы.
«Шесть лет назад я думал, что понял математическое равенство», — написал Баззард. «Я думал, что это один четко определенный термин. Затем я начал изучать математическое доказательство в компьютерной среде и обнаружил, что равенство — гораздо более сложная концепция, чем я предполагал».
Баззард научился тому, что каждый студент программирования узнает довольно быстро: в программировании существуют разные виды равенства, и нужно проработать некоторые шаги, которые человеческий разум легко пропускает при выполнении математических вычислений, чтобы правильно кодировать.
Математика и программирование требуют больше точности и намерения. Баззард считает, что значение знака равенства оставляет желать лучшего в плане «точности и целенаправленности». Он описывает текущее состояние символа как «свободное». В программном обеспечении для проверки доказательств, таком как система Lean, шаги должны определяться гораздо более дискретно.
Некоторые языки программирования требуют указания типа переменной. Если попытаться выполнить математическую операцию с переменными разных типов, язык программирования этого не позволит. В математике «тип» переменной более контекстуален, и система проверяет, может ли содержимое переменной решить задаваемый математический вопрос.
Машины, которые мы используем для решения сложных задач, требуют больше направления, чем гибкий человеческий разум. Проект Баззарда заключается в превращении математических доказательств в алгоритмические шаги, необходимые для их кодирования на компьютере.
Пример Гротендика
Баззард использует математика Александра Гротендика как пример. Гротендик был выдающимся математиком, который внедрил множество основополагающих идей в алгебраической геометрии. Он часто использовал «свободно типизированную» математику. В программном обеспечении Lean такой подход вызвал бы ошибки, поскольку система требует более четкого определения понятий равенства.
Если математика хочет быть формализованной — то есть преобразованной в пошаговые доказательства, представленные кодом, — необходимо устранить многие пропуски и «дыры». Превращение этих пробелов в код поможет создать более точные и надежные математические библиотеки. В долгосрочной перспективе это может улучшить математику, делая доказательства более доступными и понятными.
Баззард хочет начать закладывать основу для этого. «Один полезный трюк — злоупотреблять символом равенства, заставляя его означать то, чего он не означает», — объяснил Баззард.
С ростом объема математических доказательств и их сложности становится все важнее иметь уверенность в том, что означает равенство.
Точность в математике
Баззард утверждает, что точность и однозначность в математике становятся всё более критичными, особенно когда мы говорим о доказательствах, объём которых может превышать сотни страниц. Для понимания и проверки таких доказательств необходимо иметь чёткие и понятные определения, что не всегда возможно при использовании традиционного символа равенства.
Кодирование математических доказательств
Проект Баззарда по кодированию математических доказательств направлен на устранение неоднозначностей и обеспечение более высокого уровня точности. Это требует преобразования интуитивно понятных математических идей в пошаговые алгоритмы, которые могут быть проверены с помощью компьютера. Это также включает в себя детализированное описание всех промежуточных шагов и этапов, которые человеческий разум может легко пропустить, но которые критически важны для компьютерных систем.
Проблема типизации
В программировании типизация переменных играет ключевую роль. Строго типизированные языки программирования требуют точного указания типа каждой переменной, будь то целое число, строка или что-то другое. Это позволяет избежать ошибок и неоднозначностей при выполнении операций. В математике же часто используется более свободный подход, где тип переменной определяется контекстом. Баззард указывает на необходимость большей строгости и точности в определении типов и операций для обеспечения корректности математических доказательств.
Взгляд в будущее
Баззард и его коллеги работают над созданием библиотек и инструментов, которые помогут математикам преобразовывать свои доказательства в код. Это требует значительных усилий, но в долгосрочной перспективе может значительно повысить надёжность и точность математических исследований. Баззард подчёркивает, что такая работа не только не упрощает математику, но и делает её более точной и понятной для всех, кто с ней работает.
Как указывает Баззард, один из способов достижения этой цели — это более строгое определение и использование символа равенства. Злоупотребление этим символом, как это делалось в прошлом, приводит к недоразумениям и ошибкам. С ростом сложности и объёма математических доказательств важно иметь чёткое и однозначное понимание всех используемых понятий и символов.
Таким образом, работа по формализации математики и преобразованию её в пошаговые доказательства, проверяемые компьютерами, может существенно повысить её точность и надёжность. Это особенно важно в контексте современных математических исследований, которые становятся всё более сложными и объёмными. Баззард и его команда продолжают работать над созданием инструментов и методов, которые помогут достигнуть этой цели и улучшить понимание и применение математики в будущем.
Это они ещё с нолём не разбирались. Там тоже фигурирует знак равно.
Ноль обозначает "ничто", и умножать на "ничто" лишено всякого смысла.