Formalisieren eines Mathematik-Papiers in Lean 4

Sie liefern ein Lean-Projekt mit Dokumenten, in dem:

Jedes Ergebnis, das das Papier beweist, wird mit dem Argument des Papiers selbst bewiesen. Ein Beweis weicht nur dann vom Papier ab, wenn es unbedingt nötig ist, und jede Abweichung wird gemeldet (Regeln, „Treue Beweise“);
Jedes Ergebnis, das das Papier in seinen Beweisen zitiert, wird ebenfalls bewiesen: in Mathlib, in einer anderen öffentlichen Bibliothek oder in External/. Ein zitiertes Ergebnis benötigt möglicherweise Mathematik, die keine Lean-Bibliothek hat und die das Projekt nicht vernünftig erstellen kann. Ein solches Ergebnis wird zur benannten Hypothese jeder Aussage, die es verwendet, und die Formalisierung stellt dann klar, dass sie konditional ist;
Die Aussagen sagen, was das Papier sagt, und jede Abweichung wird dokumentiert;
lake build wird erfolgreich ausgeführt ohne sorry (außer in den Aussagen von Challenge.lean, wie vorgesehen), ohne admit und ohne Projekt-axiom. Jede Deklaration der Bibliothek hängt nur von propext, Classical.choice und Quot.sound ab;
REPORT.md prüft das Papier anhand der Formalisierung. Es endet mit dem, was als Nächstes kommt: wie sich das Thema seit dem Papier entwickelt hat, wie seine Ergebnisse erweitert, verallgemeinert oder verstärkt werden könnten und wie seine Beweise einfacher sein könnten. README.md fasst die Formalisierung zusammen, und CREDITS.md beschreibt, wie sie erstellt wurde: die Vorgehensweise, die Agenten und Modelle sowie die Zeit und Mühe (das Ausführungsprotokoll);
Eine private NEXT.md, die nie veröffentlicht wird, es sei denn, der Benutzer fragt, beantwortet, welches Papier der Benutzer als Nächstes schreiben könnte: einige Kandidaten, die jeweils ein eigenes Papier ergeben würden, eingehend untersucht (das Hindernis, die Versuche, die Beweise, was bereits bewiesen ist), keine Liste von inkrementellen Erweiterungen;
Das Projekt wird für Palomar verpackt und mit Erlaubnis des Benutzers veröffentlicht und durch Palomars Preflight ausgeführt.

Die Arbeit hat zwei Phasen. In Phase 1 wird alles formalisiert, was das Papier selbst beweist. Ergebnisse, die aus der Literatur stammen, können temporäre Axiome sein. In Phase 2 werden diese Axiome entfernt: Sie werden bewiesen oder die unerreichbaren werden in benannte Hypothesen umgewandelt. Die Einrichtung erfolgt vor den beiden Phasen, und Überprüfung, Bereinigung, Prüfung und Verpackung danach.

Prinzipien

Diese erklären die folgenden Regeln. Verwenden Sie sie, wenn keine Regel eine Situation abdeckt.

