LONDON (IT BOLTWISE) – Axiom Math will KI-„Slop“ aus der Mathematik verhindern, indem die Beweise in überprüfbaren Code überführt werden. Das Startup hat den formalen Nachweis des Stacks Project bekannt gegeben, einer der größten mathematischen Wissenssammlungen überhaupt. Die von KI-Agenten erstellten Lean-Implementierungen umfassen laut Angaben Millionen von Codezeilen, die ein Proof Assistant Zeile für Zeile prüft. Damit entsteht eine Grundlage, auf der künftig nicht nur Mathematiker, sondern auch Software- und KI-Teams mit geringerem Fehlerrisiko aufbauen können.
Der Reiz von Künstlicher Intelligenz in der Forschung liegt seit Monaten in der Geschwindigkeit: In immer kürzeren Abständen entstehen neue Textentwürfe, Lösungsvorschläge und „Erklärungen“ zu komplexen Themen. Genau diese Dynamik macht aber auch das Problem sichtbar, das Axiom Math adressieren will: Wenn ein KI-System mathematische Argumente lediglich nachträglich plausibilisiert, fehlt oft die letzte Instanz, die aus Plausibilität zwingende Logik macht. Das Unternehmen positioniert sich deshalb nicht als Generator neuer Ergebnisse, sondern als Produzent einer überprüfbaren Grundlage, die andere Systeme als verlässliches Fundament verwenden können.
Im Mittelpunkt steht dabei die formale Verifikation einer großen Referenzbasis: Axiom Math berichtet, dass das Stacks Project offiziell verifiziert wurde. Dabei handelt es sich um ein offenes, über Jahre gewachsenes mathematisches Korpus, das auf einem System aufsetzt, das sich weniger wie ein Lehrbuch als eher wie ein zusammenhängendes Beweisnetz lesen lässt. Laut Beschreibung wurde das Stacks Project 2005 von Johan de Jong als Open-Source-Referenz gestartet; seitdem tragen Mathematiker kontinuierlich Inhalte bei, die von klassischer Algebra bis zu fortgeschrittenen Ideen in algebraischer Geometrie, Algebra und Zahlentheorie reichen. Der technische Kern der Arbeit besteht darin, dass jeder einzelne Satz nicht „irgendwie“ durch eine KI-Näherung gestützt wird, sondern so in eine formale Sprache übertragen wird, dass ein Proof Assistant die Schritte exakt überprüfen kann.
Für die Umsetzung nutzt Axiom Lean als Programmiersprache zur formalen Darstellung von Mathematik. Mathematiker schreiben die Beweise dabei als Code um; ein Proof Assistant kontrolliert anschließend die Korrektheit Zeile für Zeile. Das unterscheidet sich konzeptionell von typischen Software-Tests, weil hier nicht nur „Ergebnisse“ überprüft werden, sondern die logische Struktur des Arguments selbst. Dass diese Idee über die Mathematik hinaus funktioniert, ist in der Technik längst bekannt: Formale Verifikation wird auch eingesetzt, um Chip-Designs abzusichern, und in Frankreich haben formale Methoden offenbar geholfen, Fehler in Software zu finden, die Familienleistungen berechnet. Entscheidend ist außerdem die Kopplung im Stacks Project: Viele Definitionen und Theoreme bauen aufeinander auf, wie in einem Familienbaum. Wer nur einzelne Behauptungen verifiziert, greift zu kurz; Axiom musste deshalb die Verknüpfungen über eine extrem große Codebasis hinweg konsistent halten.
Die Dimension wird in den Angaben über die resultierende Codemenge greifbar: Axiom beschreibt eine Übersetzung der rund 7.654 Seiten in etwa 16 Millionen Zeilen computergeprüften Codes. Diese Zahl ist nicht nur ein Hinweis auf Umfang, sondern auch auf das Engineering-Problem im Hintergrund. Axiom habe zunächst Zweifel gehabt, ob „vibe coding“ die „Schönheit“ und Konsistenz einer historisch gewachsenen Wissensstruktur bewahren kann; Carina Hong formulierte in dem Zusammenhang sinngemäß, dass große und gleichzeitig sensible Elemente im Leben nicht gut zusammenpassen. In dem gleichen Ton betont sie, dass man in einer mathematischen Grundlage vor allem Konsistenz erreichen müsse: „[Stacks] is a collection of mathematical results that is the foundation of mathematics. You want [theorems] to be consistent and not, like, paradoxical. You want the definitions to not fight with each other.“ Auch wenn solche Sätze nach „Philosophie“ klingen, verweist der technische Aufwand auf eine konkrete Herausforderung: Fehlerfreiheit in einer Verifikationskette bedeutet, dass jede kleine Inkompatibilität in einer Definition später in vielen Abhängigkeiten als Bruch sichtbar wird.
Um die Aufgabe praktisch zu skalieren, setzt Axiom auf KI-Agenten, die nicht sequentiell „ein Proof nach dem anderen“ abarbeiten, sondern parallel Aufgaben finden und eigenständig priorisieren. Nach Angaben des technischen Teams wurde dafür eine nur lockere Struktur vorgegeben; statt eines vollständigen Hierarchieplans zur Beschäftigung jedes Agenten sollte das System selbst herausfinden, welche Teilaufgaben sich parallelisieren lassen und welche Bausteine als nächstes Sinn ergeben. Zusätzlich trainiert Axiom eigene Modelle, um bei mathematischen Aufgaben eine Art „Geschmack“ für geeignete Schritte zu entwickeln. Anfangs habe man dafür auf einen Lean-Experten gesetzt, der den Agenten dieses menschliche Gespür vermitteln sollte; später, so die Darstellung, hätten die Systeme diesen Geschmack zunehmend selbst verinnerlicht. Der Ansatz ist damit eng verwandt mit den aktuellen Mustern aus der KI-Entwicklung für Produktivsysteme: nicht nur Output erzeugen, sondern Entscheidungsheuristiken so gestalten, dass das System konsistente Zwischenschritte findet.
Strategisch ordnet Axiom das Projekt als Lückenschließung in der Formalisierung ein. In der Beschreibung wird auf einen „Black Hole“-Bereich verwiesen: Es gab bislang wenig Material, an das sich Forschende in der algebraischen Geometrie mit Lean anschließen konnten, wenn sie neue Arbeiten formal prüfen wollten. Mit der nun überprüften Stacks-Basis entstehe dagegen ein Baukasten, auf den spätere Beweise aufsetzen können, statt bei null anzufangen. Der Nutzen lässt sich auch allgemein auf die Lernkurve von formalen Systemen übertragen: Wenn einmal große Mengen an überprüftem Wissen existieren, wird es einfacher, darauf aufbauende weitere Beweise ebenfalls zu formalisieren. Terence Tao brachte die Logik dafür in der Quelle kurz auf den Punkt: Je mehr formalisierte Beweise existieren, desto mehr formalisierte Beweise lassen sich erzeugen.
Über die Mathematik hinaus zielt Axiom auf ein wiederkehrendes Problem in der Softwarebranche: Entwickler kämpfen seit Jahren darum, Codefehler und Sicherheitslücken systematisch zu reduzieren. Je stärker KI-Agenten künftig in die Code-Erstellung eingreifen, desto größer wird das Risiko, dass sich fehlerhafte Annahmen „durch die Pipeline“ ziehen. Genau hier setzt das Unternehmen an, indem es KI-Agenten Zugang zu einer überprüfbaren Wissensschicht geben möchte. Axiom argumentiert, dass Mathematik der Einstieg ist, weil sie eine übertragbare Disziplin für formale Strukturen liefert: Agenten können den Lean-Code lesen, verstehen und darüber neue Infrastruktur aufbauen. Carina Hong geht dabei noch einen Schritt weiter und fordert die Branche offen heraus, Formalisierung in einem ähnlichen Maßstab zu verfolgen. Für Unternehmen mit KI-Teams bedeutet das weniger eine Frage nach dem nächsten großen Modell, sondern eine nach der nächsten verlässlichen Wissens- und Verifikationsschicht, auf der Modelle und Agenten operieren können.
🔥 Heutige Hot Deals bei Amazon: Bis zu 80% Rabatte!
🎉 Amazon Haul-Store für absolute Schnäppchenjäger!
- ★ 23-stufiges KI-Go-Training – Für Spieler mit Grundkenntnissen der Regeln – Entwickelt als intelligenter Trainingspartner passt sich die KI Spielern von 18K bis 9D an. Ideal für alle, die die Grundregeln bereits beherrschen und ihr Spiel verbessern möchten.
- IHR EMOTIONALER AI-BEGLEITER: Eiliko ist mehr als nur ein Anhänger, es ist ein charismatischer KI-Freund. Mit einem dynamischen LED-Bildschirm, der eine Vielzahl von animierten Gesichtern und Ausdrucksformen anzeigt, reagiert er auf Ihre Interaktionen mit einzigartiger Persönlichkeit und Charme.
- 【MEHR LEBEN FÜR DEINEN SCHREIBTISCH】 Lerne Eilik kennen – deinen kleinen Roboter-Freund mit Persönlichkeit. Mit liebevollen Animationen, ausdrucksstarken Reaktionen und spielerischen Interaktionen bringt Eilik mehr Freude in deinen Alltag. Ob auf dem Schreibtisch, im Büro oder am Nachttisch – Eilik wird schnell zu einem vertrauten Begleiter für besondere Momente.
- 【XL-Größe für gedeihende Pflanzen】Geben Sie Ihren Pflanzen den Raum, den sie verdienen! Unser verbessertes, großes 13,7 cm großes Design bietet Platz für Pflanzen mit einem Durchmesser von bis zu 8,9 cm und damit deutlich mehr Platz für Wurzelwachstum und Pflanzengesundheit im Vergleich zu kleineren, veralteten Modellen. Die Produktabmessungen betragen 13,6 x 13,6 x 13,2 cm und das Gerät wiegt nur 355 g.
- V28 Update - JETZT MIT NEUEN FUNKTIONEN! Als Reaktion auf das Ladeproblem von Loona haben wir das automatische Aufladen 2.0 verbessert. Diese Optimierung hilft Loona, die Ladewege in verschiedenen Szenarien zu erkennen und anzupassen, um die Erfolgsquote beim automatischen Aufladen zu erhöhen. Mobile Hotspots können sich mit Loona verbinden und überwinden WLAN-Einschränkungen, sodass Sie jederzeit und überall mit Loona interagieren können.
- Die besten Bücher rund um KI & Robotik!
- Die besten KI-News kostenlos per eMail erhalten!
- Zur Startseite von IT BOLTWISE® für aktuelle KI-News!
- IT BOLTWISE® kostenlos auf Patreon unterstützen!
- Aktuelle KI-Jobs auf StepStone finden und bewerben!
- Künstliche Intelligenz: Dem Menschen überlegen – wie KI uns rettet und bedroht | Der Neurowissenschaftler, Psychiater und SPIEGEL-Bestsellerautor von »Digitale Demenz«
Du hast einen wertvollen Beitrag oder Kommentar zum Artikel "Axiom Math verifiziert „Stacks Project“ und setzt KI auf Lean-Checks" für unsere Leser?
#Sophos
#AmazonPrime
#Bestseller
Es werden alle Kommentare moderiert!
Für eine offene Diskussion behalten wir uns vor, jeden Kommentar zu löschen, der nicht direkt auf das Thema abzielt oder nur den Zweck hat, Leser oder Autoren herabzuwürdigen.
Wir möchten, dass respektvoll miteinander kommuniziert wird, so als ob die Diskussion mit real anwesenden Personen geführt wird. Dies machen wir für den Großteil unserer Leser, der sachlich und konstruktiv über ein Thema sprechen möchte.
Du willst nichts verpassen?
Du möchtest über ähnliche News und Beiträge wie "Axiom Math verifiziert „Stacks Project“ und setzt KI auf Lean-Checks" informiert werden? Neben der E-Mail-Benachrichtigung habt ihr auch die Möglichkeit, den Feed dieses Beitrags zu abonnieren. Wer natürlich alles lesen möchte, der sollte den RSS-Hauptfeed oder IT BOLTWISE® bei Google News wie auch bei Bing News abonnieren.
Nutze die Google-Suchmaschine für eine weitere Themenrecherche: »Axiom Math verifiziert „Stacks Project“ und setzt KI auf Lean-Checks« bei Google Deutschland suchen, bei Bing oder Google News!