OpenAI выложила на GitHub 722 рукописи по математике, которые написала её внутренняя мо...
OpenAI выложила на GitHub 722 рукописи по математике, которые написала её внутренняя модель. Они собраны в 372 семейства результатов, модели дали около четырёх тысяч задач, средний результат стоил примерно трёх часов размышлений в режиме ChatGPT Pro. Саму модель не выпустили. Цифры громкие, но главное в новости одно слово: Lean. У многих рукописей есть версия на нём, а про те, у которых нет, OpenAI прямо пишет, что там могут быть ошибки. Небольшая справка для тех, кто не в теме, что такое Lean. Это язык, на котором доказательство записывается как программа, и проверяет его не рецензент, а компьютер. Сошлось - доказано, не сошлось - нет, без «ну вроде логично». Грубо говоря, калькулятор для доказательств: ему всё равно, кто автор, человек или модель. Отсюда и разница. Где проверяет человек, всё упирается в людей: arXiv уже ввёл лимит две статьи в месяц, рецензенты тонут. Где проверяет программа, лимита нет: 722, и будет больше. У меня в проектах то же самое в миниатюре. Пока «готово» проверял я глазами, агент делал ровно столько, сколько я успевал принять. Когда появились проверки, которые гоняются кодом, задач за день стало в разы больше, а глазами я смотрю только то, где проверки нет. https://openai.com/index/sharing-ai-progress-in-mathematics/ Вопрос на подумать - что в вашей работе можно проверить программой, а что пока только глазами?)