Modified amsthm Annotation Format

Backbuild Prove accepts proofs in two compatible formats. Pick the one that matches how you already write mathematics; the kernel verifies both the same way. This page teaches the natural, paper-style format for people who would rather not write dense machine notation.

After this page you will be able to take a proof written in ordinary amsthm, add the handful of macros the kernel needs, and have it verified, with any error routed back to the exact line in your own source.

Two Formats, One Kernel

Backbuild Prove accepts proofs written in two compatible formats. The canonical format is pf2, a Lamport-style, dense, machine-first notation that the HOL kernel consumes directly. The second format is modified amsthm, a natural mathematical style that matches what mathematicians write in published papers, enriched with the minimum formality needed for deterministic translation to pf2.

The kernel internally uses pf2 for all verification. The modified amsthm format is a thin, deterministic syntactic layer on top: a translator emits pf2 from your amsthm source, and the same HOL kernel checks the result. A mathematician comfortable with standard amsthm papers can write fully verified proofs with approximately five additional macros. Everything else, including your theorem environments, your prose, your align blocks, and your \ref and \cite commands, stays exactly as you already write it.

If you prefer the dense canonical notation, see Writing pf2 Annotations. If you want to write proofs the way they appear in mathematical papers, read on.

What Stays Pure amsthm

The following constructs work unchanged. If you know standard amsthm, you already know this part:

• Theorem-like environments: \begin{theorem}, \begin{lemma}, \begin{definition}, \begin{proposition}, \begin{corollary}, \begin{remark}, \begin{claim}, \begin{example}.
• Cross references: \label{thm:…}, \ref{thm:…}, \autoref{thm:…}, \cite{…}.
• Proof environment: \begin{proof}…\end{proof}.
• Displayed math environments: \begin{align}, \begin{align*}, \begin{equation}, \begin{gather}.
• Natural prose inside the proof environment. Write as you would for a journal.
• End markers: \qed and \qedhere work as expected.

None of this changes. The modified-amsthm format is strictly additive.

The Five Required Additions

The translator needs five things that standard amsthm does not require. Learn these and you have the whole format.

Macro	Purpose	Example
$\vdash P$ inside a theorem env	The formal HOL statement the kernel will prove. Placed alongside your prose description of the theorem.	See the canonical example below.
\by{…} after a claim or chain row	Justification; cites a prior step, a lemma, an axiom, or a tactic.	\by{\ref{lem:amgm2}}, \by{\stepref{r2}}, \by{algebra}
\assume{$P$}	Introduces a hypothesis into the local proof context.	\assume{$x > 0$}
\pflet{$x = rhs$}	Names an intermediate value so subsequent steps can refer to it.	\pflet{$t = xy$}
\case{…}	Begins one branch of a case split.	\case{$x = 0$}

One convenience rule closes the list: the final sentence of a proof, immediately before \qed, is treated as the conclusion and needs no explicit marker. Unjustified rows inside an align* block are tolerated by the parser but flagged by the kernel; during strict verification they must carry a \by{…}.

The Canonical Example: AM-GM for Four Variables

The AM-GM inequality for four non-negative reals states that 4xyzw ≤ x&sup4; + y&sup4; + z&sup4; + w&sup4;. Here is the natural proof a mathematician might write in a paper, in plain LaTeX:

\begin{proof}
  Let $t,u \in \mathbb{R}$ where $t=xy$ and $u=zw$. So,
  \begin{eqnarray*}
    4xyzw &=& 2\cdot2tu \\
    &\le& 2\cdot(t^2+u^2) \\
    &=& 2\cdot((xy)^2+(zw)^2) \\
    &=& 2\cdot(x^2y^2+z^2w^2) \\
    &=& 2x^2y^2+2z^2w^2 \\
    &\le& ((x^2)^2+(y^2)^2)+((z^2)^2)+(w^2)^2) \\
    &=& x^4+y^4+z^4+w^4
  \end{eqnarray*}
\end{proof}

The same proof in Backbuild Prove’s modified-amsthm format: eqnarray* becomes align*, every row carries a \by{…}, and the theorem envelope declares the formal statement with $\vdash$.

