Matematiske artikler trenger formell validering. Dette gjøres vanligvis uformelt av en dommer. Men hva om vi kunne stole på noe mer robust som auto-formalisering til Lean 4, hvor dommerens rolle reduseres til nøye kontroll av formuleringene av definisjonene og teoremene? Kompilering av automatisk generert kode ville bli et bevissertifikat. Dette skjedde i en lengre periode, som jeg gjorde med Aristoteles av @HarmonicMath. Takk til @PietroMonticone og @llllvvuu for hjelpen med oppsettet av blueprinten. Her presenterer jeg en fullstendig korrekt autoformalisering av en artikkel av min venn Stefan Barańczuk om Chebyshev-delbarhetssekvenser. Koden består av omtrent 5000 linjer med svært ikke-triviell Lean. Den retter opp alle inkonsistenser og hull i hovedartikkelen (og beviser til og med noen delegerte påstander). Jeg skal legge ut en serie slike eksperimenter som beviser at i noen områder av matematikken, inkludert elementær tallteori, kombinatorikk og analyse (alle slags ting dekkes av Mathlib), er vi ikke langt unna et massivt skifte i dokumentasjon av gyldigheten av bevis. Jeg tror dette kommer til å bli et hektisk år!