Estudio profundo para seminario

¿Qué hace Estudio profundo para seminario?

Una charla de seminario preparada como un estudio profundo de un artículo. Primero el agente ayuda al usuario a elegir el artículo en una discusión interactiva respaldada por evidencia. Luego reescribe el artículo como un resumen en el que cada afirmación lleva su estado de verificación. Rehace los cálculos con un sistema de álgebra computacional (CAS), formaliza la lógica en Lean y registra lo que encuentra en el artículo. Finalmente construye los materiales de la charla a partir de esa única fuente de verdad. El usuario decide; el agente propone con evidencia y verifica todo lo que afirma.

Los archivos incluidos son relativos al directorio base de este skill (se muestra cuando el skill se carga); más abajo se le llama $SKILL. Los archivos del proyecto van al directorio de proyecto del usuario, nunca dentro de $SKILL.

Fases y qué leer

fase	leer primero	deja atrás
0 ingesta	references/intake.md	respuestas en MEMORY.md, decisiones abiertas en PLAN.md
1 ideación de tema	references/ideation.md	el artículo elegido; cada candidato en JOURNAL.md
2 fuente, andamio, resumen	references/digest.md	repositorio, source/SOURCE.md, resumen con registro de hallazgos
3 verificación	references/verification.md, references/lean-palomar.md, references/compute.md	transcripciones CAS, pantallas numéricas, biblioteca Lean, auditoría, registros
4 materiales	references/materials.md, templates/briefs/	notas, diapositivas, plan de pizarra, documento Verso, página de inicio, vault
5 demo en vivo	references/live-demo.md	un archivo de demo ensayado y un plan de respaldo
6 documentación	references/documentation.md	bitácora, plan, memoria, notas del vault, commits
7 publicación	references/publishing.md	nada, a menos que el usuario lo pida en esta sesión
cualquier	references/traps.md	leer antes de trabajar con Lean, clúster, CAS o sitio
artículo de CC	references/computer-science.md	la lectura de ciencias de la computación de las fases 1–5

Las fases son un menú, no una marcha forzada. Una charla solo de lectura son las fases 0–2 más los materiales que necesite; un usuario que llega con un artículo empieza en la fase 0 y se salta la fase 1.

Principios

1. El usuario elige; tú propones con evidencia. Nunca selecciones el artículo, la profundidad o el objetivo de publicación en silencio. Una redirección ("no convence", "algo más reciente") es normal: refina el perfil, así que inicia una nueva ronda en lugar de defender la anterior.
2. Solo fuentes primarias. Verifica el título, autores, fechas, versión, número de páginas y disponibilidad del código en la fuente: la página de resumen de arXiv o su API, el PDF mismo, el repositorio. Etiqueta los anuncios de empresas o la prensa como afirmaciones.
3. Cada número mostrado es calculado, nunca recordado. Los números en diapositivas, páginas y notas provienen de notebooks ejecutados, transcripciones CAS, salidas de Lean o registros de compilación.
4. Una sola fuente de verdad. El resumen es la fuente de verdad matemática. Cada una de sus afirmaciones está etiquetada como [Lean], [CAS], [num], [exp] o [paper]. Las notas, diapositivas, documento Verso y página derivan de él y nunca lo contradicen.
5. El CAS encuentra, el asistente de pruebas verifica. Los certificados van desde las transcripciones CAS a través de un generador (tools/cert2lean.py) a Lean. Los archivos generados se reconstruyen, nunca se editan a mano.
6. Los hechos difíciles pero estándar se convierten en hipótesis explícitas, nunca en axiomas. Registra cada uno en el resumen y en los metadatos de formalización.
7. Los hallazgos son confidenciales por defecto. Los hallazgos sobre un artículo no publicado de otra persona permanecen en el proyecto hasta que el usuario decida. Si hay un error real, sugiere informar primero a los autores.
8. Protege la máquina y los recursos compartidos. Verifica el espacio libre en disco antes de instalar toolchains, nunca ejecutes lake update sin MATHLIB_NO_CACHE_ON_UPDATE=1, y nunca construyas dentro de otros proyectos del usuario. Sigue la etiqueta del clúster en references/compute.md.
9. Un propietario por archivo. Cada subagente escribe solo su propio directorio; tú integras, revisas y haces commit.
10. Las acciones hacia afuera necesitan una solicitud explícita en la sesión actual. Esto incluye desplegar, hacer push, crear un repositorio remoto y publicar un artefacto. Nunca escribas un secreto (contraseña, token, clave privada) en ningún archivo.
11. Busca la jerga del usuario primero en sus propios archivos. Un término desconocido ("clase de registro", un acrónimo de seminario) a menudo está definido en sus notas o proyectos. Busca allí, luego en la web, luego pregunta.

