Блог
φ² + 1/φ² = 3 — тождество, на котором стоит вся арифметика проекта. Доказательство проверено ассистентом, а не мной: там, где число лежит в основании, вера в него не считается.
Число φ = (1 + √5)/2 удовлетворяет φ² = φ + 1. Отсюда одной строкой следует тождество, которое в этом проекте встречается чаще любого другого:
φ² + 1/φ² = 3Проверить его на бумаге — минута. Именно поэтому оно и опасно: утверждение, проверяемое за минуту, проверяют один раз, а цитируют годами.
Я не сомневался в тождестве. Сомнение было не в нём, а в том, что я ни разу не проверял его после того, как впервые записал, — и не смог бы назвать день, когда проверял.
Там, где число лежит в основании, «я в этом уверен» не является измерением. Уверенность — свойство меня, а не числа.
Доказательство записано в Lean и принято ассистентом. Разница с бумагой не в строгости вывода, а в том, что теперь есть артефакт, который можно перезапустить, — и он ответит без моего участия.
Ассистент проверяет, что доказательство доказывает записанное утверждение. Что записанное утверждение — то самое, которое нужно, читает человек, и здесь машина не помощник.
Кроме того, тождество точно в Z[φ] — кольце, где φ представлено символом, а не приближением. В любом формате с плавающей точкой оно выполняется приближённо, и величина расхождения есть свойство формата.
Точное тождество и его численная реализация — два разных утверждения. Машинная проверка первого ничего не говорит о втором.
Основание проекта стоит проверить формально ровно потому, что оно кажется слишком простым для проверки. Сложное перепроверяют из осторожности; простое не перепроверяет никто, и потому именно там ошибка живёт дольше всего.
Каждая цифра выше измерена, и рядом с ней названы её пределы.