Математическое сообщество активно переводит терабайты существующих аналогов на язык Lean (проект Lean Mathematical Library). Это необходимо, так как в наше время электронные доказательства стали огромными (тысячи страниц), что живые рецензенты физически не могут проверить их наличие на скрытых ошибках. Нейросети обучаются на этих формализованных базах данных. Теперь ИИ может не просто проверять готовый код математика, но и самостоятельно заполнять «пробелы» в сложных доказательствах, автоматически просчитывая рутинные промежуточные леммы.

ИИ как генератор новых открытий (DeepMind и AlphaGeometry)

Долгое время считалось, что ИИ не способен на математическое творчество. Однако передовые AlphaGeometry и AlphaProof: Системы от DeepMind научились решать сложнейшие геометрические и алгебраические задачи уровня.

Люди, чья работа заключалась в рутинных вычислениях, решении стандартных дифференциальных уравнений или переборе известных математических моделей, полностью замещаются софтом (Wolfram Alpha, специализированные LLM).