В экосистеме OpenMath математические доказательства формируются по принципу нарастающего фундамента. Всё начинается с базовых логических правил, арифметики Пеано и простейших операций, которые образуют так называемый «генезис-блок» знаний. Пользователь Алиса добавляет ключевые определения: биномиальные коэффициенты, операцию суммирования, понятие простоты числа и ряд вспомогательных утверждений. После автоматической проверки эти элементы навсегда сохраняются в блокчейне и становятся доступными для других участников.
Затем Боб расширяет базу, доказывая свойства функции суммирования, упрощающие дальнейшие вычисления. На этой основе Кэрол строит на блокчейне доказательство биномиальной теоремы, используя только ранее подтверждённые утверждения. Позже подключается Дейв: он добавляет важную лемму о делимости биномиального коэффициента на простое число, включая в процесс лемму Гаусса.
Имея все необходимые инструменты, сообщество формулирует «лемму первокурсника», а затем завершает построение, доказывая малую теорему Ферма.
по материалам
уникальность