\begin{theorem}[AM-GM for four variables]\label{thm:amgm4}
  For all non-negative reals $x,y,z,w$,
  $\vdash 4xyzw \le x^4 + y^4 + z^4 + w^4$.
\end{theorem}

\begin{proof}
  \pflet{$t = xy$, $u = zw$ where $t,u \in \mathbb{R}$ }
  \begin{align*}
    4xyzw &= 2 \cdot 2tu                              && \by{\pflet} \\
          &\le 2 \cdot (t^2 + u^2)                     && \by{\ref{lem:amgm2}} \\
          &= 2 \cdot ((xy)^2 + (zw)^2)                 && \by{\pflet} \\
          &= 2 \cdot (x^2 y^2 + z^2 w^2)               && \by{algebra} \\
          &= 2 x^2 y^2 + 2 z^2 w^2                     && \by{distributivity} \\
          &\le (x^2)^2 + (y^2)^2 + (z^2)^2 + (w^2)^2   && \by{\ref{lem:amgm2}} \\
          &= x^4 + y^4 + z^4 + w^4                     && \by{algebra}
  \end{align*}
\end{proof}

The translator emits the following pf2 from the block above. This is what the HOL kernel actually verifies:

\begin{pf2}{thm:amgm4}
  \stmt{ \forall x\, y\, z\, w : \mathbb{R}_{\ge 0}.\;
           4xyzw \le x^4 + y^4 + z^4 + w^4 }
  \let{r0}{ t := xy,\ u := zw }
  \step{r1}{ 4xyzw = 2 \cdot 2tu }
    \pf\ By \stepref{r0}.
  \step{r2}{ 2 \cdot 2tu \le 2 \cdot (t^2 + u^2) }
    \pf\ By \ref{lem:amgm2}.
  \step{r3}{ 2 \cdot (t^2 + u^2) = 2 \cdot ((xy)^2 + (zw)^2) }
    \pf\ By \stepref{r0}.
  \step{r4}{ 2 \cdot ((xy)^2 + (zw)^2) = 2 \cdot (x^2 y^2 + z^2 w^2) }
    \pf\ By algebra.
  \step{r5}{ 2 \cdot (x^2 y^2 + z^2 w^2) = 2 x^2 y^2 + 2 z^2 w^2 }
    \pf\ By distributivity.
  \step{r6}{ 2 x^2 y^2 + 2 z^2 w^2 \le (x^2)^2 + (y^2)^2 + (z^2)^2 + (w^2)^2 }
    \pf\ By \ref{lem:amgm2}.
  \step{r7}{ (x^2)^2 + (y^2)^2 + (z^2)^2 + (w^2)^2 = x^4 + y^4 + z^4 + w^4 }
    \pf\ By algebra.
  \qedstep
    \pf\ By transitivity on \stepref{r1}--\stepref{r7}.
\end{pf2}

The translation is mechanical: each align row becomes a numbered \step, each \by{…} becomes a \pf justification, the \pflet becomes a \let step, and the final \qedstep closes the chain by transitivity.

Line-by-Line Breakdown

This is the centerpiece of the format. Each row shows the original natural-LaTeX line, the modified-amsthm version, and the pf2 line the translator emits. The WHY column explains what the change gains you.

