Tipos de contenido

TR

En esta página
  1. Artículos científicos y libros
  2. Otros — extender folio-assistant

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 adaptador paper extiende el adaptador document en 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 para Block, Chapter y Paper.
  • Formalización — las habilidades lean-formalization y proof-verification controlan Lean; cada bloque de tipo teorema puede rastrearse frente a su contraparte en Lean, y cada sorry es auditable.
  • Renderizado — latex-authoring más las herramientas paper_render_pdf / paper_render_html del adaptador paper.

Los siete tipos que un folio de documento no recibe, y los ocho que comparte:

Tipo de bloquePrefijo de etiqueta¿Lean?Perfil
definitiondef:obligatoriosolo paper
theorem / lemma / proposition / corollarythm: / lem: / …esperadosolo paper
conjectureconj:opcionalsolo paper
proofprf:opcionalsolo paper
example / remarkex: / rem:opcionalcompartido
algorithm / simulatoralg: / sim:opcionalcompartido
prose / equation / diagram / tableprose: / eq: / fig: / tbl:n/acompartido

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.


folio-assistant — code under the Apache License 2.0, documentation under CC BY 3.0. Generated schema and API references are rebuilt from source on every push to main.

deployed b08c961 · 2026-10-23T23:11:09Z