vltanh/formalize-math-paper

Formalización de un artículo de matemáticas en Lean 4

Entregas un proyecto Lean, con documentos adjuntos, en el que:

• cada resultado que demuestra el artículo se prueba con el argumento propio del artículo. Una demostración se aparta del artículo solo cuando es necesario, y cada desviación se informa (Reglas, "Demostraciones fieles");
• cada resultado que el artículo cita en sus demostraciones también se demuestra: en Mathlib, en otra biblioteca pública, o en External/. Un resultado citado puede requerir matemáticas que ninguna biblioteca Lean tiene aún y que el proyecto no puede construir razonablemente. Dicho resultado se convierte en una hipótesis con nombre de cada enunciado que lo usa, y la formalización declara claramente que es condicional;
• los enunciados dicen lo que dice el artículo, y toda desviación se documenta;
• lake build se ejecuta sin sorry (excepto en los enunciados de Challenge.lean, por diseño), sin admit y sin axiom del proyecto. Toda declaración de la biblioteca depende solo de propext, Classical.choice y Quot.sound;
• REPORT.md audita el artículo contra la formalización. Termina con lo que sigue: cómo se ha desarrollado el tema desde el artículo, cómo se podrían extender, generalizar o reforzar sus resultados, y cómo se podrían simplificar sus demostraciones. README.md resume la formalización, y CREDITS.md explica cómo se hizo: el procedimiento, los agentes y modelos, y el tiempo y esfuerzo (el registro de ejecución);
• un NEXT.md privado, que nunca se publica a menos que el usuario lo pida, responde qué artículo podría escribir el usuario a continuación siguiendo este: algunos candidatos que cada uno daría lugar a un artículo propio, explorados en profundidad (el obstáculo, los intentos, la evidencia, lo que ya está demostrado), no una lista de extensiones incrementales;
• el proyecto está empaquetado para Palomar y, con el permiso del usuario, se publica y se ejecuta a través de la verificación previa de Palomar.

El trabajo tiene dos etapas. En la Etapa 1, formaliza todo lo que demuestra el propio artículo. Los resultados que toma de la literatura pueden ser axiomas temporales. En la Etapa 2, elimina esos axiomas: demuéstralos, o convierte los que están fuera de alcance en hipótesis declaradas. La configuración viene antes de las dos etapas, y la verificación, limpieza, auditoría y empaquetado vienen después.

Principios

Estos explican las reglas siguientes. Úsalos cuando ninguna regla cubra una situación.

