В блоге Xena Project вышел программный текст за подписью семи человек: Джереми Авигад, Кевин Базард, Йоан Комелен, Реми Дежен, Ким Моррисон, Оливер Нэш и Адам Топаз. Они поддерживают массовую формализацию математики с помощью ИИ, но с жёсткой оговоркой. Результат нужен только тогда, когда им пользуются математики, а чистая корректность без читаемости и поддержки ничего не стоит. Их формулировка: «Плохая формализация существующих результатов хуже, чем никакой». Поводом для тревоги стали недавние громкие истории...