Claude formalisiert Fermats letzten Satz in Lean

Anthropic hat vor Kurzem eine massive Forschungsaufgabe abgeschlossen. Ein internes Modell arbeitete 11 Tage lang daran, Fermats letzten Satz mithilfe der Beweissprache Lean 4 zu formalisieren.

Dies ist keine neue mathematische Entdeckung. Andrew Wiles hat diesen Satz bereits 1995 bewiesen. Was Anthropic getan hat, war, diesen bestehenden Beweis in Code zu übersetzen. Dies ermöglicht es einem Computer, jeden logischen Schritt mit absoluter Sicherheit zu überprüfen.

Das Ausmaß dieses Projekts ist gewaltig: • Das Modell erzeugte 13 Millionen Zeilen Lean-Code. • Es bewies 30.300 Zwischensätze. • Es verwendete fast 6 Milliarden Output-Token.

Das Modell arbeitete größtenteils eigenständig. Menschen gaben nur gelegentlich Anweisungen auf hoher Ebene. Der Prozess wurde mitten in der Nacht abgeschlossen, als niemand zusah. Das System protokollierte den Erfolg automatisch.

Zwei wichtige Punkte:

  1. Dieses Modell ist ein internes Forschungswerkzeug. Sie können noch nicht über eine API darauf zugreifen. Es ist nicht dasselbe wie die Claude-Modelle, die Sie heute verwenden.
  2. Der wahre Wert für Entwickler liegt in der Koordinationsschicht namens Prove2Me.

Prove2Me ist ein Open-Source-Tool. Es nutzt einen Abhängigkeitsgraphen, um Aufgaben zu verwalten. Anstatt einer einfachen Checkliste erstellt es eine Karte darüber, wie Beweise miteinander verknüpft sind.

Diese Struktur löst zwei Hauptprobleme für Agenten-Workflows:

  • Sie verhindert, dass mehrere Agenten dieselbe Arbeit erledigen.
  • Sie verleiht Agenten ein gemeinsames Gedächtnis, damit sie das Hauptziel nicht vergessen.

Die meisten Agenten-Workflows scheitern, weil sie im Laufe der Zeit den Kontext verlieren. Die Verwendung eines gemeinsamen, externen Graphen anstelle eines langen Chat-Fensters hält die Aufgabe auf Kurs.

Sie sollten die Prove2Me-Architektur studieren, wenn Sie Agenten-Workflows entwickeln. Selbst wenn Sie nicht die Forschungsmodelle von Anthropic nutzen, ist die Art und Weise, wie sie Aufgaben koordinieren, eine Blaupause für Arbeiten mit langem Zeithorizont.

Quelle: https://dev.to/raxxostudios/claude-just-formalized-fermats-last-theorem-in-lean-3p36

Optionale Lern-Community: https://t.me/GyaanSetuAi