Сейчас делается много работ об автоматизированном доказательстве теорем, это одно из основных направлений ИИ в науке. Мы тоже внесли свой вклад — сделали LongTails для исследований в математической оптимизации. Уже получили более 35 новых результатов, включая существенные улучшения известных оценок сложности. Это задачи, которыми занимается большое сообщество и по которым регулярно выходят статьи. Методы оптимизации лежат в основе обучения любых нейросетей. Более эффективные алгоритмы сокращают время обучения, вычислительные затраты и энергопотребление дата-центров. Они помогают проектировать прочные и лёгкие конструкции, строить маршруты доставки, распределять нагрузку в электросетях, искать новые молекулы и материалы, обрабатывать физические эксперименты и управлять инвестиционными рисками. Все доказательства формально проверены в Lean 4. Идея в том, чтобы объяснить Lean 4 и нейронке базовую теорию, а дальше она уже либо сама ищет решение, либо использует эволюционные фреймворки. Отличная работа Саши Тюрина. Выложили код и результаты в открытый доступ, рекомендую посмотреть, потому что так мы можем покрыть целую область науки :) Сайт: https://k3nfalt.github.io/longtails/ GitHub: https://github.com/k3nfalt/longtails/