Matematiska artiklar behöver formell validering. Detta görs vanligtvis informellt av en domare. Men tänk om vi kunde förlita oss på något mer robust som autoformalisering till Lean 4 där granskarens roll skulle reduceras till noggrann kontroll av formuleringarna av definitioner och satser? Kompilering av automatiskt genererad kod skulle bli ett beviscertifikat. Det här var vad som hände i en längre period som jag gjorde med Aristoteles av @HarmonicMath. Tack till @PietroMonticone och @llllvvuu för hjälpen med installationen av ritningen. Här presenterar jag en fullständig korrekt autoformalisering av en artikel av min vän Stefan Barańczuk om Chebyshevs delbarhetssekvenser. Koden består av cirka 5000 rader av mycket icke-trivial Lean. Den rättar till alla inkonsekvenser och luckor i huvudartikeln (och bevisar till och med vissa delegerade påståenden). Jag kommer att publicera en serie sådana experiment som visar att inom vissa områden av matematiken, inklusive elementär talteori, kombinatorik och analys (alla möjliga saker som Mathlib täcker), är vi inte långt ifrån en massiv förändring i dokumentationen av bevisens giltighet. Jag tror att det här kommer bli ett hektiskt år!