Hier präsentiere ich eine vollständige Auto-Formalisation eines aktuellen Mathematikpapiers (schon wieder!) Barańczuk, Stefan. "Reduzierung der Anzahl der Gleichungen, die eine Teilmenge des n-Raums über einem endlichen Körper definieren." Annales de la Faculté des sciences de Toulouse : Mathématiques, ser. 6, vol. 33, no. 1 (2024): 177–182. Ich habe ein paar Tage an diesem Projekt gearbeitet. Zuerst habe ich Aristotle von @HarmonicMath verwendet, das in etwa 15 Stunden den Beweis vollständig auto-formalisiert hat. Dann, mit der großartigen Hilfe von @PietroMonticone, gelang es mir, eine Blaupause-Version des Beweises zu erstellen. Dies ist eine Version, in der alle Teile der Dokumentation in LaTeX interaktiv werden und inspiziert sowie studiert werden können. Wir können die Abhängigkeiten im Beweis sehen und ihre Beziehungen studieren. In der Nachbearbeitungsphase habe ich auch Grok Heavy und Codex CLI mit GPT-5.2 im xhigh-Modus verwendet, um eine zeilenweise Analyse des formalen Beweises zu schreiben. Dies ist eine große Hilfe für Menschen, die keine professionellen Lean 4-Programmierer sind. Man kann wirklich alle Schritte des Beweises verinnerlichen. Ich möchte meine Eindrücke zusammenfassen und was ich aus dieser Erfahrung gelernt habe. @vladtenev @Leonard41111588 @HarmonicMath @llllvvuu @littmath @AlexKontorovich @jdlichtman @KenOno691 @CarinaLHong @gdb @hongyuan_mei

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!

Wenn ich heute ein Student wäre, würde die Interaktion mit modernen LLMs fast wie Schummeln erscheinen. Heute Morgen habe ich zufällig ein Bild von der Tafel gemacht und ChatGPT-5.2-Pro gebeten, den Kontext, die Lösung und einige Anmerkungen zum berühmten Chevalley-Satz über konstruierbare Mengen zu erklären. Was ich erhielt, war ein bemerkenswert tiefgehender Bericht, der qualitativ hochwertiges Material zur algebraischen Geometrie aus dem gesamten Internet synthetisierte. Das wirft eine ernsthafte Frage auf: Was ist der echte Aufwand und die Herausforderung für Studenten heute? Kosten sind sicherlich ein Faktor, aber sobald der Zugang zu diesen Modellen verfügbar ist, wie sollte man in diesem Überfluss lernen, in dem Erklärungen, Referenzen und interaktive Erkundungen sofort zugänglich sind? Vielleicht besteht der Kampf nicht mehr darin, Informationen zu beschaffen oder sogar individuelle Argumente zu verstehen, sondern darin, Urteilsvermögen zu entwickeln: zu wissen, welche Fragen man stellen sollte, welchen Erklärungen man vertrauen kann, wie man Tiefe von oberflächlicher Plausibilität unterscheidet und wie man Ideen verinnerlicht, anstatt sie nur zu konsumieren. In einer Umgebung, in der Antworten im Überfluss vorhanden sind, könnte die wirkliche Schwierigkeit darin liegen, Geschmack, mathematische Intuition und die Fähigkeit zu entwickeln, in diesem plötzlichen Überfluss an Wissen zu navigieren – anstatt darin zu ertrinken.