Tipos de contenido
TR
Esta página se genera a partir de content/docs/content-types/ — cada sección a continuación enlaza a su propia fuente.
✎ Edit TR
folio-assistant es independiente del contenido: la plataforma no sabe nada sobre ningún artículo o guía en particular. Cada tipo de contenido está respaldado por un adaptador de contenido (código que sabe cómo validar, compilar y renderizar ese tipo) y un paquete de habilidades (el formalismo de autoría: lo que hacen un autor y el LLM).
Esta página describe el formalismo de cada tipo de contenido. Se mantiene intencionalmente separada de cualquier contenido concreto; los artefactos concretos residen en su propio repositorio de contenido.
Artículos científicos y libros
✎ Edit TR
Paquete de habilidades: authoring-math ·
Adaptador: paper ·
Guía: Redacción de un artículo
Artículos científicos y libros rigurosos donde la prosa y las matemáticas están respaldadas por una formalización en Lean 4 verificada por máquina y renderizadas mediante LaTeX.
Un artículo es un documento más bloques con Lean. Todo lo explicado en la sección anterior aplica aquí: el mismo árbol de bloques, el mismo grafo editorial de
uses[], los mismos sidecars de QA, el mismo ciclo de vida —y la ruta de renderizado a Markdown, que funciona mientras se redacta en una máquina sin TeX. El adaptadorpaperextiende el adaptadordocumenten el código, exactamente por esa razón. Lo que añade un artículo son los siete tipos siguientes cuya aseveración es una afirmación formal, y las dos cadenas de herramientas que los verifican y componen tipográficamente.
- Modelo fuente — el contenido es un árbol de bloques tipados (
definition,theorem,lemma,proof,equation,prose, …). Consulta la referencia de la API de TypeScript paraBlock,ChapteryPaper. - Formalización — las habilidades
lean-formalizationyproof-verificationcontrolan Lean; cada bloque de tipo teorema puede rastrearse frente a su contraparte en Lean, y cadasorryes auditable. - Renderizado —
latex-authoringmás las herramientaspaper_render_pdf/paper_render_htmldel adaptador paper.
Los siete tipos que un folio de documento no recibe, y los ocho que comparte:
| Tipo de bloque | Prefijo de etiqueta | ¿Lean? | Perfil |
|---|---|---|---|
definition | def: | obligatorio | solo paper |
theorem / lemma / proposition / corollary | thm: / lem: / … | esperado | solo paper |
conjecture | conj: | opcional | solo paper |
proof | prf: | opcional | solo paper |
example / remark | ex: / rem: | opcional | compartido |
algorithm / simulator | alg: / sim: | opcional | compartido |
prose / equation / diagram / table | prose: / eq: / fig: / tbl: | n/a | compartido |
Las cuatro filas «solo paper» son MATH_BLOCK_KINDS en
schemas/block-kinds.ts;
las filas «compartido» son DOCUMENT_BLOCK_KINDS, derivadas como el complemento de modo que un
tipo añadido posteriormente no pueda quedar sin clasificar.
Dos de esas filas merecen una segunda mirada. definition es el punto más estricto
de toda la división: es el único tipo cuyo campo lean es obligatorio en lugar
de opcional, por lo que un folio de documento no podría contener uno incluso si el perfil
lo permitiera. Y los tipos «compartidos» aún declaran un lean opcional: el tipo
permite lo que el perfil prohíbe, razón por la cual content_profile_check tiene una
segunda regla más allá de «¿está permitido este tipo?».
Esquemas de habilidades pertinentes:
latex-authoring,
lean-formalization,
proof-verification.
Otros — extender folio-assistant
✎ Edit TR
Los nuevos tipos de contenido son de primera clase: agrega un adaptador de contenido y un paquete de habilidades, y el ciclo de vida, RBAC y la infraestructura de MCP vienen incluidos sin costo alguno. Consulta Agregar un tipo de contenido.