Lean4 half dabei, einen kleinen Bug in einer aktuellen Arbeit von Terence Tao zu finden

• Beitrag von Terence Tao auf mathstodon.xyz
• In einer aktuellen Arbeit von Terence Tao wurde durch ein Lean4-Formalisierungsprojekt ein kleiner, aber wichtiger Bug entdeckt
• Der Bug wurde beim Formalisieren auf Seite 6 der Arbeit gefunden; die Arbeit ist unter https://arxiv.org/pdf/2310.05328.pdf einsehbar
• In Taos Arbeit wurde für den Fall n=3, k=2 der divergierende Ausdruck 12log⁡n−1n−k−1 gefunden
• Das Problem tritt nur für kleine Werte von n auf und kann durch die Änderung einiger numerischer Konstanten auf der Seite behoben werden
• Für n≥8 bleibt die Logik weiterhin gültig, und Fälle mit kleinem n können auf einfachere Weise behandelt werden
• Lean4 forderte Tao auf, 0<n−3 zu beweisen, aber er hatte nur die Hypothese n>2, wodurch ein Widerspruch entstand
• Tao plant, einer neuen Version der Arbeit eine Fußnote hinzuzufügen, die einen kleinen Fehler anerkennt, der nach dem Versuch der Formalisierung in Lean4 entdeckt wurde
• Der Beitrag weckte Interesse und positive Reaktionen in der Community und unterstreicht die Bedeutung von Proof Assistants dafür, eine robuste Grundlage für künftige Arbeiten zu schaffen

[GN⁺]

Hacker-News-Kommentare

• Der berühmte Mathematiker Terence Tao nutzte Lean4 und GPT4, um einen kleinen Fehler in einer aktuellen Arbeit zu entdecken.
• Taos Lernprozess mit Lean4 ist in seinen Mastodon-Beiträgen dokumentiert und stellt eine interessante Fallstudie dazu dar, wie Lean4 die Arbeit beschleunigen kann.
• Für Einsteiger wird das Natural Number Game als leichter Einstieg in Lean4 empfohlen.
• Ein Nutzer schilderte seine Erfahrung damit, mit Lamports TLA+ formale Spezifikationen zu erstellen und Programmierfehler zu reduzieren.
• Trotz der Komplexität der Implementierung in Compilern besteht Interesse an abhängigen Typen.
• Die Kombination aus Lean4 und automatischem Beweisen wirkt wie eine vielversprechende technologische Kombination der Zukunft und könnte neue Entdeckungen fördern.
• Dass Tao Copilot verwendet, um Lean zu lernen, wurde als Beispiel dafür hervorgehoben, wie Lean4 die Reibung bei der Einführung neuer Werkzeuge verringern kann.
• Taos Fortschritte mit Lean4 können auf seinem GitHub eingesehen werden.
• Ein Nutzer schlug die Idee vor, formale Beweisprüfer mit Sprachmodellen zu kombinieren, um synthetische Vermutung-Beweis-Paare zu erzeugen; dies könnte sich bis zu übermenschlichen Fähigkeiten bei der Beweiserzeugung ausweiten.
• Der Begriff „Bug“ wurde verwendet, um einen mathematischen Fehler zu beschreiben, was einige Nutzer als ungewöhnlich empfanden.