Математические статьи нуждаются в формальной валидации. Обычно это делается неформально рецензентом. Но что если мы могли бы полагаться на что-то более надежное, например, автоформализацию в Lean 4, где роль рецензента была бы сведена к тщательной проверке формулировок определений и теорем? Компиляция автоматически сгенерированного кода станет сертификатом доказательства. Это произошло в более длительном эксперименте, который я провел с Аристотелем вместе с @HarmonicMath. Спасибо @PietroMonticone и @llllvvuu за помощь в настройке плана. Здесь я представляю полную корректную автоформализацию статьи моего друга Стефана Баранчука о последовательностях делимости Чебышёва. Код состоит из примерно 5000 строк высоконетривиального Lean. Он исправляет все несоответствия и пробелы в основной статье (даже доказывая некоторые делегированные предложения). Я собираюсь опубликовать серию таких экспериментов, доказывающих, что в некоторых областях математики, включая элементарную теорию чисел, комбинаторику и анализ (все виды тем, охватываемых Mathlib), мы не так далеки от массового сдвига в документации действительности доказательств. Я думаю, что это будет напряженный год!