Типы контента

На этой странице

Научные статьи и книги
Другие — расширение folio-assistant

Эта страница сгенерирована из content/docs/content-types/ — каждый раздел ниже ссылается на собственный исходный файл.

✎ Edit TR

folio-assistant не зависит от контента: платформе ничего не известно о какой-либо конкретной статье или руководстве. Каждый вид контента поддерживается адаптером контента (код, который умеет валидировать, собирать и отображать этот вид) и пакетом навыков (формализм создания — то, что делают автор и LLM).

На этой странице описан формализм каждого типа контента. Он намеренно отделен от какого-либо конкретного контента; конкретные артефакты располагаются в собственном репозитории контента.

Научные статьи и книги

✎ Edit TR

Пакет навыков: authoring-math · Адаптер: paper · Руководство: Написание статьи

Строгие научные статьи и книги, где текст и математические выкладки подкреплены формализацией в Lean 4, проверенной машиной, и сверстаны с помощью LaTeX.

Статья — это документ плюс блоки с поддержкой Lean. Всё из предыдущего раздела применимо и здесь: то же дерево блоков, тот же редакторский граф uses[], те же сайдкары QA, тот же жизненный цикл — а также путь рендеринга в Markdown, который работает при подготовке черновика на компьютере без установленного TeX. Адаптер paper расширяет адаптер document в коде именно по этой причине. Статья добавляет семь приведенных ниже видов блоков, утверждения которых представляют собой формальные утверждения, и две инструментальные цепочки, которые проверяют их и выполняют верстку.

Исходная модель — контент представляет собой дерево типизированных блоков (definition, theorem, lemma, proof, equation, prose, …). См. справочник по API TypeScript для Block, Chapter и Paper.
Формализация — навыки lean-formalization и proof-verification управляют Lean; каждый блок типа теоремы можно сопоставить с его аналогом в Lean, при этом каждый sorry подлежит аудиту.
Рендеринг — latex-authoring плюс инструменты адаптера paper paper_render_pdf / paper_render_html.

Семь видов, которые фолио документов не получает, и восемь общих видов:

Вид блока	Префикс метки	Lean?	Профиль
`definition`	`def:`	обязательно	только paper
`theorem` / `lemma` / `proposition` / `corollary`	`thm:` / `lem:` / …	ожидается	только paper
`conjecture`	`conj:`	опционально	только paper
`proof`	`prf:`	опционально	только paper
`example` / `remark`	`ex:` / `rem:`	опционально	общий
`algorithm` / `simulator`	`alg:` / `sim:`	опционально	общий
`prose` / `equation` / `diagram` / `table`	`prose:` / `eq:` / `fig:` / `tbl:`	не применимо	общий

Четыре строки со значением только paper соответствуют MATH_BLOCK_KINDS в schemas/block-kinds.ts; строки общий соответствуют DOCUMENT_BLOCK_KINDS, полученным как дополнение, чтобы вид, добавленный позже, не остался без классификации.

На две из этих строк стоит обратить особое внимание. definition — это самая четкая граница разделения: это единственный вид, чье поле lean является обязательным, а не опциональным, поэтому фолио документа не могло бы содержать его, даже если бы это разрешал профиль. При этом общие виды по-прежнему декларируют опциональное поле lean: система типов разрешает то, что запрещает профиль, поэтому у content_profile_check есть второе правило помимо «разрешен ли этот вид».

Соответствующие схемы навыков: latex-authoring, lean-formalization, proof-verification.

Другие — расширение folio-assistant

✎ Edit TR

Новые типы контента являются первоклассными сущностями: добавьте адаптер контента и пакет навыков, и вы автоматически получите поддержку жизненного цикла, RBAC и механизмов интеграции MCP. См. Добавление типа контента.