🤖 Модель OpenAI решила десять открытых математических задач

Компания OpenAI представила доказательства для десяти математических задач, остававшихся нерешенными с 2016 года. Эти достижения были получены моделью Astra, которая является частью новых разработок OpenAI. Все доказательства были формализованы в языке Lean и выложены в открытый доступ. Среди основных результатов — доказательство существования несофических групп и опровержение гипотезы жесткости Конна. Однако модель не смогла решить "задачи тысячелетия" Математического института Клэя.