Mathematische Arbeiten benötigen eine formale Validierung. Dies geschieht normalerweise informell durch einen Gutachter. Aber was wäre, wenn wir uns auf etwas Robusteres wie die Auto-Formalisation in Lean 4 verlassen könnten, bei der die Rolle des Gutachters auf eine sorgfältige Überprüfung der Formulierungen der Definitionen und Theoreme reduziert würde? Die Kompilierung des automatisch generierten Codes würde zu einem Beweiszertifikat werden. Das ist es, was in einem längeren Lauf passiert ist, den ich mit Aristoteles von @HarmonicMath gemacht habe. Danke an @PietroMonticone und @llllvvuu für die Unterstützung bei der Einrichtung des Entwurfs. Hier präsentiere ich eine vollständige korrekte Auto-Formalisation eines Papiers meines Freundes Stefan Barańczuk über Chebyshev-Teilbarkeitsfolgen. Der Code umfasst etwa 5000 Zeilen hochgradig nicht-trivialen Lean. Er korrigiert alle Inkonsistenzen und Lücken im Hauptpapier (sogar einige delegierte Propositionen werden bewiesen). Ich werde eine Reihe solcher Experimente posten, die beweisen, dass wir in einigen Bereichen der Mathematik, einschließlich elementarer Zahlentheorie, Kombinatorik und Analysis (alle Arten von Themen, die von Mathlib abgedeckt werden), nicht weit von einem massiven Wandel in der Dokumentation der Gültigkeit von Beweisen entfernt sind. Ich denke, das wird ein hektisches Jahr!