🎓 GPT-5.2 Pro решила задачу из списка Erdős
Математик Теренс Тао сообщил, что модель GPT-5.2 Pro смогла практически автономно решить задачу №728 из списка Erdős. В процессе использовался инструмент Aristotle для перевода доказательства на язык Lean, что позволило автоматически исправлять логические ошибки. Тао отмечает, что прорыв заключается не только в интеллекте, но и в невероятной скорости подготовки черновиков и перевода формальных доказательств в читаемые тексты.
🌍 Происходит «индустриализация» математики — сокращается время от нахождения идеи до публикации рукописи. ИИ становится мощным инструментом автоматизации рутинных аспектов доказательства и формализации кода.
👤 Математические исследования ускоряются. Несмотря на то, что ИИ пока справляется только с 1-2% открытых задач, его способность работать с языком Lean делает его незаменимым ассистентом для ученых.
Источник 1: https://the-decoder.com/terence-tao-says-gpt-5-2-pro-cracked-an-erdos-problem-but-warns-the-win-says-more-about-speed-than-difficulty/ Источник 2: https://twitter.com/OpenAI/status/2060451757818601808