Я «вайбнул» доказательство гипотезы Конвея
I Vibed a Proof of Conway's Conjecture
Даниэль Абрамов (gaearon) за месяц и огромное количество токенов получил Lean-доказательство гипотезы уточнения Конвея об омнифических целых — последней нерешённой гипотезы Конвея о сюрреальных числах. Доказательство прошло механические проверки Palomar, но пока не подтверждено математиками. В статье он рассказывает, как выбирал задачу, почему первые попытки с Claude утонули в «словесном салате» и как переключение на скептичный ChatGPT изменило подход.
Я подумал, что идея «решить» математическую задачу, не понимая её сути, довольно абсурдна, и именно поэтому она показалась мне ещё более привлекательной.