userbox020/math-workflow

Flujo de trabajo matemático

Resuelve el problema declarado por el usuario. No lo conviertas en un proyecto de investigación amplio.

Flujo de trabajo

1. Reformula el problema e identifica su dominio matemático. Determina si el usuario desea una prueba, un cálculo, una búsqueda en el corpus o una verificación formal; aclara solo ambigüedades que bloqueen el avance.
2. Usa math_search para buscar manuscritos y estrategias relacionadas. Empieza de manera amplia y luego reduce por terminología o hipótesis. Usa math_manuscript para leer solo el resumen, el esquema o la sección LaTeX relevante. Si falta el código fuente TeX o necesitas la redacción publicada, usa math_pdf_text en páginas seleccionadas.
3. Para una prueba, proporciona un plan de lemas antes del álgebra. Separa los resultados citados del corpus de la nueva derivación y verifica que las hipótesis de cada resultado citado se apliquen.
4. Para una verificación formal solicitada o una declaración en Lean, usa math_lean_search para localizar declaraciones existentes, math_lean_check primero en fragmentos pequeños y luego math_lean_build para el objetivo concreto. Usa math_comparator solo cuando exista una configuración de desafío coincidente. No construyas todo el paquete por defecto.
5. Para trabajo numérico o simbólico, usa math_compute para operaciones de SymPy en lista blanca. De lo contrario, muestra el cálculo e indica la limitación de ejecución. La evidencia numérica no es una prueba de una afirmación exacta.
6. Verifica de forma independiente casos límite, cuantificadores, hipótesis y pasos intermedios. Confirma si cada comprobación Lean realmente pasó y qué declaración comprobó; un fragmento irrelevante que pasa no verifica el teorema solicitado.

Guardas del corpus y verificación

• math/CONTENTS.md asigna 721 manuscritos en 373 familias de resultados. El archivo contiene resultados de investigación en bruto, no resultados certificados de forma independiente.
• Actualmente 175 artículos tienen formalizaciones en Lean; math/lean/formalization.yaml es el catálogo. La presencia en el catálogo no certifica todas las afirmaciones de un artículo.
• Revisa math/history.md cuando un resultado parezca sospechoso; registra revisiones y retiradas. No confíes en silencio en un resultado retirado.
• Nunca afirmes que un artículo está verificado solo porque está en el corpus.
• Nunca afirmes verificación en Lean a menos que la invocación relevante de math_lean_check, math_lean_build o math_comparator haya tenido éxito. Informa explícitamente sobre fallos, comprobaciones omitidas, requisitos previos faltantes y brechas restantes.
• math/lean/ es el único paquete Lake OAI, anclado a leanprover/lean4:v4.34.1. Prefiere objetivos concretos como OAI.Analysis.
• Usa math_status para inspeccionar la disponibilidad actual; no trates una comprobación no disponible como un éxito. Las compilaciones nativas de Lean en Windows pueden bloquearse por una ruta no válida en NTFS dentro del conjunto de dependencias ancladas, y Comparator/landrun requieren Linux/WSL. Informa sobre estos bloqueadores en lugar de cambiar silenciosamente las afirmaciones.
• Cita las rutas de origen relativas a math/, por ejemplo lean/formalization.yaml, con identificadores de manuscrito y nombres de sección cuando estén disponibles.

Patrones de uso de herramientas

• Consulta primero de forma amplia, luego reduce; no realices descubrimiento a nivel de repositorio para una pregunta localizada.
• Lee secciones relevantes en lugar de PDFs completos. Resuelve las rutas de PDF publicados a partir de metadatos en lugar de asumir un nombre de archivo; usa math_pdf_text solo para páginas seleccionadas.
• Prefiere math_grep para nombres o notaciones exactas en TeX, Markdown y Lean; usa math_lean_search para nombres de declaraciones. Limita las búsquedas a archivos o directorios relevantes cuando sea posible.
• Usa math_compute para comprobaciones simbólicas, pero indica la operación y verifica la expresión devuelta de forma independiente.
• Mantén la salida acotada: resume las coincidencias y cita solo las declaraciones o pasos de prueba necesarios.
• Usa math_reindex después de cambios en math/ cuando el índice necesite actualizarse.

Forma de la respuesta

1. Teorema / afirmación: declaración precisa, supuestos y alcance.
2. Prueba / derivación: plan de lemas y pasos justificados, o el cálculo o búsqueda solicitados.
3. Estado de verificación: comprobaciones realmente ejecutadas, resultados y límites de su cobertura.
4. Fuentes: rutas y secciones relevantes del corpus; distingue citas de trabajo nuevo.
5. Brechas abiertas: pasos no resueltos o comprobaciones faltantes, o explícitamente ninguna identificada.