Proofs, Theorems, and Algorithms

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:

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)

will be rendered as

Algorithm 2 (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 2.

Additional Documentation#

Further documentation for sphinx-proof is also available.

Contents