Content types
This page is generated from docs/source/concepts-content-types/ — each section below links to its own source.
folio-assistant is content-agnostic: the platform knows nothing about any particular paper or guideline. Each kind of content is supported by a content adapter (code that knows how to validate/build/render that kind) and a skill package (the authoring formalism — what an author and the LLM do).
This page describes the formalism of each content type. It is intentionally kept separate from any concrete content; concrete artifacts live in their own content repository.
Scientific papers & books
Skill package: authoring-math ·
Adapter: paper ·
Guide: Writing a paper
Rigorous scientific papers and books where prose and mathematics are backed by a machine-checked Lean 4 formalization and rendered through LaTeX.
A paper is a document plus Lean-bearing blocks. Everything in the section above applies here: the same block tree, the same editorial
uses[]graph, the same QA sidecars, the same lifecycle — and the Markdown render path, which works while drafting on a machine with no TeX. Thepaperadapter extends thedocumentadapter in code, for exactly that reason. What a paper adds is the seven kinds below whose assertion is a formal claim, and the two toolchains that check and typeset them.
- Source model — content is a tree of typed blocks (
definition,theorem,lemma,proof,equation,prose, …). See the TypeScript API reference forBlock,Chapter, andPaper. - Formalization —
lean-formalizationandproof-verificationskills drive Lean; each theorem-like block can be tracked against its Lean counterpart, and everysorryis auditable. - Rendering —
latex-authoringplus the paper adapter’spaper_render_pdf/paper_render_htmltools.
The seven kinds a document folio does not get, and the eight it shares:
| Block kind | Label prefix | Lean? | Profile |
|---|---|---|---|
definition | def: | required | paper only |
theorem / lemma / proposition / corollary | thm: / lem: / … | expected | paper only |
conjecture | conj: | optional | paper only |
proof | prf: | optional | paper only |
example / remark | ex: / rem: | optional | shared |
algorithm / simulator | alg: / sim: | optional | shared |
prose / equation / diagram / table | prose: / eq: / fig: / tbl: | n/a | shared |
The four paper only rows are MATH_BLOCK_KINDS in
schemas/block-kinds.ts;
the shared rows are DOCUMENT_BLOCK_KINDS, derived as the complement so a
kind added later cannot go unclassified.
Two of those rows are worth a second look. definition is the sharpest point
of the whole split — it is the one kind whose lean field is required rather
than optional, so a document folio could not hold one even if the profile
allowed it. And the shared kinds still declare an optional lean: the type
permits what the profile forbids, which is why content_profile_check has a
second rule beyond “is this kind allowed”.
Relevant skill schemas:
latex-authoring,
lean-formalization,
proof-verification.
Others — extending folio-assistant
New content types are first-class: add a content adapter and a skill package, and the lifecycle, RBAC, and MCP plumbing come for free. See Adding a content type.