>>119009
Знает ли религиозный даун, что гомотопическая теория типов (HoTT) сейчас зачинает постепенно заменять старую аксиоматику? Это один из самых мощных современных конкурентов старой ZFC. Это объединение топологии, теории типов и теории категорий, с более естественным фундаментом для современной абстрактной математики. ZFC неконструктивна. Невычислимая. Она говорит, что объект существует, но не дает алгоритма, как его построить (особенно из-за аксиомы выбора). Для программирования и автоматической проверки доказательств гораздо актуальнее Теория типов (как в языке Coq или Lean например). А тупое уебище христанутое гонит фуфлыгу, будто бы какие-то математические жрецы не дают менять аксиомы. Вот же даун!