113 подписчиков
В Lean'е формализовали (то есть записали математическое доказательство, строгость которого проверена):
• теорему Ферма для регулярных простых (Куммер, 1847)
• основную теорему арифметики, основную теорему алгебры, основную теорему анализа
• выворачивание сферы наизнанку (Смейл, 1957)
• независимость континуум-гипотезы от ZFC (Гёдель, 1940 + Коэн, 1963)
• всякие абстрактные понятия, введенные Шольце (перфектоиды, жидкие векторные пространства...)
- некоторые свежие результаты аддитивной комбинаторики
• довольно много фундаментальной математики
картинка:
А из "ста великих теорем" на данный момент формализованы (хотя бы в одном из proof assistant'ов) все, кроме теоремы Ферма:
Около минуты
14 марта 2024