Конец эры человеческого превосходства: скоро будет представлено компьютерное доказательство теоремы Ферма

Передовые алгоритмы теперь расшифровывают то, что ранее было доступно только человеческому интеллекту. Математик преобразует революционное доказательство объемом в 100 страниц в компьютерный код, используя инструмент доказательства Lean, который позволяет превращать доказательства, написанные прозой, в правила и логику для тестирования. Кевин Баззард уже использует Lean и создает инструменты, помогающие студентам лучше изучать доказательства.

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

Теорема, предложенная французским математиком 17-го века Пьером де Ферма, утверждает, что нет трех положительных целых чисел a, b и c, которые удовлетворяли бы уравнению aⁿ + bⁿ = cⁿ для любого целочисленного значения n больше 2. Теорема оставалась недоказанной на протяжении сотен лет, пока в 1993 году английский математик Эндрю Уайлс не представил письменное доказательство объемом в 100 страниц. Уайлс стал известным именем, по крайней мере, в математических кругах.

Lean – это инструмент кодирования, созданный на основе языка C++, специально для помощи в кодификации и верификации доказательств по индукции. Британский математик Кевин Баззард провел годы, создавая инструменты в Lean, которые поддерживают всю программу обучения математике бакалавриата в Имперском колледже Лондона. Студенты могут видеть материал, обсуждаемый на занятиях, разбитый на функциональные шаги, использующие логику и математические операторы.

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

Баззард сообщил, что его цель состоит в том, чтобы помочь закодировать более сложные математические идеи, которые вдохновила Теорема Ферма. Столетиями люди разрабатывали целые, очень ценные новые области математики, пытаясь доказать эту теорему. Теперь превращение 100-страничного доказательства Уайлса в формальный язык и правила могут открыть поддержку компьютерных доказательств для новых поколений математиков.

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