Как я "прочувствовал" доказательство гипотезы Конвея
Программист потратил месяц свободного времени на использование ИИ для доказательства открытой математической гипотезы Конвея, поставленной 50 лет назад. Результат — формальное доказательство в Lean, хотя и не проверенное независимо математиками.