Fase 0: ingesta

Primero inspecciona el entorno de solo lectura, para que las preguntas ofrezcan opciones concretas. Verifica el espacio libre en disco (df -h ~), los toolchains de Lean instalados, el CAS disponible (local o remoto), Python y uv, y cualquier proyecto que el usuario haya nombrado como formato a copiar. Luego pregunta con la herramienta de preguntas (AskUserQuestion en Claude Code): como máximo cuatro preguntas por llamada, de dos a cuatro opciones cada una, la opción recomendada primero y marcada como "(Recomendado)". El banco de preguntas está en references/intake.md; cubre la charla, el tema y la profundidad, el CAS y el cómputo, los entregables, cómo se entrega el dashboard (solo local o en línea, y dónde; ahora o después) y git. Omite lo que el primer mensaje del usuario ya responda y confírmalo en una línea. Registra las respuestas como decisiones fechadas en MEMORY.md; las decisiones abiertas van a PLAN.md como ❓.

Fase 1: ideación de tema (cuando no se da el artículo)

Ejecuta rondas hasta que el usuario elija (references/ideation.md):

1. Construye un perfil de intereses a partir del registro arXiv del usuario (tools/arxiv_scan.py author), los README de sus proyectos actuales y lo que haya dicho. Muéstralo en tres líneas para que pueda corregirlo.
2. Busca en paralelo: búsqueda web de noticias; la API de arXiv en categorías × temas × una ventana de actualidad (tools/arxiv_scan.py scan, luego rank); repositorios de código a través de la API de GitHub y clones superficiales en el área de trabajo (tools/tactic_census.py para código Lean).
3. Verifica cada candidato que presentarás (id, título, autores, fechas, versiones, páginas del PDF, enlace al código). Vuelve a comprobar una afirmación espectacular tú mismo cuando sea económico.
4. Presenta la lista corta en prosa: una recomendación con por qué encaja con el usuario y el formato, dos o tres alternativas con sus ventajas y desventajas, artículos justo fuera de los filtros, noticias que valgan cinco minutos y las fuentes. Termina con una pregunta directa. La herramienta de preguntas es una conveniencia para una elección final nítida; si el usuario la rechaza para aclarar, quiere hablar, así que pregunta qué quiere cambiar.
5. Registra cada candidato y la razón por la que fue descartado; va a JOURNAL.md en el momento del andamio.

Fase 2: fuente, andamio, resumen

Obtén el PDF y la fuente LaTeX en source/ (ignorados por git). Registra la versión y los checksums SHA-256 en source/SOURCE.md. Transcribe fórmulas y listas del LaTeX, nunca de la capa de texto del PDF. Arma el andamio del proyecto con tools/scaffold.py (plantillas de documentación, el resumen y opcionalmente los esqueletos de Lean, CAS, clúster, sitio, diapositivas, libro, Verso y vault). Luego escribe el resumen (templates/digest/digest.md): el resultado en tres líneas, antecedentes, configuración, una sección por teorema con su arquitectura de demostración y etiquetas de estado, el registro de hallazgos (gravedades: confirmado / redacción / hipótesis implícita / fortalecimiento / error) y ejercicios. Detalles: references/digest.md.

Fase 3: verificación

Convierte cada afirmación computacional y cada "se comprueba" en una fila de una tabla de verificación en PLAN.md, luego trabaja en ella:

• primero pantallas numéricas (alta precisión; detectan errores de transcripción, no prueban nada);
• scripts CAS con transcripciones confirmadas, cuyas líneas CHECK deben ser verdaderas; los desacuerdos van al registro de hallazgos (references/verification.md);
• certificados: el CAS imprime bloques CERT, tools/cert2lean.py escribe el archivo Lean, y linear_combination o ring verifican cada identidad; grind puede reprobar los mismos pasos sin certificado, lo que vale la pena mostrar;
• Lean: primero las afirmaciones, luego las demostraciones; ligero o clase Palomar (Challenge.lean/Solution.lean/comparator.json, solo axiomas estándar, auditoría de axiomas con import all, lake comparator --paranoid, compilación sin advertencias, registros). Consulta references/lean-palomar.md y references/compute.md para compilaciones locales versus en clúster y las reglas de espacio en disco.

Trata las advertencias de linter como posibles hallazgos: un argumento de instancia no utilizado puede significar que el teorema es más general de lo que afirma el artículo.

Fase 4: materiales, mediante subagentes paralelos

Lanza un agente en segundo plano por cada entregable, cada uno propietario de su directorio: reverificación CAS, el documento Verso, notas (Jupyter Book), diapositivas con un plan de pizarra, y la página de inicio con su imagen principal y el vault. Completa los briefs en templates/briefs/. Cada brief nombra las fuentes de verdad (el resumen, los archivos Lean, las transcripciones), los hechos que puede afirmar, los comandos que puede ejecutar, y que nunca debe inventar números, nombres, horas o salas. Sigue verificando mientras se ejecutan. Cuando un hecho cambie (un nuevo resultado, un nuevo conteo, una nueva demo), envía a cada agente en ejecución una actualización breve y autocontenida con SendMessage: qué cambió, dónde está, qué agregar, "opcional, mantén tu plan actual". Los agentes recalculan números, por lo que también arbitran el resumen: pídeles que informen cualquier desacuerdo, luego corrige el resumen (con fecha) e informa a los demás. Vigila el disco libre mientras varios agentes se ejecutan. Cuando un agente termine, revisa su salida (compílala, ábrela, toma capturas de pantalla sin interfaz gráfica), enlaza los entregables entre sí y haz commit. Los materiales generados se reconstruyen a partir de sus fuentes: las diapositivas rechazan código que no sea un extracto textual y llevan bibliotecas empaquetadas para que la charla funcione sin conexión. Detalles: references/materials.md.

Fase 5: demo en vivo

Construye un archivo de demo que se ejecute en segundos: #check y #print axioms del teorema principal, un certificado verificado por linear_combination, el mismo hecho probado por grind, y una variante "rómpelo" comentada que falle visiblemente. Ejecútalo localmente, o remotamente a través del comando demo del controlador del clúster. Ensáyalo dos veces y mantén un plan de respaldo (el documento Verso renderizado o capturas de pantalla). Detalles: references/live-demo.md.

Fase 6: documentación y fin de sesión

El proyecto lleva CLAUDE.md (instrucciones de operación), MEMORY.md (hechos y decisiones fechados), JOURNAL.md (entradas fechadas), PLAN.md (✅ hecho · 🟡 en progreso · ⬜ por hacer · ❓ decisión del usuario), MAINTENANCE.md (runbook), README.md y el vault. Al final de cada sesión: añade una entrada en la bitácora, actualiza el plan, agrega notas del vault para nuevos conceptos y decisiones, y haz commit (Conventional Commits). Los archivos de memoria del cliente contienen solo hechos que deberían sobrevivir al proyecto. Detalles: references/documentation.md.

Fase 7: publicación (solo bajo solicitud explícita)

Construye todo localmente primero. Publica solo lo que el usuario pidió, en esta sesión, en el destino elegido en la fase 0: un artefacto privado de Claude, GitHub Pages o un servidor web a través de un script de despliegue de lista blanca con una ejecución en seco, una verificación de enlaces y un escaneo de fugas (tools/leak_scan.py). Un repositorio público recibe un historial nuevo y un escaneo de fugas antes de que el usuario haga push. Detalles: references/publishing.md.

Lista de verificación inicial

1. Preguntas de la fase 0 respondidas, decisiones registradas.
2. Artículo elegido (fase 1) o dado; fuente obtenida y checksum calculado.
3. python3 "$SKILL/tools/scaffold.py" <proyecto> ...; git init; primer commit.
4. Resumen escrito, afirmaciones etiquetadas, tabla de verificación en PLAN.md.
5. Verificación y formalización iniciadas; agentes de materiales lanzados una vez que el resumen es estable.
6. Fin de sesión: bitácora, plan, vault, commit.