• El artículo es la fuente de verdad para los enunciados y argumentos; Lean juzga la corrección. Un enunciado que difiere del artículo es una formalización incorrecta, por muy limpia que sea su demostración. También lo es una demostración que alcanza el enunciado del artículo mediante otro argumento: la formalización comprueba las demostraciones del artículo, no solo sus afirmaciones. Revisa los enunciados contra la fuente TeX antes de que alguien los demuestre. Compara las demostraciones con las del artículo una vez escritas. Nunca cambies ninguna de ellas en silencio.
• Una formalización que nadie ha compilado es un borrador. El Lean escrito de memoria y nunca compilado a menudo tiene nombres de lemas adivinados, firmas incorrectas y lemas auxiliares falsos. Compila siempre que haya una cadena de herramientas Lean disponible. Si no la hay, o el usuario prohíbe compilar, di claramente que el resultado no está verificado.
• "Estándar", "obvio", "por simetría", "rutinario" aún necesitan demostraciones. Mathlib puede tener el hecho; si no, demuéstralo. Solo lo que el propio artículo toma de otra fuente puede convertirse en un axioma.
• Externo significa de dónde viene un resultado, no que sea de confianza. Un resultado citado vive en External/ por su fuente. Se demuestra como todo lo demás.
• Una suposición es una suposición, sea cual sea su forma. Un resultado citado que no se demuestra se supone, ya sea escrito como axioma, hipótesis o campo de una estructura. Los axiomas no están permitidos. Las hipótesis están permitidas cuando un lector del enunciado puede ver cada una, bajo el nombre del resultado que supone. Una estructura que mezcla datos con teoremas supuestos oculta de qué depende un resultado. También lo hace un parámetro cuyo tipo parece datos pero contiene un teorema.
• Los datos vienen con su propiedad definitoria. Cuando un enunciado toma un objeto del artículo como parámetro en lugar de construirlo, también debe exigir la propiedad que define el objeto. De lo contrario, el teorema trata sobre todo objeto que satisfaga las demás hipótesis, lo cual es un enunciado diferente.
• Las opciones de representación necesitan puentes. Los objetos de Lean pueden diferir de los del artículo: índices desde 0 en lugar de 1, listas en lugar de familias indexadas, una estructura Mathlib empaquetada en lugar de un objeto informal, un modelo concreto en lugar de una descripción "salvo isomorfismo". Cuando sea así, demuestra un lema que conecte los dos y documenta la elección. Nunca asumas que dos representaciones son equivalentes.
• Las constantes y los rangos son parte de las matemáticas. Potencias, factores, suelos, techos, desigualdades estrictas frente a débiles, los extremos de los rangos y la resta truncada en ℕ deciden si un enunciado es verdadero.
• Informa honestamente. Si se omitió un paso, falla una demostración, un enunciado tuvo que cambiar o una demostración tuvo que apartarse del artículo, dilo y da la razón. La auditoría es útil solo si se puede confiar.
• Un vacío en una demostración no es un enunciado falso. Cuando la demostración del artículo usa un hecho que sus hipótesis no proporcionan, el enunciado aún puede ser verdadero. Busca un argumento correcto antes de concluir nada sobre el enunciado.
• Mide el trabajo. Los lectores y los registros preguntan cómo se hizo una formalización. La respuesta es barata de registrar sobre la marcha y difícil de reconstruir después.

Reglas

• Nunca debilites ni cambies el enunciado de un resultado del artículo para que funcione una demostración. Si el enunciado del artículo es falso, deja de trabajar en él e informa al usuario de inmediato, con el contraejemplo. Otro trabajo puede continuar mientras tanto. Si el usuario está de acuerdo, formaliza la versión correcta más cercana y regístrala como un error en el informe. Las erratas obvias son la única excepción (a continuación).

• Nunca añadas una hipótesis a un resultado del artículo porque su demostración parezca necesitarla. Añadir una debilita el resultado. Añade una solo cuando el enunciado mismo tenga un contraejemplo, no porque falle un paso de la demostración, y luego sigue la regla anterior. De lo contrario, demuestra el enunciado tal como está impreso, mediante un argumento corregido, y registra el vacío en la demostración como un elemento E. Si no encuentras ni una demostración ni un contraejemplo, informa al usuario de lo que falta. Ellos deciden si seguir trabajando o formalizar un enunciado más débil, documentado como una desviación.

• Demostraciones fieles. Demuestra cada resultado mediante la demostración del artículo: las mismas afirmaciones intermedias, las mismas construcciones y divisiones en casos, y los mismos resultados anteriores donde el artículo los cita. Los resultados que la demostración del artículo cita forman su ruta. La demostración formal debe tener la misma ruta, y la comprobación de ruta (Fase 6) lo verifica. Solo la mecánica puede diferir: tácticas, el lema de Mathlib que cierra un paso rutinario, el orden de los pasos independientes, y lemas auxiliares que empaquetan un paso del artículo. Si Mathlib demuestra por casualidad un resultado numerado, demuéstralo de todos modos con el argumento del artículo, a menos que el propio artículo lo trate como conocido (lo cita o lo llama estándar).

