userbox020/math-workflow

Mathe-Workflow

Löse das vom Benutzer angegebene Problem. Mache daraus kein breites Forschungsprojekt.

Workflow

1. Formuliere das Problem neu und identifiziere seine mathematische Domäne. Bestimme, ob der Benutzer einen Beweis, eine Berechnung, eine Korpusabfrage oder eine formale Verifikation wünscht; kläre nur blockierende Unklarheiten.
2. Verwende math_search, um verwandte Manuskripte und Strategien zu finden. Beginne breit, dann verfeinere nach Terminologie oder Hypothesen. Verwende math_manuscript, um nur die relevanten Abstract, Gliederungen oder LaTeX-Abschnitte zu lesen. Wenn die TeX-Quelle fehlt oder du die Wortwahl der Veröffentlichung benötigst, verwende math_pdf_text für ausgewählte Seiten.
3. Gib für einen Beweis zuerst einen Lemma-Plan, bevor du mit der Algebra beginnst. Trenne Ergebnisse, die aus dem Korpus zitiert werden, von der neuen Herleitung und prüfe, dass die Hypothesen jedes zitierten Ergebnisses zutreffen.
4. Verwende für eine angeforderte formale Verifikation oder eine Lean-Aussage zuerst math_lean_search, um vorhandene Deklarationen zu finden, math_lean_check für kleine Codeausschnitte, dann math_lean_build für das fokussierte Ziel. Verwende math_comparator nur, wenn eine passende Challenge-Konfiguration existiert. Baue standardmäßig nicht das gesamte Paket.
5. Verwende für numerische oder symbolische Arbeit math_compute für auf der Whitelist stehende SymPy-Operationen. Andernfalls zeige die Berechnung und nenne die Ausführungsbeschränkung. Numerische Evidenz ist kein Beweis einer exakten Behauptung.
6. Überprüfe unabhängig Randfälle, Quantoren, Hypothesen und Zwischenschritte. Bestätige, ob jeder Lean-Check tatsächlich bestanden wurde und welche Aussage er überprüft hat; ein bestandener, nicht zusammenhängender Codeausschnitt verifiziert nicht das angeforderte Theorem.

Korpus- und Verifikations-Schutzmechanismen

• math/CONTENTS.md bildet 721 Manuskripte in 373 Ergebnisgruppen ab. Das Archiv enthält rohe Forschungsergebnisse, keine unabhängig zertifizierten Resultate.
• Derzeit haben 175 Arbeiten Lean-Formalisierungen; math/lean/formalization.yaml ist der Katalog. Die Anwesenheit im Katalog zertifiziert nicht jede Behauptung in einer Arbeit.
• Prüfe math/history.md, wenn ein Ergebnis verdächtig erscheint; es dokumentiert Revisionen und Rücknahmen. Verlasse dich nicht stillschweigend auf ein zurückgezogenes Ergebnis.
• Behaupte niemals, dass eine Arbeit verifiziert ist, nur weil sie im Korpus ist.
• Behaupte niemals eine Lean-Verifikation, es sei denn, der entsprechende Aufruf von math_lean_check, math_lean_build oder math_comparator war tatsächlich erfolgreich. Berichte explizit über Fehlschläge, ausgelassene Prüfungen, fehlende Voraussetzungen und verbleibende Lücken.
• math/lean/ ist das einzige Lake-Paket OAI, festgelegt auf leanprover/lean4:v4.34.1. Bevorzuge fokussierte Ziele wie OAI.Analysis.
• Verwende math_status, um die aktuelle Verfügbarkeit zu prüfen; behandle eine nicht verfügbare Prüfung nicht als Erfolg. Native Windows-Lean-Builds können durch einen NTFS-ungültigen Pfad in den festgelegten Abhängigkeiten blockiert werden, und Comparator/landrun benötigen Linux/WSL. Melde solche Blockaden, anstatt stillschweigend die Behauptung zu wechseln.
• Zitiere Quellpfade relativ zu math/, z. B. lean/formalization.yaml, mit Manuskriptkennungen und Abschnittsnamen, sofern verfügbar.

Tool-Nutzungsmuster

• Frage zuerst breit, dann verfeinere; führe keine Repos-weite Suche für eine lokalisierte Frage durch.
• Lies relevante Abschnitte anstelle ganzer PDFs. Löse die Pfade für veröffentlichte PDFs aus Metadaten auf, anstatt einen Dateinamen anzunehmen; verwende math_pdf_text nur für ausgewählte Seiten.
• Bevorzuge math_grep für exakte Namen oder Notation in TeX, Markdown und Lean; verwende math_lean_search für Deklarationsnamen. Beschränke Suchen nach Möglichkeit auf relevante Dateien oder Verzeichnisse.
• Verwende math_compute für symbolische Prüfungen, nenne aber die Operation und überprüfe den zurückgegebenen Ausdruck unabhängig.
• Halte die Ausgabe begrenzt: Fasse Treffer zusammen und zitiere nur die benötigten Aussagen oder Beweisschritte.
• Verwende math_reindex nach Änderungen an math/, wenn der Index aktualisiert werden muss.

Antwortstruktur

1. Theorem / Behauptung: präzise Aussage, Annahmen und Geltungsbereich.
2. Beweis / Herleitung: Lemma-Plan und begründete Schritte oder die angeforderte Berechnung oder Suche.
3. Verifikationsstatus: tatsächlich durchgeführte Prüfungen, Ergebnisse und deren Abdeckungsgrenzen.
4. Quellen: relevante Korpuspfade und Abschnitte; unterscheide Zitate von neuer Arbeit.
5. Offene Lücken: nicht aufgelöste Schritte oder fehlende Prüfungen, oder explizit keine identifiziert.