Proofs, Theorems, and Algorithms

Infrastructure to support items such as proof and algorithm style formatting is provided by the sphinx-proof extension.

This extension supports the html and pdflatex builders.

sphinx-proof includes support for the following directives:

  1. Algorithms

  2. Axioms

  3. Conjectures

  4. Corollaries

  5. Criteria

  6. Definitions

  7. Examples

  8. Lemmas

  9. Observations

  10. Properties

  11. Propositions

  12. Proofs

  13. Remarks

  14. Theorems

Installation

Warning

This is not currently a default package in jupyter-book as is a relatively new package.

It needs to be enabled through the _config.yml after installation.

To install you can use pip:

pip install sphinx-proof

Adding extension through _config.yml

Open _config.yml and add sphinx_proof to:

sphinx:
  extra_extensions:
    - sphinx_proof

Using sphinx-proof

This package uses a prf sphinx domain.

All markup objects follow the {prf:<typeset>} (such as {prf:proof}) pattern and allows the directives to be referenced using the inline role {prf:ref}.

Warning

When referencing directives in sphinx-proof you need to use the {prf:ref}`<label>` inline role. Using other cross-referencing facilities will not work such as [](<label>)

Below we show an example using the {prf:algorithm} directive.

A similar pattern can be followed for the other syntax supported by sphinx-proof.

In MyST Markdown, you can add an algorithm to your document using the algorithm directive:

```{prf:algorithm} Ford–Fulkerson
:label: my-algorithm

**Inputs** Given a Network $G=(V,E)$ with flow capacity $c$, a source node $s$, and a sink node $t$

**Output** Compute a flow $f$ from $s$ to $t$ of maximum value

1. $f(u, v) \leftarrow 0$ for all edges $(u,v)$
2. While there is a path $p$ from $s$ to $t$ in $G_{f}$ such that $c_{f}(u,v)>0$
	for all edges $(u,v) \in p$:

	1. Find $c_{f}(p)= \min \{c_{f}(u,v):(u,v)\in p\}$
	2. For each edge $(u,v) \in p$

		1. $f(u,v) \leftarrow f(u,v) + c_{f}(p)$ *(Send flow along the path)*
		2. $f(u,v) \leftarrow f(u,v) - c_{f}(p)$ *(The flow might be "returned" later)*
```

will be rendered as

Algorithm 1 (Ford–Fulkerson)

Inputs Given a Network \(G=(V,E)\) with flow capacity \(c\), a source node \(s\), and a sink node \(t\)

Output Compute a flow \(f\) from \(s\) to \(t\) of maximum value

  1. \(f(u, v) \leftarrow 0\) for all edges \((u,v)\)

  2. While there is a path \(p\) from \(s\) to \(t\) in \(G_{f}\) such that \(c_{f}(u,v)>0\) for all edges \((u,v) \in p\):

    1. Find \(c_{f}(p)= \min \{c_{f}(u,v):(u,v)\in p\}\)

    2. For each edge \((u,v) \in p\)

      1. \(f(u,v) \leftarrow f(u,v) + c_{f}(p)\) (Send flow along the path)

      2. \(f(u,v) \leftarrow f(u,v) - c_{f}(p)\) (The flow might be “returned” later)

and can be referenced using the label assigned to the algorithm such as {prf:ref}`ford-fulkerson` which will provide a link such as Algorithm 1.

Additional Documentation

Further documentation for sphinx-proof is also available.