Как сделать формализацию математики пригодной для новых исследований

🧮 Большую часть математики можно формализовать за три года. Но что мы получим на выходе? Такую перспективу описывают Кевин Баззард, Джереми Авигад и другие математики в блоге Xena. Формализовать - значит перевести определения, теоремы и доказательства на язык вроде Lean, чтобы компьютер мог проверять логические шаги. Авторы видят в ИИ возможность резко ускорить эту работу. Но предупреждают: миллионы строк проверенного кода могут оказаться бесполезными, если на них невозможно строить новые исследования. Нужны понятные определения, документация, совместимость библиотек и повторное использование результатов. Уже есть два подхода: • Tau Ceti - единая библиотека: математики задают план, ИИ пишет код, другие ИИ проверяют. • Formal Frontier - система агентов, превращающая математические тексты в связанные формальные библиотеки. Компьютерная проверка доказывает корректность формального утверждения. Ценность для науки появляется, когда результат можно понять, исследовать и использовать дальше. 📖 https://xenaproject.wordpress.com/2026/10/16/how-to-formalize-all-of-mathematics/