Types de contenu

Sur cette page

Articles scientifiques et livres
Autres — étendre folio-assistant

Cette page est générée à partir de content/docs/content-types/ — chaque section ci-dessous renvoie vers sa propre source.

✎ Edit TR

folio-assistant est indépendant du contenu : la plateforme ne sait rien d’un article ou d’une directive en particulier. Chaque genre de contenu est pris en charge par un adaptateur de contenu (du code qui sait comment valider/construire/restituer ce genre) et un ensemble de compétences (le formalisme de rédaction — ce qu’un auteur et le LLM font).

Cette page décrit le formalisme de chaque type de contenu. Elle est intentionnellement gardée séparée de tout contenu concret ; les artefacts concrets résident dans leur propre dépôt de contenu.

Articles scientifiques et livres

✎ Edit TR

Ensemble de compétences : authoring-math · Adaptateur : paper · Guide : Rédiger un article

Articles scientifiques et livres rigoureux où la prose et les mathématiques sont appuyées par une formalisation Lean 4 vérifiée par machine et restituées via LaTeX.

Un article est un document auquel s’ajoutent des blocs porteurs de Lean. Tout ce qui figure dans la section précédente s’applique ici : le même arbre de blocs, le même graphe éditorial uses[], les mêmes sidecars de QA, le même cycle de vie — ainsi que la voie de rendu Markdown, qui fonctionne lors de la rédaction sur une machine sans TeX. L’adaptateur paper étend l’adaptateur document dans le code, précisément pour cette raison. Ce qu’un article ajoute, ce sont les sept genres ci-dessous dont l’assertion est une affirmation formelle, ainsi que les deux chaînes d’outils qui les vérifient et les composent.

Modèle source — le contenu est un arbre de blocs typés (definition, theorem, lemma, proof, equation, prose, …). Voir la référence de l’API TypeScript pour Block, Chapter et Paper.
Formalisation — les compétences lean-formalization et proof-verification pilotent Lean ; chaque bloc de type théorème peut être suivi par rapport à son équivalent Lean, et chaque sorry est vérifiable.
Rendu — latex-authoring ainsi que les outils paper_render_pdf / paper_render_html de l’adaptateur paper.

Les sept genres qu’un folio de type document ne reçoit pas, et les huit qu’il partage :

Genre de bloc	Préfixe d’étiquette	Lean ?	Profil
`definition`	`def:`	obligatoire	paper uniquement
`theorem` / `lemma` / `proposition` / `corollary`	`thm:` / `lem:` / …	attendu	paper uniquement
`conjecture`	`conj:`	optionnel	paper uniquement
`proof`	`prf:`	optionnel	paper uniquement
`example` / `remark`	`ex:` / `rem:`	optionnel	partagé
`algorithm` / `simulator`	`alg:` / `sim:`	optionnel	partagé
`prose` / `equation` / `diagram` / `table`	`prose:` / `eq:` / `fig:` / `tbl:`	s. o.	partagé

Les quatre lignes « paper uniquement » correspondent à MATH_BLOCK_KINDS dans schemas/block-kinds.ts ; les lignes « partagé » correspondent à DOCUMENT_BLOCK_KINDS, obtenu par complémentarité pour qu’un genre ajouté ultérieurement ne puisse rester non classé.

Deux de ces lignes méritent un second regard. definition constitue le point de démarcation le plus net de toute la séparation — c’est le seul genre dont le champ lean est obligatoire plutôt qu’optionnel, si bien qu’un folio de type document ne pourrait pas en contenir un même si le profil l’autorisait. Et les genres « partagé » continuent de déclarer un lean optionnel : le type autorise ce que le profil interdit, raison pour laquelle content_profile_check comporte une seconde règle au-delà de « ce genre est-il autorisé ? ».

Schémas de compétences pertinents : latex-authoring, lean-formalization, proof-verification.

Autres — étendre folio-assistant

✎ Edit TR

Les nouveaux types de contenu sont de premier ordre : ajoutez un adaptateur de contenu et un ensemble de compétences, et le cycle de vie, le RBAC et la plomberie MCP sont inclus d’office. Voir Ajouter un type de contenu.