• Apártate de la demostración del artículo solo cuando sea necesario, es decir, por una de estas razones y ninguna otra:

  1. el argumento del artículo es incorrecto en ese paso, o tiene un vacío allí, y no se puede reparar siguiendo sus propias líneas (el paso también es un elemento E);
  2. el paso necesita matemáticas que Lean no tiene y que el proyecto no puede construir razonablemente (como para resultados citados fuera de alcance, a continuación), y otro argumento lo evita;
  3. el paso no tiene significado en una representación que la formalización debe usar (Principios), por lo que una traducción fiel del mismo es un argumento diferente.

  Una demostración más corta, más elegante, más general o más automática no es una razón. Tampoco lo es una demostración que sea más fácil de formalizar o más rápida de construir. Un argumento más simple que encuentres aún vale la pena conservarlo: regístralo, con un esbozo, para la sección "Qué sigue" del informe (Fase 8), y demuestra el resultado con el argumento del artículo. Apártate tan poco como requiera la razón: repara el paso, no la demostración. Si una desviación reemplazaría todo el argumento de un resultado numerado, no solo un paso, propónselo primero al usuario, con la razón. Otro trabajo continúa mientras tanto.

• Informa toda desviación, siempre. Para cada una, registra lo que hace el artículo, lo que hace la formalización en su lugar, y qué razón obliga al cambio. Regístralo en el docstring de la declaración ("Desviación del artículo: …"), en la tabla de desviaciones del informe, en formalization.yaml (fidelity.divergences), en cualquier texto complementario, en el archivo de diferencias registradas de la comprobación de ruta cuando la ruta cambia, y en el próximo informe de estado. Una desviación que falte en cualquiera de estos es un defecto: encuéntrala y corrígela como lo harías con un enunciado que se cambió en silencio.

• Resultados citados fuera de alcance. Un resultado citado puede necesitar matemáticas que ninguna biblioteca Lean tiene. Si construir esas matemáticas en el proyecto es un esfuerzo moderado, constrúyelas. De lo contrario, el valor predeterminado es una formalización condicional: el resultado se convierte en una hipótesis con nombre de todo enunciado cuya demostración lo use. Aplica el valor predeterminado sin preguntar e infórmalo en el próximo informe de estado. Pregunta al usuario solo cuando construir las matemáticas faltantes sería un esfuerzo grande pero factible: si gastar ese esfuerzo es su decisión. Mientras tanto, continúa el otro trabajo bajo el valor predeterminado. Si eligen construirlo, planifica el trabajo por capas. Cada capa reemplaza algunas hipótesis con construcciones y demostraciones a partir de otras más básicas, y termina en un estado que se puede publicar. Estas hipótesis son las únicas que se pueden añadir a un resultado del artículo sin un contraejemplo. Nunca presentes una formalización condicional como completa: su README, formalization.yaml e informe dicen que es condicional y enumeran lo que supone.

• Erratas en los enunciados. Si un enunciado es falso solo por una errata obvia (un índice incorrecto, un nombre intercambiado, un - 1 faltante), y solo una lectura puede ser la intencionada, formaliza esa lectura de inmediato, tanto en la biblioteca como en el Desafío. Enumera cada corrección en el informe y en el próximo informe de estado al usuario. Cuando sea posible más de una corrección, trata el enunciado como falso.

