qmd-prover 是你的 AI 编码助手——Claude Code 或 Codex——的插件，能帮助它 写并核对真实的数学。它建立了写证明的纪律，然后核实该纪律是否被遵守。

学科。你的数学是用明文.qmd文件写的。.qmd文件就是 普通文本文件（即任何编辑器都能打开的那种），格式称为Quarto。 markdown。在它内部，每个定义、引理、定理和证明都属于自己的块。一个块 由三行冒号:::开闭，其第一行给出一个简短的标签和 说明它是什么样的东西。这里有一个完整的、很小的例子——一个定义，一个定理，并且 其证据：

从这些片段中读出来：

• ::: …::: 与文本其余部分隔开一个街区。两行之间的所有内容 冒号的 就属于该区块。（中间的$…$正是数学符号的真实写法 书写;之后会以真实符号的形式呈现。）
• #def-even 是该块的label——其简称，即@id。每个语句都有一个，且 它在整个项目中独一无二。
• **.definition / .theorem / '。

qmd-prover

qmd-prover is an add-on for your AI coding assistant — Claude Code or Codex — that helps it write and check real mathematics. It sets up a discipline for writing proofs, and then checks that the discipline was followed.

The discipline. Your mathematics is written in plain-text .qmd files. A .qmd file is just an ordinary text file (the kind you can open in any editor) written in a format called Quarto markdown. Inside it, every definition, lemma, theorem, and proof sits in its own block. A block is opened and closed by a line of three colons, :::, and its first line gives it a short label and says what kind of thing it is. Here is a complete, tiny example — one definition, one theorem, and its proof:

::: {#def-even .definition name="Even number"}
An integer $n$ is **even** when $n = 2k$ for some integer $k$.
:::

::: {#thm-sum-even .theorem name="Sum of two even numbers"}
If $a$ and $b$ are even, then $a + b$ is even.
:::

::: {.proof of="thm-sum-even"}
By @def-even, write $a = 2k$ and $b = 2m$. Then $a + b = 2(k + m)$,
which is even by @def-even.
:::

Reading that from the pieces:

• ::: … ::: fences one block off from the rest of the text. Everything between the two lines of colons belongs to that block. (The $…$ in the middle is just how mathematical notation is written; it renders as real symbols later.)
• #def-even is the block’s label — its short name, its @id. Every statement has one, and it is unique across the whole project.
• .definition / .theorem / .proof says what kind of block it is. name="…" is the plain title a reader sees.
• The proof is its own separate block, and of="thm-sum-even" links it to the statement it proves. A statement and its proof are never mixed together.
• @def-even inside the proof is a pointer: it says “this step uses the definition labeled def-even.” Every time a proof leans on another result, it names that result this way, right at the spot where it uses it. Those pointers are what make every assumption visible.

You never type any of this — the assistant writes it. What matters is that the discipline is fixed, so the assistant (and the checks) can always tell which result depends on which.

Among all the results you build, one theorem is the one you ultimately want proved — that theorem is your goal. In the example above, the theorem thm-sum-even would be the goal, and the definition exists only to support it.

How the discipline is checked. Because every proof follows the discipline, the work can be checked in two layers:

• Mechanical checks (no AI). A plain program reads all the references @id and confirms the wiring is sound: every block has a unique label, every proof links to a real statement, every @id points at a result that actually exists, and no chain of citations loops back on itself. This