Das Papier ist die Quelle der Wahrheit für Aussagen und Argumente; Lean beurteilt die Korrektheit. Eine Aussage, die von der des Papiers abweicht, ist eine falsche Formalisierung, egal wie sauber ihr Beweis ist. Gleiches gilt für einen Beweis, der die Aussage des Papiers mit einem anderen Argument erreicht: Die Formalisierung überprüft die Beweise des Papiers, nicht nur seine Behauptungen. Überprüfen Sie Aussagen anhand der TeX-Quelle, bevor jemand sie beweist. Vergleichen Sie Beweise mit denen des Papiers, sobald sie geschrieben sind. Ändern Sie niemals eines davon stillschweigend.
Eine Formalisierung, die niemand kompiliert hat, ist ein Entwurf. Aus dem Gedächtnis geschriebenes und nie kompiliertes Lean enthält oft geratene Lemma-Namen, falsche Signaturen und falsche Hilfslemmata. Kompilieren Sie, wann immer eine Lean-Toolchain verfügbar ist. Wenn keine vorhanden ist oder der Benutzer das Kompilieren verbietet, sagen Sie klar, dass das Ergebnis unverifiziert ist.
„Standard“, „offensichtlich“, „symmetrisch“, „routine“ benötigen immer noch Beweise. Mathlib hat die Tatsache möglicherweise; wenn nicht, beweisen Sie sie. Nur das, was das Papier selbst aus einer anderen Quelle übernimmt, darf zu einem Axiom werden.
Extern bedeutet, woher ein Ergebnis stammt, nicht dass es vertrauenswürdig ist. Ein zitiertes Ergebnis lebt in External/ wegen seiner Quelle. Es wird wie alles andere bewiesen.
Eine Annahme ist eine Annahme, egal in welcher Form. Ein zitiertes Ergebnis, das nicht bewiesen ist, wird angenommen, egal ob es als Axiom, Hypothese oder Feld einer Struktur geschrieben ist. Axiome sind nicht erlaubt. Hypothesen sind erlaubt, wenn ein Leser der Aussage jede einzelne sehen kann, unter dem Namen des Ergebnisses, das sie annimmt. Eine Struktur, die Daten mit angenommenen Theoremen mischt, verbirgt, wovon ein Ergebnis abhängt. Gleiches gilt für einen Parameter, dessen Typ wie Daten aussieht, aber ein Theorem enthält.
Daten kommen mit ihrer definierenden Eigenschaft. Wenn eine Aussage ein Objekt des Papiers als Parameter akzeptiert, anstatt es zu konstruieren, muss sie auch die Eigenschaft verlangen, die das Objekt definiert. Andernfalls handelt der Satz von jedem Objekt, das die anderen Hypothesen erfüllt, was eine andere Aussage ist.
Repräsentationsentscheidungen benötigen Brücken. Leans Objekte können von denen des Papiers abweichen: Indizes ab 0 statt 1, Listen statt indizierte Familien, eine gebündelte Mathlib-Struktur statt eines informellen Objekts, ein konkretes Modell statt einer Beschreibung „bis auf Isomorphie“. Wenn dies der Fall ist, beweisen Sie ein Lemma, das die beiden verbindet, und dokumentieren Sie die Wahl. Gehen Sie niemals davon aus, dass zwei Darstellungen äquivalent sind.
Konstanten und Bereiche sind Teil der Mathematik. Potenzen, Faktoren, Ab- und Aufrundungen, strikte versus schwache Ungleichungen, die Endpunkte von Bereichen und die abgeschnittene Subtraktion auf ℕ entscheiden, ob eine Aussage wahr ist.
Berichten Sie ehrlich. Wenn ein Schritt übersprungen wurde, ein Beweis fehlschlägt, eine Aussage geändert werden musste oder ein Beweis vom Papier abweichen musste, sagen Sie dies und geben Sie den Grund an. Die Prüfung ist nur nützlich, wenn ihr vertraut werden kann.
Eine Lücke in einem Beweis ist keine falsche Aussage. Wenn der Beweis des Papiers eine Tatsache verwendet, die seine Hypothesen nicht hergeben, kann die Aussage dennoch wahr sein. Suchen Sie nach einem korrekten Argument, bevor Sie etwas über die Aussage schließen.
Messen Sie die Arbeit. Leser und Registrierungen fragen, wie eine Formalisierung erstellt wurde. Die Antwort ist günstig, während der Arbeit zu protokollieren, und danach schwer zu rekonstruieren.

Regeln