• Un lema auxiliar falso (uno que tú o un borrador introdujeron) necesita un contraejemplo concreto, verificado en Lean (decide, norm_num o #eval) cuando sea posible. Luego añade la hipótesis mínima, actualiza sus llamantes y registra el cambio en el mensaje de commit.

• Al final no hay sorry (fuera de Challenge.lean), admit, axiom, native_decide ni implemented_by. native_decide añade un axioma, que Comparator rechaza.

• Nunca adivines un nombre o firma de Mathlib. Busca en las fuentes fijadas en .lake/packages/mathlib, o usa #check, exact? y Loogle. Mathlib a menudo renombra y depreca declaraciones, y los avisos de deprecación nombran el reemplazo.

• Si no puedes compilar (sin cadena de herramientas, o el usuario lo prohíbe), escribe el Lean sin compilarlo. Verifica cada nombre, firma y ruta de importación contra las fuentes Mathlib fijadas, mantén el orden de enunciados primero, y etiqueta cada resultado como no verificado. Quien compile el proyecto más tarde comienza en la Fase 3.

• Ejecuta un lake build a la vez por checkout. Las compilaciones que se ejecutan al mismo tiempo eliminan los archivos .olean del otro, y un editor abierto en el proyecto ejecuta sus propias compilaciones lake setup-file. Si ves "el archivo objeto … no existe", reintenta en lugar de editar para evitarlo.

• Pregunta antes de cualquier acción que otros puedan ver: hacer push, crear un repositorio, cambiar la visibilidad de un repositorio, abrir o cerrar pull requests, eliminar ramas, ejecutar la verificación previa de Palomar, enviar a Palomar, registrar. El permiso para una de estas no es permiso para las demás.

• Los autores son personas. Atribuye a los sistemas de IA en el README, en CREDITS.md y en la sección automation de formalization.yaml, nunca como autores o mantenedores.

• Mantén un registro de ejecución desde el inicio (ver "Registro de ejecución" a continuación). Reporta en CREDITS.md, en formalization.yaml y en los informes de estado.

Flujo de trabajo

Fase	Objetivo	Hecho cuando
0. Configurar	registrar la tarea, hacer las preguntas abiertas	configuración registrada
1. Inventario	conocer el artículo: sus resultados, definiciones, constantes, citas y de dónde pueden venir sus demostraciones, erratas sospechadas	lista de verificación de trabajo completa
2. Proyecto	un proyecto Lean sobre una versión de Mathlib, con el sistema de módulos, organizado por sección del artículo	lake build se ejecuta
3. Enunciados	todo definición y resultado numerado enunciado, con demostraciones sorry; el Desafío	los enunciados se elaboran y pasan una revisión independiente contra el artículo; línea base confirmada
4. Etapa 1	demostrar todo lo que demuestra el artículo, mediante las demostraciones del artículo	solo quedan resultados citados, como axiomas en External/; cada desviación informada
5. Etapa 2	demostrar los resultados citados	cero axiomas; todo resultado aún supuesto es una hipótesis con nombre
6. Verificar	auditoría de axiomas, tabla de dependencias, comprobación de ruta, Solución y Comparator	scripts/Audit.lean y la comprobación de ruta pasan; demostraciones comparadas con las del artículo; Comparator acepta
7. Limpiar	sin advertencias, sin hipótesis no usadas, sin nombres engañosos, rutas sin cambios	la compilación muestra solo los sorry del Desafío; la comprobación de ruta sigue pasando
8. Auditar	REPORT.md, README.md, CREDITS.md; el NEXT.md privado	cada hallazgo verificado contra la fuente TeX; cada candidato de seguimiento verificado por novedad y contra el estándar
9. Empaquetar	CI, archivos y comprobaciones de Palomar; publicación y verificación previa, con permiso	las comprobaciones locales de Palomar pasan; después de la publicación, el preflight informa status: pass

Confirma en cada hito, con un mensaje que diga qué cambió y por qué.

Fase 0: Configurar

Registra estos. Pregunta al usuario solo sobre lo que no puedas resolver tú mismo:

paper:            arXiv id y versión (o DOI); TeX fuente si está disponible; versiones posteriores si las hay
title:            título del artículo
authors:          autores (con afiliaciones y ORCID cuando se publiquen)
results:          lista de resultados numerados (lemas, proposiciones, teoremas, corolarios, etc.)
definitions:      lista de definiciones numeradas
constants:        constantes y sus valores numéricos exactos
citations:        lista de resultados citados, con su fuente (artículo, libro, Mathlib, etc.)
  - source:        referencia completa (arXiv, DOI, ISBN, etc.)
  - statement:     enunciado tal como aparece en la cita
  - needed:        para qué resultados del artículo se usa
  - status:        unknown, en Mathlib, en proyecto (especificar), hipótesis (dar nombre) o fuera de alcance
obvious_misprints: lista de erratas obvias encontradas hasta ahora
questions:        preguntas abiertas para el usuario

Fase 1: Inventario

Tu objetivo es una lista de verificación, no código. Léela, extrae los resultados y constantes, y completa la tabla. Para cada resultado citado, busca en Mathlib y en bibliotecas conocidas. Si el artículo está en un campo del que no sabes nada, dilo. Luego pasa a la Fase 2 y haz preguntas solo si no puedes continuar.

Fase 2: Proyecto

Crea el proyecto con lake new. Elige la versión más reciente de Mathlib que esté en el canal stable. No uses master. Organiza las fuentes como:

MyPaper/
├── lakefile.lean
├── lean-toolchain
├── MyPaper/
│   ├── Section1/
│   │   ├── Basic.lean
│   │   └── …
│   ├── …
│   ├── SectionN/
│   │   └── …
│   └── Challenge.lean
├── External/           # solo demostraciones de resultados citados
│   └── …
├── scripts/
│   ├── Audit.lean
│   ├── RouteCheck.lean
│   └── …
├── README.md
├── REPORT.md
├── CREDITS.md
├── NEXT.md
├── formalization.yaml
├── .github/workflows/…
└── palomar.toml

Challenge.lean contiene cada resultado numerado del artículo como un teorema, sin demostración (sorry). Su propósito es que cualquiera pueda ver el enunciado y empezar a demostrarlo. Los sorry del Desafío son el único lugar donde se permiten.

Fase 3: Enunciados

Pega los enunciados del artículo, con exactitud. Traduce nombres de variables y referencias a la notación de Lean. Usa set_option pp.notation false cuando evite ambigüedades. Revisa cada enunciado contra el TeX.

Para cada resultado numerado, crea una declaración con un docstring que copie el enunciado del artículo como texto (en español). Si el artículo enuncia el resultado en un bloque, copia ese bloque. Si lo enuncia en prosa, parafrasea fielmente.

/-!
## Teorema 3.2 (Nombre si lo tiene)

Enunciado del artículo: …
-/
theorem theorem_3_2 {α β : Type} [h : Hipotético] : … :=
  sorry

Los enunciados pueden necesitar ajustes a la notación de Lean, pero la matemática debe ser la misma. Cuando difieran, registra un elemento de discrepancia y explica por qué en el docstring.

Fase 4: Etapa 1

Demuestra todo lo que el artículo demuestra. Usa la demostración del artículo. Si una demostración es corta, escríbela directamente. Si es larga, estructúrala como una secuencia de lemas auxiliares. Para cada desviación, sigue las reglas.

Fase 5: Etapa 2

Para cada axioma en External/:

• Búscalo en Mathlib,
• Si está, sustitúyelo por la importación,
• Si no está, decídete: (a) demuéstralo aquí, (b) conviértelo en hipótesis,
• (a) solo si es factible en una semana de trabajo; si no, (b).

Fase 6: Verificar

Ejecuta scripts/Audit.lean, que comprueba que no hay sorry, admit, axiom, native_decide ni implemented_by. Ejecuta scripts/RouteCheck.lean para verificar que cada demostración sigue la ruta del artículo. Si falla, arregla las desviaciones que faltan.

Fase 7: Limpiar

Elimina advertencias, hipótesis no usadas, nombres engañosos. Mantén las rutas sin cambios. Vuelve a ejecutar la comprobación de ruta.

Fase 8: Auditar

Escribe REPORT.md:

• Resumen de la formalización,
• Tabla de resultados y su estado (demostrado, hipótesis, error),
• Tabla de desviaciones,
• Sección "Qué sigue": extensiones, generalizaciones, simplificaciones,
• Análisis de posibles artículos posteriores (NEXT.md).

Escribe README.md como una guía para lectores humanos.

Escribe CREDITS.md con la atribución adecuada.

Fase 9: Empaquetar

Configura CI (GitHub Actions) para que ejecute lake build y los scripts. Añade palomar.toml con metadatos. Con permiso, publica y ejecuta el preflight.

Preguntas y registro

Haz preguntas al usuario como mensajes separados, no como parte de un informe de estado. Espera respuesta antes de continuar cuando sea necesario. Mantén un registro de ejecución en formato:

[timestamp] Fase X: descripción de la acción, resultado, tiempo empleado

Y al final, en CREDITS.md, presenta el registro completo.