Prace matematyczne wymagają formalnej walidacji. Zwykle odbywa się to nieformalnie przez recenzenta. Ale co jeśli moglibyśmy polegać na czymś bardziej solidnym, jak automatyczna formalizacja w Lean 4, gdzie rola recenzenta zostałaby ograniczona do skrupulatnego sprawdzania sformułowań definicji i twierdzeń? Kompilacja automatycznie generowanego kodu stałaby się certyfikatem dowodu. To właśnie miało miejsce w dłuższym okresie, który przeprowadziłem z Arystotelesem przez @HarmonicMath. Dziękuję @PietroMonticone i @llllvvuu za pomoc w przygotowaniu planu. Tutaj przedstawiam kompletną poprawną automatyczną formalizację pracy mojego przyjaciela Stefana Barańczuka na temat ciągów podzielności Czebyszewa. Kod ma około 5000 linii wysoce nietrywialnego Lean. Poprawia wszystkie niespójności i luki w głównym artykule (nawet dowodząc niektórych delegowanych propozycji). Zamierzam opublikować serię takich eksperymentów, dowodząc, że w niektórych obszarach matematyki, w tym w elementarnej teorii liczb, kombinatoryce i analizie (wszystkie rodzaje rzeczy objęte przez Mathlib), nie jesteśmy daleko od masowej zmiany w dokumentacji ważności dowodów. Myślę, że to będzie intensywny rok!