ИНТЕРАКТИВНОЕ ДОКАЗАТЕЛЬСТО: ВЕРИФИКАЦИЯ И ГЕНЕРИРОВАНИЕ НОВОГО МАТЕМАТИЧЕСКОГО ЗНАНИЯ
А.В. Хлебалин
Института философии и права СО РАН, 630090, г. Новосибирск, ул. Николаева, 8
sasha_khl@mail.ru
Ключевые слова: компьютерное доказательство, автоматизированные системы верификации в математике, гомотопная теория типов, доказательство, вычисление, computer-assisted proof, automate verification systems in mathematics, homotopy type theory, proof, calculation
Страницы: 87-95
Аннотация
В статье рассматриваются классические вопросы эпистемологии математики в связи с применением компьютерных систем в математическом исследовании. Показано, что зачастую проблемы эпистемологической характеристики математических результатов, полученных с помощью компьютера, связаны с непроясненностью содержания традиционных концепций эпистемологии математики, таких как доказательство, вычисление, истины и верификация. На примере характеристики логико-теоретических оснований интерактивных компьютерных систем, созданных на базе теории типов, демонстрируется их потенциал в области экспликации традиционных концепций эпистемологии математики.
DOI: 10.15372/PS20200105 |
