Matematické práce potřebují formální ověření. Obvykle to dělá neformálně rozhodčí. Ale co kdybychom se mohli spolehnout na něco robustnějšího, například automatickou formalizaci do Lean 4, kde by role recenzenta byla redukována na pečlivé ověřování formulací definic a vět? Kompilace automaticky generovaného kódu se stala důkazním certifikátem. To se stalo v delším období, které jsem udělal s Aristotelem do @HarmonicMath. Díky @PietroMonticone a @llllvvuu za pomoc s nastavením plánu. Zde předkládám úplně správnou autoformalizaci článku mého přítele Stefana Barańczuka o Čebyševových sekvencích dělitelnosti. Kód má asi 5000 řádků vysoce netriviálního Lean. Opravuje všechny nesrovnalosti a mezery v hlavním článku (dokonce dokazuje některé delegované tvrzení). Chystám se zveřejnit sérii takových experimentů, které dokazují, že v některých oblastech matematiky, včetně elementární teorie čísel, kombinatoriky a analýzy (všelijaké věci pokrývá Mathlib), nejsme daleko od masivního posunu v dokumentaci platnosti důkazů. Myslím, že to bude hektický rok!