Проект посвящён философскому анализу эпистемологических, онтологических и методологических аспектов современного теоретико-типового подхода к основаниям математики. Исследование указанных аспектов планируется осуществить через рассмотрение теоретико-типового понятия компьютерного доказательства. В последнее десятилетие активно развиваются теории типов (например, гомотопическая), применяемые в рамках оснований математики, и выстраиваются унивалентные основания математики. Последнее предполагает активное использование компьютерных доказательств математических результатов. Тем не менее теоретико-типовое понятие компьютерного доказательства обладает эпистемологическими характеристиками, отличающими его от более традиционного понятия компьютерного доказательства (например, доказательства методом перебора, использованного Апелем и Хакеном в их доказательстве теоремы о четырёх красках). Кроме того, теоретико-типовой подход и соответствующее ему понятие доказательства предполагают изменение понятия математического объекта и методологии математического исследования, что требуется своего философского анализа. В результате реализации предлагаемого Проекта будут сформулированы современные теоретико-типовые понятия математического доказательства и математического объекта, получены описание и объяснение практики современного математического исследования в рамках теоретико-типового подхода к основаниям математики, а также сформулированы методологические выводы для дальнейших математических исследований. В настоящее время методология современного математического исследования в контексте активной компьютеризации изучена весьма мало и требуется своего философского и междисциплинарного анализа, а также оказывается весьма актуальной в контексте возрастающей роли применения вычислительной техники и современных методов программирования для получения научных знаний в рамках различных научных дисциплин.