Schwächen oder ändern Sie niemals die Aussage eines Papierergebnisses, um einen Beweis zum Funktionieren zu bringen. Wenn die Aussage des Papiers falsch ist, stellen Sie die Arbeit daran ein und informieren Sie sofort den Benutzer, mit dem Gegenbeispiel. Andere Arbeiten können in der Zwischenzeit fortgesetzt werden. Wenn der Benutzer zustimmt, formalisieren Sie die nächstgelegene korrekte Version und dokumentieren Sie sie als Fehler im Bericht. Offensichtliche Druckfehler sind die eine Ausnahme (unten).
Fügen Sie einem Papierergebnis niemals eine Hypothese hinzu, weil sein Beweis sie zu benötigen scheint. Das Hinzufügen einer solchen schwächt das Ergebnis. Fügen Sie eine nur hinzu, wenn die Aussage selbst ein Gegenbeispiel hat, nicht weil ein Schritt des Beweises fehlschlägt, und folgen Sie dann der vorherigen Regel. Beweisen Sie andernfalls die Aussage wie gedruckt, mit einem korrigierten Argument, und dokumentieren Sie die Lücke im Beweis als E-Punkt. Wenn Sie weder einen Beweis noch ein Gegenbeispiel finden, teilen Sie dem Benutzer mit, was fehlt. Er entscheidet, ob die Arbeit fortgesetzt oder eine schwächere Aussage formalisiert wird, dokumentiert als Abweichung.
Treue Beweise. Beweisen Sie jedes Ergebnis mit dem Beweis des Papiers: dieselben Zwischenbehauptungen, dieselben Konstruktionen und Fallunterscheidungen, und dieselben früheren Ergebnisse, wo das Papier sie zitiert. Die Ergebnisse, die der Beweis des Papiers zitiert, bilden seine Route. Der formale Beweis muss dieselbe Route haben, und die Routenprüfung (Phase 6) überprüft dies. Nur die Mechanik darf sich unterscheiden: Taktiken, das Mathlib-Lemma, das einen Routine-Schritt abschließt, die Reihenfolge unabhängiger Schritte und Hilfslemmata, die einen Schritt des Papiers kapseln. Wenn Mathlib zufällig ein nummeriertes Ergebnis beweist, beweisen Sie es dennoch mit dem Argument des Papiers, es sei denn, das Papier selbst behandelt es als bekannt (es zitiert es oder nennt es Standard).
Weichen Sie vom Beweis des Papiers nur ab, wenn Sie müssen, das heißt, aus einem dieser Gründe und keinem anderen:
1. Das Argument des Papiers ist an diesem Schritt falsch oder hat dort eine Lücke und kann nicht entlang seiner eigenen Linien repariert werden (der Schritt ist auch ein E-Punkt);
2. Der Schritt benötigt Mathematik, die Lean fehlt und die das Projekt nicht vernünftig erstellen kann (wie bei unerreichbaren zitierten Ergebnissen, unten), und ein anderes Argument vermeidet dies;
3. Der Schritt hat keine Bedeutung in einer Darstellung, die die Formalisierung verwenden muss (Prinzipien), sodass eine getreue Übersetzung ein anderes Argument ist.
Ein kürzerer, eleganterer, allgemeinerer oder automatischerer Beweis ist kein Grund. Ebenso wenig ein Beweis, der einfacher zu formalisieren oder schneller zu bauen ist. Ein einfacheres Argument, das Sie finden, ist dennoch erhaltenswert: Dokumentieren Sie es, mit einer Skizze, für den Abschnitt „Was kommt als Nächstes“ des Berichts (Phase 8), und beweisen Sie das Ergebnis mit dem Argument des Papiers. Weichen Sie so wenig ab, wie der Grund erfordert: reparieren Sie den Schritt, nicht den Beweis. Wenn eine Abweichung das gesamte Argument eines nummerierten Ergebnisses ersetzen würde, nicht nur einen Schritt, schlagen Sie es dem Benutzer zuerst vor, mit dem Grund. Andere Arbeiten werden in der Zwischenzeit fortgesetzt.
Melden Sie jede Abweichung, immer. Dokumentieren Sie für jede, was das Papier tut, was die Formalisierung stattdessen tut und welcher Grund die Änderung erzwingt. Dokumentieren Sie es im Docstring der Deklaration („Abweichung vom Papier: …“), in der Tabelle der Abweichungen des Berichts, in formalization.yaml (fidelity.divergences), in jedem Begleittext, in der Datei der aufgezeichneten Unterschiede der Routenprüfung, wenn sich die Route ändert, und im nächsten Statusbericht. Eine Abweichung, die in einem dieser fehlt, ist ein Fehler: Finden und beheben Sie ihn, wie Sie es bei einer stillschweigend geänderten Aussage tun würden.
Zitierte Ergebnisse außer Reichweite. Ein zitiertes Ergebnis benötigt möglicherweise Mathematik, die keine Lean-Bibliothek hat. Wenn der Aufbau dieser Mathematik im Projekt ein moderater Aufwand ist, bauen Sie sie. Andernfalls ist die Voreinstellung eine konditionale Formalisierung: Das Ergebnis wird zu einer benannten Hypothese jeder Aussage, deren Beweis es verwendet. Wenden Sie die Voreinstellung ohne Nachfrage an und melden Sie sie im nächsten Statusbericht. Fragen Sie den Benutzer nur, wenn der Aufbau der fehlenden Mathematik ein großer, aber machbarer Aufwand wäre: Ob dieser Aufwand betrieben werden soll, ist seine Entscheidung. Setzen Sie in der Zwischenzeit die andere Arbeit unter der Voreinstellung fort. Wenn er sich für den Aufbau entscheidet, planen Sie die Arbeit in Schichten. Jede Schicht ersetzt einige Hypothesen durch Konstruktionen und Beweise aus grundlegenderen und endet in einem Zustand, der veröffentlicht werden kann. Dies sind die einzigen Hypothesen, die einem Papierergebnis ohne Gegenbeispiel hinzugefügt werden dürfen. Präsentieren Sie eine konditionale Formalisierung niemals als vollständig: Ihr README, formalization.yaml und Bericht sagen, dass sie konditional ist, und listen auf, was sie annimmt.
Flüchtigkeitsfehler in Aussagen. Wenn eine Aussage nur aufgrund eines offensichtlichen Druckfehlers (falscher Index, vertauschter Name, fehlendes - 1) falsch ist und nur eine Lesart beabsichtigt sein kann, formalisieren Sie diese Lesart sofort, sowohl in der Bibliothek als auch in der Challenge. Listen Sie jede solche Korrektur im Bericht und im nächsten Statusbericht an den Benutzer auf. Wenn mehr als eine Korrektur möglich ist, behandeln Sie die Aussage als falsch.
Ein falsches Hilfslemma (eines, das Sie oder ein Entwurf eingeführt haben) benötigt ein konkretes Gegenbeispiel, das in Lean überprüft wird (decide, norm_num oder #eval), wenn möglich. Fügen Sie dann die minimale Hypothese hinzu, aktualisieren Sie seine Aufrufer und dokumentieren Sie die Änderung in der Commit-Nachricht.
Am Ende gibt es kein sorry (außerhalb von Challenge.lean), admit, axiom, native_decide oder implemented_by. native_decide fügt ein Axiom hinzu, das Comparator ablehnt.
Raten Sie niemals einen Mathlib-Namen oder eine Signatur. Durchsuchen Sie die festgelegten Quellen in .lake/packages/mathlib oder verwenden Sie #check, exact? und Loogle. Mathlib benennt und verwirft häufig Deklarationen, und Veraltungswarnungen nennen den Ersatz.
Wenn Sie nicht kompilieren können (keine Toolchain oder der Benutzer verbietet es), schreiben Sie das Lean ohne Kompilierung. Überprüfen Sie jeden Namen, jede Signatur und jeden Importpfad anhand der festgelegten Mathlib-Quellen, halten Sie die Reihenfolge Aussagen-zuerst ein und kennzeichnen Sie jedes Ergebnis als unverifiziert. Wer das Projekt später kompiliert, beginnt bei Phase 3.
Führen Sie jeweils einen lake build pro Checkout aus. Gleichzeitig ausgeführte Builds löschen gegenseitig ihre .olean-Dateien, und ein Editor, der das Projekt geöffnet hat, führt seine eigenen lake setup-file-Builds aus. Wenn Sie „Objektdatei … existiert nicht“ sehen, wiederholen Sie den Vorgang, anstatt das Skript zu umgehen.
Fragen Sie vor jeder Aktion, die andere sehen können: Pushen, Erstellen eines Repositorys, Ändern der Sichtbarkeit eines Repositorys, Öffnen oder Schließen von Pull-Requests, Löschen von Branches, Ausführen von Palomars Preflight, Einreichen bei Palomar, Registrieren. Die Erlaubnis für eine dieser Aktionen ist nicht die Erlaubnis für die anderen.
Autoren sind Menschen. Nennen Sie KI-Systeme im README, in CREDITS.md und im Abschnitt automation von formalization.yaml, niemals als Autoren oder Maintainer.
Führen Sie ein Ausführungsprotokoll von Anfang an (siehe „Ausführungsprotokoll“ unten). Melden Sie es in CREDITS.md, in formalization.yaml und in Statusberichten.

Workflow

Phase	Ziel	Erledigt, wenn
0. Konfigurieren	die Aufgabe dokumentieren, die offenen Fragen stellen	Konfiguration aufgezeichnet
1. Bestandsaufnahme	das Papier kennen: seine Ergebnisse, Definitionen, Konstanten, Zitate und woher deren Beweise kommen können, vermutete Tippfehler	Arbeitscheckliste vollständig
2. Projekt	ein Lean-Projekt auf einem Mathlib-Release, mit dem Modulsystem, gegliedert nach Papierabschnitten	`lake build` läuft
3. Aussagen	jede Definition und jedes nummerierte Ergebnis formuliert, mit `sorry`-Beweisen; die Challenge	Aussagen ausgearbeitet und bestehen eine unabhängige Überprüfung gegen das Papier; Baseline committet
4. Phase 1	alles beweisen, was das Papier beweist, mit den Beweisen des Papiers	nur zitierte Ergebnisse bleiben, als Axiome in `External/`; jede Abweichung gemeldet
5. Phase 2	die zitierten Ergebnisse beweisen	null Axiome; jedes noch angenommene Ergebnis ist eine benannte Hypothese
6. Überprüfen	Axiom-Audit, Abhängigkeitstabelle, Routenprüfung, Solution und Comparator	`scripts/Audit.lean` und die Routenprüfung bestehen; Beweise mit denen des Papiers verglichen; Comparator akzeptiert
7. Bereinigen	keine Warnungen, keine ungenutzten Hypothesen, keine irreführenden Namen, Routen unverändert	der Build zeigt nur die `sorry`s der Challenge; die Routenprüfung besteht weiterhin
8. Prüfung	`REPORT.md`, `README.md`, `CREDITS.md`; die private `NEXT.md`	jeder Befund gegen die TeX-Quelle überprüft; jeder Folgekandidat auf Neuheit und gegen die Messlatte überprüft
9. Verpacken	CI, Palomar-Dateien und -Prüfungen; Veröffentlichung und Preflight, mit Erlaubnis	Palomars lokale Prüfungen bestehen; nach der Veröffentlichung meldet der Preflight `status: pass`

Commit bei jedem Meilenstein, mit einer Nachricht, die sagt, was sich geändert hat und warum.

Phase 0: Konfigurieren

Dokumentieren Sie diese. Fragen Sie den Benutzer nur nach dem, was Sie nicht selbst herausfinden können:

paper:            arXiv-ID und Version (oder DOI); Quell-TeX, falls verfügbar; spätere Version …

… (Fortsetzung folgt im Original)

paper_title: – Titel des Papiers
authors: – Autoren
area: – Mathematikbereich (Algebra, Analysis, Kombinatorik, …)
language: – Sprache des Papiers
statements: – Datei der formalisierten Aussagen (aus Phase 3)
proofs: – Verzeichnis der formalisierten Beweise
lemmata: – Liste der benötigten Lemmata
problems: – Liste der offenen Probleme (E-Punkte)
divergences: – Liste der Abweichungen vom Papier
assumptions: – Liste der angenommenen (nicht bewiesenen) Ergebnisse aus der Literatur
toolchain: – Lean-Version und Mathlib-Release
build: – ob lake build erfolgreich ist
compiled: – ob das Projekt kompiliert werden kann
verified: – ob die Routenprüfung und der Comparator bestehen
published: – ob das Projekt in Palomar veröffentlicht ist
preflight: – ob Palomars Preflight bestanden wurde
run_log: – Pfad zum Ausführungsprotokoll
next_steps: – Liste der nächsten Schritte
notes: – zusätzliche Notizen

Öffnen Sie eine Nachverfolgungsaufgabe für jede offene Frage. Beantworten Sie jede Frage, sobald die Informationen verfügbar sind, und dokumentieren Sie die Antwort.

Phase 1: Bestandsaufnahme

Erstellen Sie eine vollständige Liste aller:

Definitionen
Nummerierte Ergebnisse (Sätze, Lemmata, Korollare, …)
Konstanten (mit Werten, wenn möglich)
Zitate (welche Ergebnisse werden aus der Literatur verwendet)
Vermutete Tippfehler (mit alternativen Lesarten)

Lesen Sie das Papier sorgfältig, einschließlich aller Anhänge und Fußnoten. Überprüfen Sie die Liste mit einem unabhängigen Leser (einem anderen KI-Agenten oder Menschen), um Vollständigkeit und Genauigkeit zu gewährleisten.

# Bestandsaufnahme

## Definitionen

| # | Name | Beschreibung | Seite |
|---|------|--------------|-------|
| 1 | … | … | … |

## Ergebnisse

| # | Name | Typ | Beweismethode | Seite |
|---|------|-----|--------------|-------|
| 1 | … | Satz | … | … |

## Konstanten

| # | Name | Wert | Seite |
|---|------|------|-------|
| 1 | … | … | … |

## Zitate

| # | Ergebnis | Quelle | Status |
|---|----------|--------|--------|
| 1 | … | [arXiv:…] | zu beweisen |

## Tippfehler

| # | Position | Lesart | Alternative |
|---|----------|--------|-------------|
| 1 | S. 3, Zeile 5 | $n+1$ | vielleicht $n-1$ |

Phase 2: Projekt

Erstellen Sie ein Lean-Projekt:

Lakefile.lean mit Abhängigkeit von Mathematik
Mathlib/ als Unterprojekt (oder verlinkt)
External/ für zitierte Ergebnisse aus anderen Quellen
Challenges/ für die Challenge-Datei
Scripts/ für Audit- und Routenprüfungs-Skripte
docs/ für Dokumentation

Struktur nach Papierabschnitten:

project/
├── Lakefile.lean
├── Mathlib/
├── External/
│   ├── SomePaper/
│   │   └── Results.lean
├── Paper/
│   ├── Section1.lean
│   ├── Section2.lean
│   └── Section3.lean
├── Challenges/
│   └── Challenge.lean
├── Scripts/
│   ├── Audit.lean
│   └── RouteCheck.lean
├── docs/
│   ├── README.md
│   ├── REPORT.md
│   └── CREDITS.md
└── formalization.yaml

Phase 3: Aussagen

Formulieren Sie jede Definition und jedes nummerierte Ergebnis aus Phase 1 als Lean-Code. Jede Aussage erhält einen sorry-Beweis:

theorem theorem_name (h : hypothesis) : conclusion :=
  by
    sorry

Fügen Sie eine Challenge.lean-Datei hinzu, die die Hauptergebnisse als Herausforderung enthält (ebenfalls mit sorry).

Überprüfen Sie jede Aussage unabhängig gegen die TeX-Quelle des Papiers, bevor Sie fortfahren. Beheben Sie alle Diskrepanzen.

Phase 4: Phase 1 – Beweise der Papierergebnisse

Beweisen Sie jedes Ergebnis mit dem Argument des Papiers. Verwenden Sie temporäre Axiome in External/ für zitierte Ergebnisse, die noch nicht bewiesen sind.

Dokumentieren Sie jede Abweichung vom Beweis des Papiers sofort im Docstring der Deklaration:

/-- Abweichung vom Papier: 
Das Papier argumentiert wie folgt: … 
Die Formalisierung verwendet stattdessen: …
Grund: …
-/
theorem my_theorem ...

Führen Sie eine Liste der E-Punkte (Lücken im Beweis des Papiers).

Phase 5: Phase 2 – Beweise der zitierten Ergebnisse

Beweisen Sie jedes zitierte Ergebnis, das noch ein Axiom ist. Bauen Sie die benötigte Mathematik in External/ auf, wenn der Aufwand moderat ist. Andernfalls wandeln Sie das Axiom in eine benannte Hypothese um.

Dokumentieren Sie jede konditionale Abhängigkeit in formalization.yaml.

Phase 6: Überprüfen

Führen Sie aus:

Axiom-Audit: scripts/Audit.lean prüft, dass keine unerlaubten Axiome vorhanden sind.
Abhängigkeitstabelle: Visualisieren Sie die Abhängigkeiten zwischen Ergebnissen.
Routenprüfung: Vergleichen Sie die Route des formalen Beweises mit der Route des Papierbeweises.
Solution: Überprüfen Sie, dass die Challenge lösbar ist.
Comparator: Akzeptiert der Comparator das Ergebnis?

Beheben Sie alle Fehler, bevor Sie fortfahren.

Phase 7: Bereinigen

Entfernen Sie alle Warnungen des Lean-Compilers.
Entfernen Sie ungenutzte Hypothesen aus Aussagen.
Benennen Sie Deklarationen um, die irreführende Namen haben.
Stellen Sie sicher, dass die Routen der Beweise unverändert sind.

Phase 8: Prüfung

Erstellen Sie:

REPORT.md: Detaillierte Prüfung des Papiers anhand der Formalisierung, einschließlich:
- Liste der Abweichungen
- Liste der E-Punkte
- Liste der Korrekturen von Druckfehlern
- Analyse der Beweisstärke
- Abschnitt „Was kommt als Nächstes“: Wie das Thema sich entwickelt hat, mögliche Erweiterungen, Verallgemeinerungen, Vereinfachungen.
README.md: Zusammenfassung der Formalisierung, Zielsetzung, Status.
CREDITS.md: Beschreibung des Erstellungsprozesses (KI-Agenten, Modelle, Zeitaufwand).
NEXT.md (privat): Analyse möglicher Folgearbeiten, basierend auf der formalisierten Mathematik.

Phase 9: Verpacken

Fügen Sie CI-Konfiguration hinzu (z.B. GitHub Actions).
Fügen Sie Palomar-Konfigurationsdateien hinzu.
Führen Sie Palomars lokale Prüfungen durch.
Mit Erlaubnis des Benutzers: Veröffentlichen Sie das Projekt bei Palomar und führen Sie den Preflight durch.

Ausführungsprotokoll

Führen Sie ein Protokoll aller Aktionen, Entscheidungen und Probleme, beginnend mit Phase 0. Das Protokoll ist Teil von CREDITS.md und wird in Statusberichten gemeldet.

# Ausführungsprotokoll

| Datum | Phase | Aktion | Entscheidung | Problem | Notiz |
|-------|-------|--------|-------------|--------|-------|
| … | … | … | … | … | … |

Statusberichte

Senden Sie regelmäßig Statusberichte an den Benutzer (nach jeder Phase oder häufiger auf Anfrage). Der Bericht enthält:

Aktuelle Phase und Fortschritt
Liste der offenen Fragen
Liste der Abweichungen und E-Punkte
Liste der Änderungen an Aussagen
Nächste Schritte

Werkzeuge

lake build zum Kompilieren
lean --run scripts/Audit.lean für das Axiom-Audit
lean --run scripts/RouteCheck.lean für die Routenprüfung
git für Versionskontrolle
curl oder wget zum Herunterladen von Papieren
pdftotext oder pandoc zum Extrahieren von Text aus PDFs
detex zum Entfernen von TeX-Markup
grep und sed für Textverarbeitung
jq für JSON-Verarbeitung

Tipps

Lesen Sie das Papier mehrmals, bevor Sie mit der Formalisierung beginnen.
Verwenden Sie exact? in Lean, um Mathlib-Lemmata zu finden.
Verwenden Sie Loogle (https://loogle.lean-lang.org) für die Suche in Mathlib.
Verwenden Sie #check und #print, um Mathlib-Deklarationen zu inspizieren.
Verwenden Sie #eval und norm_num für numerische Berechnungen.
Verwenden Sie dec_trivial und omega für kleine Entscheidungsprobleme.
Verwenden Sie calc für Ketten von Gleichungen.
Verwenden Sie have und let, um Zwischenergebnisse zu benennen.
Verwenden Sie refine und apply, um Beweisziele schrittweise zu verfeinern.
Verwenden Sie simpa und simp, um Ziele mit lokalen Annahmen zu vereinfachen.
Verwenden Sie rename, um Variablen umzubenennen.
Verwenden Sie case für Fallunterscheidungen.
Verwenden Sie induction für Induktionsbeweise.
Verwenden Sie injection für Injektivität von Konstruktoren.
Verwenden Sie exists für Existenzbeweise.
Verwenden Sie constructor für Konjunktionen und Disjunktionen.
Verwenden Sie left und right für Disjunktionen.
Verwenden Sie contradiction zur Ableitung von Widersprüchen.
Verwenden Sie ac_rfl für assoziativ-kommutative Umformungen.
Verwenden Sie ring und field_simp für algebraische Vereinfachungen.
Verwenden Sie positivity für Positivitätsbeweise.
Verwenden Sie nlinarith für nichtlineare Arithmetik.
Verwenden Sie polyrith für polynomiale Gleichungen.

Glossar

Route: Die Liste der Ergebnisse, die der Beweis eines Satzes zitiert, in der Reihenfolge des Papiers.
E-Punkt: Eine Lücke im Beweis des Papiers (das Papier argumentiert fälschlicherweise oder unvollständig).
Abweichung: Eine Änderung des formalen Beweises gegenüber dem Beweis des Papiers, die nicht durch einen E-Punkt verursacht wird.
Konditionale Formalisierung: Eine Formalisierung, die einige zitierten Ergebnisse als Hypothesen annimmt, anstatt sie zu beweisen.
Palomar: Ein Registrierungssystem für Lean-Projekte.
Comparator: Ein Werkzeug, das die Konsistenz einer Formalisierung mit den Regeln überprüft.
Axiom-Audit: Eine Überprüfung, dass keine unerlaubten Axiome vorhanden sind.
Challenge: Eine Datei, die die Hauptergebnisse als Herausforderung enthält.
Solution: Eine Datei, die die Lösung der Challenge enthält.

vltanh/formalize-math-paper

Was ist formalize-math-paper?

In Ihrer bevorzugten KI fragen

Dokumentation