Посмотрел, на что реально тут способна эта ваша хвалёная mathlib из лина4.
Во-первых сама оригинальная статья "Birational Invariants from Hodge Structures and Quantum Multiplication": Концевич особо отмечает, что "In particular, we prove that a very general cubic fourfold is not rational", а QuantaMagazine зацепился конкретно за это "частичное", потому что упоминается теория струн ("String Theory Inspires a Brilliant, Baffling New Math Proof").
Всюду один хайп :)

Во-вторых оказывается что mathlib, которая уже якобы охватывает едва ли нет всю базовую математику, по сути лишь один хилый колосочек в бескрайнем непаханом поле. В этой либе нету формализации ни квантовой когомологии (Громов-Виттен), ни спектралок для F-bundles (да и их самих), ни изоморфизма Нётера-Лефшица, да даже групп Ходжа...

Надо ручками запилить отдельную микро-теорию атомов, на ней определить факторизацию бирациональных отображений, и что для "very general cubic fourfold" существует "плохой атом", и дофига чего другого, чтобы только подобраться к оригинальной теореме.

=

А тем временем веб-версия Lean4, ещё пару месяцев назад работавшая, теперь из России доступна только через винни-пуха. И это не просто на уровне сайта -- стоит его отключить, как тут же контейнер в консоли блокируется. Потому что эти темы сегодня развивает прежде всего академическая Европа, из которых нас выпиливают медленно, но верно.

А я говорил: надо миллиарды сливать не на "свой приставка" и "свой игровой движок", а вкладываться в наукоёмкие темки вроде своего теорем-прувера. Отдача неимоверная! Надо не ЦОДы строить, а развивать алгоритмы и математику дивного нового будущего.

Но при этом в России выделен триллион(!) на искусственный идиотизм. Ёлки, ну дайте МИАН хотя бы один миллиард из этой суммы (это всего 0.1%!), и они сделают пруф-ассистант мирового уровня, который порвёт все эти лины агды коки! Это абсолютно прорывная темка не только в мировой математике, но скоро будет и в AI (вся формальная верификация), отвечаю!!1

Филдсовский лауреат Теренс Тао сегодня дико по этим темкам упарывается, теорем-пруверы (недоступные из России) аццки качает среди математиков. Были бы у меня деньги, я бы только этим и занимался.

А как будет? Никак не будет и ничего не будет :) Попилят триллион на мусорных нейротемках с околонулевым выхлопом, и всё (личное мнение :) ничего не утверждаю).

-- Ну, а что делать (с) Косинец.