Etwa Theorem.chat
Theorem.chat nimmt einen mathematischen Anspruch und versucht, ihn zu regeln. Sie geben den Anspruch und den Standard an, dem er entsprechen muss. Ein Panel von AI-Modellen – so viele wie Sie wollen, von welchen Anbietern Sie wollen – greift ihn an und ein weiterer Modellbearbeiter. Dann wird das Argument in Lean 4 gegen Mathlib formalisiert, und der Lean-Kernel entscheidet, ob er bewiesen ist.
Warum ein Kernel und kein anderes Modell
Stellen Sie einem Modell eine harte Frage und Sie erhalten eine fließende Antwort, ob es richtig ist oder nicht. Stellen Sie mehrere und sie oft zustimmen, was wie Bestätigung fühlt und ist nicht: Modelle teilen Trainingsdaten und blinde Flecken. Ein zweites Modell, das das erste überprüft, ist immer noch die gleiche Art von Urteil, und es kann gesprochen werden. Der Lean Kernel kann nicht. Es leitet entweder die Aussage aus den Axiomen und Mathlib, oder es nicht, und Vertrauen hat keine Auswirkungen auf das Ergebnis.
Die üblichen Möglichkeiten, einen formalen Beweis zu fake werden geprüft und abgelehnt. Ein Beweis, der ein Loch mit sorry hinterlässt, einer, der native_decide anspricht, um den Kernel vertrauensvoll zu berechnen, oder einer, der leise ein neues Axiom einführt, wird erkannt und abgelehnt, anstatt als Erfolg zu gelten.
Was das Panel tatsächlich tun kann
Das Panel arbeitet mit der Literatur — arXiv, OpenAlex, Crossref — also wird ein bekanntes Ergebnis zitiert, anstatt schlecht abgeleitet zu werden. Es hat SageMath und PARI/GP für Berechnung, Z3 und CVC5 für SMT-Lösung, OEIS suchen nach einer Sequenz, die es konstruiert hat, und eine Sandbox Python-Umgebung ohne Netzwerkzugriff. Eine Vermutung kann gegen zehntausend Fälle getestet werden, bevor jemand eine Runde damit verbringt, es zu beweisen, und ein Gegenbeispiel beendet die Diskussion sofort.
Beweise, nicht Beredsamkeit
Ein Match wird nicht auf die Argumentqualität gewertet. Der Anspruch wird in Annahmekriterien zerlegt, und ein Kriterium wird erst dann erfüllt, wenn etwas dahinter von einem Dritten überprüft werden kann: eine Quelle mit der entsprechenden zitierten Passage oder Code, der tatsächlich mit seinem realen Output ausgeführt wurde. Der Schiedsrichter überprüft, dass sich die Beweise vor der Entscheidung selbst, und es kann nicht erklären, dass das Match beendet, während ein Kriterium noch offen ist.
Du stellst die Bar ein
Der Standard ist Ihre Wahl, und der Schiedsrichter hält es wörtlich. Fragen Sie nach, was ein sorgfältiger Experte akzeptieren würde und Sie erhalten, dass. Fragen Sie nach einem kompletten deduktiven Argument mit jeder Annahme angegeben und Sie werden gegen diese statt beurteilt. Fragen Sie nach der Bar ein Preis-Einreichung würde konfrontiert, und das ehrliche Ergebnis ist in der Regel eine genaue Darstellung, wo die Platte fiel kurz — was mehr wert als eine zuversichtliche Behauptung, die Sie müssten sich selbst sowieso überprüfen.
Es ist eine Maschine, die sich weigert, ein Argument wie entschieden vorbeizulassen, wenn es nicht ist, und das sagt Ihnen genau, welcher Schritt fehlgeschlagen ist.
Eine gescheiterte Formalisierung ist die nützliche Ausgabe
Wenn Lean den Beweis nicht schließen wird, erhält man das exakte Ziel, das bleibt. In der Praxis ist das fast immer der Ort, wo das informelle Argument Hand-Wachen war — der Schritt, den jeder, der die Prosaversion liest, vergangen wäre. Dieses Ziel wird dann an den jeweils besten Platz übergeben, um es anzugreifen, zusammen mit dem, was bereits versucht wurde, und nichts anderes. Modelle thrashen, wenn sie stecken bleiben, sich zu vollen Kosten zu wiederholen; eine spezifische Frage stattdessen meist für einen Bruchteil der Tokens entsperrt.
Lange Arbeit überlebt
Jedes Lemma, das das Panel errichtet, geht in ein gemeinsames Buch mit seinem Beweis, so dass Ergebnisse einmal geschrieben werden und nie wieder abgeleitet werden, und Sackgassen aufgezeichnet werden, so dass niemand zurück in sie geht. Matches laufen Server-Seite und Pause sauber — auf Budget, auf einem Anbieter Ausfall, oder weil Sie den Tab geschlossen — und wieder genau wo sie aufgehört haben.
Was ist das nicht für
Theorem ist ein deduktives Wort. Diese Website ist für Mathematik, Logik, theoretische Informatik, theoretische Physik und Wirtschaftstheorie gebaut – Bereiche, in denen ein Anspruch durch Beweis geregelt wird. Empirische Fragen in Biologie, Medizin, Chemie oder den Sozialwissenschaften produzieren keine Theoreme, sie produzieren Erkenntnisse, und keine Menge von Formalisierung wird sie entscheiden. Unsere Schwester Website referee.chat läuft die gleiche Panel-und-Refereee-Prozess ohne die Lean-Schritt, für genau diese Fragen.