Original amsthm	Modified amsthm	Generated pf2	Why
(theorem statement in prose)	$\vdash 4xyzw \le x^4 + y^4 + z^4 + w^4$	\stmt{ … }	The kernel needs a formal HOL proposition to prove. Prose is retained; the $\vdash$ line sits alongside it.
Let $t = xy$ and $u = zw$.	\pflet{$t = xy$, $u = zw$}	\let{r0}{t := xy,\ u := zw}	Names the intermediate values so subsequent steps can cite them by label. Prose starting with “Let” is also recognized heuristically.
\begin{eqnarray*}	\begin{align*}	(environment switch only)	eqnarray is deprecated in modern LaTeX. align* is the amsmath replacement and parses more reliably.
4xyzw &=& 2\cdot2tu \\	4xyzw &= 2 \cdot 2tu && \by{\pflet}	\step{r1}{4xyzw = 2 \cdot 2tu} \pf\ By \stepref{r0}.	The \by{\pflet} cites the earlier \pflet row. Without it the kernel cannot tell why the equality holds.
&\le& 2\cdot(t^2+u^2) \\	&\le 2 \cdot (t^2 + u^2) && \by{\ref{lem:amgm2}}	\step{r2}{…} \pf\ By \ref{lem:amgm2}.	Cites the two-variable AM-GM lemma by label. The kernel looks up the registered theorem and checks it discharges the inequality.
&=& 2\cdot((xy)^2+(zw)^2) \\	&= 2 \cdot ((xy)^2 + (zw)^2) && \by{\pflet}	\step{r3}{…} \pf\ By \stepref{r0}.	Substituting t := xy and u := zw back in is still justified by the \pflet.
&=& 2\cdot(x^2y^2+z^2w^2) \\	&= 2 \cdot (x^2 y^2 + z^2 w^2) && \by{algebra}	\step{r4}{…} \pf\ By algebra.	(xy)^2 = x^2 y^2 is pure ring reasoning, so the algebra tactic closes it automatically.
&=& 2x^2y^2+2z^2w^2 \\	&= 2 x^2 y^2 + 2 z^2 w^2 && \by{distributivity}	\step{r5}{…} \pf\ By distributivity.	Naming the exact rule (distributivity) is more precise than algebra and helps audit reports read like mathematics.
&\le& ((x^2)^2+(y^2)^2)+… \\	&\le (x^2)^2 + (y^2)^2 + (z^2)^2 + (w^2)^2 && \by{\ref{lem:amgm2}}	\step{r6}{…} \pf\ By \ref{lem:amgm2}.	Same two-variable AM-GM lemma, applied twice and summed. Bonus: the modified version fixes the unbalanced parens in the original.
&=& x^4+y^4+z^4+w^4	&= x^4 + y^4 + z^4 + w^4 && \by{algebra}	\step{r7}{…} \pf\ By algebra.	(x^2)^2 = x^4, and so on; ring identities again.
(implicit conclusion)	(implicit conclusion)	\qedstep \pf\ By transitivity on \stepref{r1}--\stepref{r7}.	The kernel auto-generates the final transitivity step by chaining the relations in r1 through r7.

Justification Syntax Reference

Every form \by{…} can take. Mix and match as the proof demands.

Form	Meaning
\by{\ref{lem:foo}}	Cite a registered theorem or lemma by its LaTeX label.
\by{\stepref{r1}}	Cite a prior step in the same proof by row label.
\by{\stepref{r1}--\stepref{r5}}	Cite a range of prior steps (useful for transitivity chains).
\by{AXIOM_NAME} or \by{RULE_NAME}	Cite a named inference rule or axiom from the kernel.
\by{algebra}, \by{arithmetic}, \by{commutativity}	Invoke a named tactic. The kernel tries the tactic and either discharges the step or produces a precise error.
\by{\cite{foo2024}}	External citation, for proofs that reference published work. The kernel records the citation in the certificate bundle.

Migration Guide: From a Standard amsthm Paper

If you already have a LaTeX paper written with amsthm, the path to a verified proof is short. Work through it in this order:

1. Add the formal statement. Inside each \begin{theorem}[display name]\label{thm:…} environment, add a line of the form $\vdash FORMAL$. Keep your prose description above it if you like, since both coexist. The prose is for readers; the $\vdash$ line is for the kernel.
2. Replace eqnarray* with align*. The eqnarray environment is deprecated in modern LaTeX and has known alignment problems. Modified-amsthm requires align/align*.
3. Add \by{…} to each align row. Every non-trivial chain row needs a justification. The right-aligned annotation pattern (&& \by{…}) keeps the body readable while giving the kernel what it needs.
4. Replace “Let X = Y” prose with \pflet{$X = Y$}. This is optional (Prove’s prose heuristics recognize sentences starting with “Let … =”), but the explicit macro is unambiguous and cross-referenceable.
5. Wrap case analysis in \case{…}. For proofs that split on hypotheses, each branch begins with a \case marker naming the branch condition.
6. Run backbuild prove run. The CLI reports any missing justifications with the exact source line number. Fix, re-run, and iterate until all rows check.

