Математик Теренс Тао сообщил о значимом успехе в применении искусственного интеллекта для решения математических задач. ChatGPT смог решить задачу №728 из списка Эрдёша “почти автономно”, ограничившись минимальной обратной связью и не используя готовые решения. Это отличие от предыдущих случаев, когда ИИ просто находил уже существовавшие решения с помощью поиска в литературе. На этот раз GPT-5.2 Pro от OpenAI сгенерировал доказательство ужесточенной версии задачи, а другой инструмент — Aristotle — автоматически перевел это доказательство в формальный язык Lean для проверки корректности. В процедуре были незначительные ошибки, которые Aristotle автоматически исправил. По словам Тао, главное отличие — скорость подготовки… Подробнее
GPT-5.2 Pro решает задачу Эрдёша: мнение Терренса Тао
16 января16 янв
~1 мин