Рубрика «автоматическое доказательство»

Компьютерное доказательство теории конденсированной математики — первый шаг к «великому объединению» - 1
Пример расчётного доказательства в программе Lean

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

Теперь вспомогательный софт для доказательства теорем (proof assistant software) не просто проверяет доказательства, но помогает выйти на принципиально новый уровень великого объединения разных математических разделов. Концепция «конденсированной математики» обещает принести новые идеи и связи между областями, начиная от геометрии и заканчивая теорией чисел. Это в своём роде «великое объединение» математики
Читать полностью »


https://ajax.googleapis.com/ajax/libs/jquery/3.4.1/jquery.min.js