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