Похлеще Навье-Стоксов: доказана иррациональность значения дзета-функции
(!)
Любопытно, стал искать подробности на понятном языке (
), влезла Алиса с утверждением, что я ошибаюсь, и иррациональность константы ещё не доказана. Я упомянул автора доказательства, Алиса поправилась, но выразила сомнение, что доказательство верное.
В качестве аргумента привела недавний случай, когда Рамана Кумар доказал с помощью ИИ, что гипотеза Коллатца неверна. И привёл доказательство на Lean.
Таким образом
был обнаружен баг в ядре Lean.
По идее, всякое последующее исправление ядра Lean должно инициировать проверку всех предшествующих "доказательств"?
