This is a port of Lamport's structured proof style (pf2) in typst. The goals of this project are to enable writing short, concise proofs with minimal interaction with external tools.
References to proof steps are checked for validity. One may only refer to proof steps which are older siblings or older siblings of ancestors. #parent allows referencing the current proof step's parent for assumptions. One can completely avoid this check by using the #refer() escape hatch.
Typst
#blk[
+ $2 = 8\/4$ <r0> \
#pf By Thm. 1.2
+ $8 = 2 sqrt(16)$
+ $8 = 4 + 4$ <r1> \
#pf Obvious.
+ $4 = sqrt(16)$
+ $4 . 4 = 16$ \
#pf Step @r1
+ #qed \
#pf By #prev(1)
+ #qed \
#pf #prev(1) and @r0
+ #qed \
#pf By #prev(1)
]TeX
\begin{proof}
\step{1}{$2 = 8/4$}
\begin{proof}
\pf\ By Thm.\ 1.2.
\end{proof}
\step{1a}{$8 = 2\sqrt{16}$}
\begin{proof}
\step{1-1}{$8=4+4$}
\begin{proof}
\pf\ Obvious.
\end{proof}
\step{1-2}{$4=\sqrt{16}$}
\begin{proof}
\step{1-2-a}{$4\cdot4=16$}
\begin{proof}
\pf\ Step \stepref{1-1}.
\end{proof}
\qedstep
\begin{proof}
\pf\ By \stepref{1-2-a}.
\end{proof}
\end{proof}
\qedstep
\begin{proof}
\pf\ \stepref{1-2} and \stepref{1}
\end{proof}
\end{proof}
\qedstep
\begin{proof}
\pf\ By \stepref{1a}
\end{proof}
\end{proof}
Copy the pf2.typ file into your project, along with example.typ. Run typst compile example.typ.
Please create an issue if you'd like any of these fixed.
- Only supports short numbering style -
<2>2instead of1.1.2. - For really long and deeply nested proofs (3 pages rendered) in a single
#blk, the incremental compilation times are high (~800ms).