userbox020/flux-de-travail-mathematique

Flux de travail mathématique

Résolvez le problème énoncé par l'utilisateur. N'en faites pas un vaste projet de recherche.

Flux de travail

1. Reformulez le problème et identifiez son domaine mathématique. Déterminez si l'utilisateur souhaite une preuve, un calcul, une recherche dans le corpus ou une vérification formelle ; ne clarifiez que les ambiguïtés bloquantes.
2. Utilisez math_search pour les manuscrits et stratégies connexes. Commencez large, puis réduisez par terminologie ou hypothèses. Utilisez math_manuscript pour lire uniquement le résumé, le plan ou la section LaTeX pertinente. Si le source TeX est manquant ou si vous avez besoin du texte publié, utilisez math_pdf_text sur les pages sélectionnées.
3. Pour une preuve, donnez un plan de lemmes avant l'algèbre. Séparez les résultats cités du corpus de la nouvelle déduction, et vérifiez que les hypothèses de chaque résultat cité s'appliquent.
4. Pour une vérification formelle demandée ou un énoncé Lean, utilisez math_lean_search pour localiser les déclarations existantes, math_lean_check sur de petits extraits d'abord, puis math_lean_build pour la cible ciblée. Utilisez math_comparator uniquement lorsqu'une configuration de défi correspondante existe. Ne construisez pas l'intégralité du package par défaut.
5. Pour un travail numérique ou symbolique, utilisez math_compute pour les opérations SymPy autorisées. Sinon, montrez le calcul et indiquez la limitation d'exécution. La preuve numérique ne constitue pas une preuve d'une affirmation exacte.
6. Vérifiez indépendamment les cas limites, les quantificateurs, les hypothèses et les étapes intermédiaires. Confirmez si chaque vérification Lean a réellement réussi et quel énoncé elle a vérifié ; un extrait non lié qui réussit ne vérifie pas le théorème demandé.

Garde-fous du corpus et de la vérification

• math/CONTENTS.md répertorie 721 manuscrits dans 373 familles de résultats. L'archive contient des résultats de recherche bruts, non des résultats certifiés de manière indépendante.
• Actuellement, 175 articles disposent de formalisations Lean ; math/lean/formalization.yaml est le catalogue. La présence dans le catalogue ne certifie pas chaque affirmation d'un article.
• Consultez math/history.md lorsqu'un résultat semble suspect ; il enregistre les révisions et les retraits. Ne vous fiez pas silencieusement à un résultat retiré.
• N'affirmez jamais qu'un article est vérifié simplement parce qu'il est dans le corpus.
• N'affirmez jamais de vérification Lean à moins que l'appel math_lean_check, math_lean_build ou math_comparator concerné n'ait réellement réussi. Signalez explicitement les échecs, les vérifications ignorées, les prérequis manquants et les lacunes restantes.
• math/lean/ est le seul package Lake OAI, épinglé à leanprover/lean4:v4.34.1. Préférez les cibles ciblées comme OAI.Analysis.
• Utilisez math_status pour inspecter la disponibilité actuelle ; ne traitez pas une vérification indisponible comme un succès. Les builds Lean natives Windows peuvent être bloquées par un chemin invalide NTFS dans l'ensemble de dépendances épinglé, et Comparator/landrun nécessitent Linux/WSL. Signalez ces bloqueurs au lieu de changer silencieusement d'affirmation.
• Citez les chemins source relativement à math/, par exemple lean/formalization.yaml, avec les identifiants de manuscrit et les noms de section lorsque disponibles.

Schémas d'utilisation des outils

• Interrogez d'abord largement, puis réduisez ; n'effectuez pas de découverte à l'échelle du dépôt pour une question localisée.
• Lisez les sections pertinentes plutôt que des PDF entiers. Résolvez les chemins PDF publiés à partir des métadonnées plutôt que de supposer un nom de fichier ; utilisez math_pdf_text uniquement pour les pages sélectionnées.
• Préférez math_grep pour les noms ou notations exacts en TeX, Markdown et Lean ; utilisez math_lean_search pour les noms de déclaration. Limitez les recherches aux fichiers ou répertoires pertinents lorsque cela est possible.
• Utilisez math_compute pour les vérifications symboliques, mais indiquez l'opération et vérifiez l'expression renvoyée indépendamment.
• Limitez la sortie : résumez les correspondances et citez uniquement les énoncés ou étapes de preuve nécessaires.
• Utilisez math_reindex après les modifications de math/ lorsque l'index nécessite une actualisation.

Structure de la réponse

1. Théorème / affirmation : énoncé précis, hypothèses et portée.
2. Preuve / déduction : plan de lemmes et étapes justifiées, ou le calcul ou la recherche demandé.
3. Statut de vérification : vérifications réellement effectuées, résultats et limites de leur couverture.
4. Sources : chemins et sections pertinents du corpus ; distinguez les citations du nouveau travail.
5. Lacunes ouvertes : étapes non résolues ou vérifications manquantes, ou aucune identifiée explicitement.