ИИ-модель OpenAI Astra решила 10 открытых задач математики и продемонстрировала новый метод доказательства теорем
Компания OpenAI представила результаты работы своей модели Astra. ИИ-модель разрешила сразу десять открытых проблем фундаментальной математики и теоретической информатики. Модель представила полноценные доказательства, автоматически проверенные с помощью формального верификатора Lean. Научный мир впервые столкнулся с прецедентом, когда нейросеть берет на себя трудную рутину доказательств, оставляя человеку постановку задач, интерпретацию методов и анализ результатов.
Предвидение Владимира Воеводского. Лауреат Филдсовской премии Владимир Воеводский еще в 2000-х годах осознал кризис в математике. Он пришел к выводу, что сложность математических доказательств превысила возможности человека. Воеводский посвятил много лет исследованиям, которые позволяют формализовать доказательства на языке Coq, и машины избавят ученых от рутинной проверки ошибок. Но проблема была в написании формальных программ на Coq, это оказалось очень трудным делом. Воеводский предсказал переход к компьютерной верификации. Сегодня его мечта сбывается: место Coq занял Lean, а сами программы пишет ИИ, который берет на себя роль помощника математика. Сам Воеводский, к сожалению, до реализации своих идей не дожил.