AI доказало теорему, над которой математики бились 50 лет
Is mathematics about to enter the conservatory?
В тот же день, когда Claude завершил формализацию доказательства Великой теоремы Ферма в Lean, в arXiv появилась статья Ван и Ву из Hunan University, в которой с помощью AI доказана сферическая теорема Хадвигера — гипотеза, открытая с 1974 года. Авторы использовали OpenAI Codex для разработки деталей доказательства, поиска пробелов и оформления рукописи. Автор блога, сам пробовавший доказать эту теорему, размышляет о будущем математики: если компьютеры скоро докажут все сложные результаты, стоит ли продолжать поддерживать математиков как культурную ценность?
Эти инструменты затрудняют понимание того, верно ли сложное рассуждение, не говоря уже о том, кто заслуживает финансирования, постоянной должности и славы.