Prose Heuristics (Phase 2)

The translator reads English too. These sentence patterns are recognized and translated without any extra macros, so existing papers translate with far fewer edits than the full macro set suggests.

• “Let X = Y” is translated to \pflet{$X = Y$}.
• “Assume X” / “Suppose X” is translated to an assumption step (\assume{$X$}).
• “Therefore X” / “Hence X” / “Thus X” / “So X” / “It follows that X” is translated to a consequence step. Non-trivial consequences still need an explicit \by{…}; trivial ones may be auto-discharged.

Anything else is emitted as an unjustified step. The kernel may discharge it automatically by normalization, or it may demand an explicit \by{…}. The error message always tells you which.

IDE Integration: errors on your source line

Every translator error is routed to the line in your amsthm source that caused it, not to a position in the intermediate pf2 the translator generated. The Backbuild Prove VS Code extension (which also runs in Cursor, Windsurf, and other VS Code-compatible editors via the VS Code Marketplace and Open VSX) places the diagnostic squiggly directly under the failing macro in your source. Diagnostics are delivered over the Language Server Protocol, so any LSP-capable editor gets the same source-accurate placement.

Columns are reported in UTF-16 code units per LSP 3.17 §3.17.8 so non-ASCII identifiers (λ, ℝ, ∀, supplementary-plane math symbols) land on the correct cursor position even though they occupy multiple UTF-8 bytes.

Warnings carry stable diagnostic codes that IDE extensions and CI pipelines can allow-list or escalate without parsing free-text messages. Set BBPROVE_IGNORE_WARNINGS=AMSTHM-003,AMSTHM-005 in the environment to suppress specific codes; the suppressed codes never appear in the pf2 output or the structured-warnings API, so CI can pin-allow deprecation noise while still failing on unjustified steps.

Code	Meaning
AMSTHM-001	Unjustified chain row: the align row has no \by{…}.
AMSTHM-002	Multi-row chain uses a relation (\le, \ge, \subseteq, …) without variadic-transitivity support. Add an explicit trailing prose step.
AMSTHM-003	Deprecated environment (eqnarray*). Translation still succeeds; migrate to align*.
AMSTHM-004	Prose sentence didn’t match any recognised pattern. Add \by{…} or use Let / Assume / Therefore.
AMSTHM-005	Therefore/Hence/Thus has no \by{…}. Kernel will reject as unjustified.

Common Error Messages

The translator and kernel share an error vocabulary. Every diagnostic points to a source line and suggests the fix.

Message	Fix
missing formal statement: theorem env contains no “$\vdash …$”	Add a $\vdash FORMAL$ line inside the theorem environment.
unjustified chain step at line N	Add \by{…} to the align row at line N.
unknown justification “foo”	foo is not a registered theorem, axiom, or tactic. Check spelling or register the theorem first.
unresolved \ref{lem:x}	No registered theorem has label lem:x. Verify the label exists and was registered before this file runs.
ambiguous transitivity	Chain mixes incompatible relations (e.g. = with \in). Split into separate chains or use an explicit bridging step.

Why This Matters

Verified mathematics has historically demanded a new dialect for every proof assistant. Modified amsthm reverses that bargain: mathematicians write in the format they already know, with the proofs they already publish. The five-macro overlay is the smallest bridge that lets a HOL kernel mechanize what a human reader would call a complete proof. Published papers become verified artifacts; verified artifacts read as published papers. Five macros, no new DSL, full kernel certainty.

Next Steps

• Getting Started: install the CLI or an editor extension and verify your first annotation
• Writing pf2 Annotations: the canonical pf2 format the translator emits
• Supported Languages: embed modified-amsthm proofs in 20+ programming languages
• Lean 4 Cross-Check: have an independent engine confirm every verified proof