Add sphinx-proof example

Author: benjaoming

docs/_config.yml

@@ -51,11 +51,25 @@ sphinx:
         - "https://nbformat.readthedocs.io/en/latest"
         - null
       sd:
-        - https://sphinx-design.readthedocs.io/en/latest
+        - "https://sphinx-design.readthedocs.io/en/latest"
         - null
-
+      sphinxproof:
+        - "https://sphinx-proof.readthedocs.io/en/latest/"
+        - null
+    hoverxref_intersphinx:
+     - "sphinxproof"
+    mathjax3_config:
+      tex:
+        macros:
+          "N": "\\mathbb{N}"
+          "floor": ["\\lfloor#1\\rfloor", 1]
+          "bmat": ["\\left[\\begin{array}"]
+          "emat": ["\\end{array}\\right]"]
+        
   extra_extensions:
+    - sphinx.ext.intersphinx
     - sphinx_inline_tabs
     - sphinx_proof
     - sphinx_examples
-    - hoverxref.extension
+    - hoverxref.extension
+

docs/_toc.yml

@@ -8,5 +8,7 @@ chapters:
 - file: notebooks
 - file: markdown-notebooks
 - file: intersphinx
-- file: sphinx-hoverxref
 - file: sphinx-examples
+- file: sphinx-hoverxref
+- file: sphinx-proof
+

docs/intro.md

@@ -33,7 +33,7 @@ We have also added some popular features for Jupyter Book that really you should
 * [intersphinx to link to other documentation and Jupyter Book projects](/intersphinx)
 * [sphinx-examples to show examples and results side-by-side](/sphinx-examples)
 * [sphinx-hoverxref to preview cross-references](/sphinx-hoverxref)
-* [sphinx-proof for logic and math, to write proofs, theorems, lemmas etc.](/sphinx-hoverxref) (TODO)
+* [sphinx-proof for logic and math, to write proofs, theorems, lemmas etc.](/sphinx-proof)
 * [sphinx-inline-tabs to display alternatives side-by-side with a tabbed interface](/sphinx-hoverxref) (TODO)
 
 

docs/sphinx-proof.md

@@ -0,0 +1,24 @@
+# Write proofs with sphinx-proof
+
+Easily render proofs, theorems, axioms, lemmas, definitions and much more with `sphinx-proof`. Read more in the [documentation of sphinx-proof](sphinxproof:syntax).
+
+````{prf:proof}
+We'll omit the full proof.
+
+But we will prove sufficiency of the asserted conditions.
+
+To this end, let $y \in \mathbb R^n$ and let $S$ be a linear subspace of $\mathbb R^n$.
+
+Let $\hat y$ be a vector in $\mathbb R^n$ such that $\hat y \in S$ and $y - \hat y \perp S$.
+
+Let $z$ be any other point in $S$ and use the fact that $S$ is a linear subspace to deduce
+
+```{math}
+\| y - z \|^2
+= \| (y - \hat y) + (\hat y - z) \|^2
+= \| y - \hat y \|^2  + \| \hat y - z  \|^2
+```
+
+Hence $\| y - z \| \geq \| y - \hat y \|$, which completes the proof.
+````
+