Компьютерные доказательства и их понимание человеком: случай унивалентных оснований

Компьютерное доказательство теоремы о четырех красках, которое было впервые опубликовано Аппелем, Хакеном и Кохом в 1977-м году, спровоцировало продолжающуюся по сегодняшний день философскую дискуссию об эпистемической ценности компьютерных доказательств. В настоящей работе мы показываем, опираясь на поход предложенный в 2006 году Баслером, как унивалентные основания математики (УО) решают некоторые эпистемологические проблемы, которые ранее обсуждались в литературе в связи с компьютерными доказательствами, и тем самым сглаживают различия между компьютерными и традиционными математическими доказательствами. Мы иллюстрируем наши аргументы примером формализованной и компьютеризированной версии доказательства из области алгебраической топологии.