Практика компьютерных доказательств и человеческое понимание: эпистемологическая проблематика

В последние десятилетия в математике особую остроту приобрели эпистемологические проблемы, связанные со слишком большой длиной доказательства важных математических результатов, а также с большим и постоянно возрастающим количеством публикаций по математике. Предполагается, что эти затруднения могут быть разрешены (хотя бы частично) путем обращения к компьютерным доказательствам. Однако и компьютерные доказательства оказываются проблематичными с эпистемологической точки зрения. И относительно доказательств в обычной (неформальной) математике, и относительно компьютерных доказательств в равной степени актуальна проблема их обозримости. Исходя из традиционного понимания доказательства оно обязательно должно быть обозримым, иначе оно не будет достигать своей основной цели - формирования убежденности в правильности доказываемого математического результата. Около 15 лет назад начал развиваться новый подход к основаниям математики, сочетающий в себе конструктивистские, структуралистские черты и ряд преимуществ классического подхода к математике. Этот подход выстраивается на основе гомотопической теории типов и носит название унивалентных оснований математики. Благодаря мощному понятию равенства этот подход позволяет значительно сократить длину формализованных доказательств, что намечает путь к разрешению возникших эпистемологических затруднений.