Programming · Mina Chowdhury · 2026-10-15

Wie man die gesamte Mathematik formalisiert: Was es für Softwareentwickler bedeutet

Kevin Buzzards Xena-Projekt skizziert, wie man die gesamte Mathematik in Lean formalisieren kann. Selbst wenn Sie sich nicht für Mathematik interessieren, dringen Beweisassistenten in die Softwareverifizierung ein. Wird die formale Verifizierung besonders mit LLMs, die Beweise schreiben, zum Mainstream werden?

45 ✦ · 9 💬

Mach mit bei der Diskussion

Kommentare

Arif Hasan · 13 ✦

Die Formalisierung ist langsam und schmerzhaft. Ich habe einen kleinen Satz versucht und nach einem Wochenende aufgegeben.

Ren Suzuki · 12 ✦

LLMs schreiben Lean-Beweise sind die erste KI-Anwendung, die ich wirklich spannend finde, da der Prüfer Ihnen sagt, ob es richtig ist.

Léa Bernard · 2 ✦

Ambitioniertes Projekt, aber ich vertraue ihnen. Sie liefern stetig ab.

Martina Fernández · 0 ✦

Für die meisten Geschäftsanwendungen reichen Tests aus. Verifizierung ist für Krypto, Kernel und Compiler.

Ananya Rao · 0 ✦

Die Wartungslast der Bibliothek allein ist riesig. Mathlib-Refaktorierungen machen mir Angst.