Операция выполнена!
Закрыть
info@vsetut.pro
Стать автором
Вернуться

[Перевод] Проект Lean: Можно ли формализовать всю математику на компьютере – и нужно ли?

26.06.2026 09:36:59 | Хабр
Хабы: Блог компании FirstVDS, Научно-популярное, Математика, Функциональное программирование

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

Начиная с 1960-х годов исследователи разрабатывают компьютерные программы, называемые системами интерактивного доказательства. Используя такую систему, математик записывает каждую строку доказательства (включая каждое определение) на языке, понятном компьютеру, а затем система проверяет логику. Если хотя бы один шаг не вытекает из предыдущего — если не доказана каждая мелочь вплоть до того, что 1 + 1 = 2, — программа не примет доказательство.

Сейчас учёные надеются формализовать всю математику с помощью системы интерактивного доказательства под названием Lean. Уже создана библиотека, содержащая более 120 000 определений, и проверено четверть миллиона теорем. Несколько математиков поддерживают эту базу данных, обновляя её и проверяя новые данные. (Некоторые из них занимаются этой работой полный рабочий день.) Они уже получили более 10 миллионов долларов финансирования, в основном от миллиардера-финансиста Алекса Герко.

Читать далее
Подробнее
Читайте также
НОВОСТИ

ВСЕ НОВОСТИ
ПИШИТЕ

Техническая поддержка проекта ВсеТут

info@vsetut.pro

Copyright © 2026 - vsetut.pro