Repository files navigation

A tool to display **mathematical proofs** as **structured** objects, seehttps://francoisschwarzentruber.github.io/prooffold/

Video: [https://www.youtube.com/watch?v=FPZiGevIyR8]

It tries to solve two main issues of traditional proofs written in a book:

• the global organization of a proof in a textbook is often not very clear. This is due to the linearity of a textual proof. Here, the proof is displayed in panels, making an emphasis on the structure of the proof
• In a textbook, justifications of a statement often ends up "by Theorem 1.2.3, Lemma 42.4 and Corollary 8.8.4 and Equation 1". Here, by clicking on a statement, the arguments used to deduced that fact are highlighted.

• Structured proofs
• LaTEX for writing formulas
• Labels [(1) (2)] and references [by (1,2)]
• inline graphs via graphviz
• interactive canvas described in Processing (P5JS)
• Automatic aligned equations and inequations
• Asciiart, it partially works but soon viahttps://github.com/francoisschwarzentruber/asciidraw we will be able to write nice pictures
• Arrows of implications
• Include Tikz pictures

Proofs are easy to be written.

  Fact  Theorem. $a^2 = b^2 + c^2$.        {          explain sth of the proof of the theorem          an amazing fact       (1)          {             proof of that amazing fact          }          we have that $x = 0$         (2)          Thus we have bling       by (1,2)        }  Another Fact

Each line is a fact, or simple text. Blocks (panels) are delimited by{ and} and corresponds to a detailed proof of the fact written just before the block. (1), (2) etc. and by (1,2) enable to highlight some facts used to prove another fact. In the example below,Thus we have bling is deduced froman amazing fact andwe have that $x = 0$.

Graphs in graphviz are described by:

         graph {             <<graphviz code>>          }         digraph {             <<graphviz code>>          }

Algorithms need indentation and they can be written via:

         algo {             <<description of the algorithm>>          }

Interactive canvas are described in Processing (P5) via:

         p5 {{             <<graphviz code>>          }}

Adding new proofs! Also discussing about how to improve the way to display proofs.

1. Create a new file in theproofs folder, for instancemyproof.proof.
2. Write your proof inside
3. Locally run./run.sh
4. Openhttp://0.0.0.0:8000/?id=myproof

Then if you want, you can make apull request!