diff --git a/README.md b/README.md index 7af7f93..b1cbcf8 100644 --- a/README.md +++ b/README.md @@ -5,12 +5,16 @@ A new proof interface for Lean 4.
- Paperproof vscode + Paperproof vscode
Paperproof will inspect how the hypotheses and goals were changing throughout the Lean 4 proof, and display this history - making it equivalent to how we think of a mathematical proof on paper. -You can see Paperproof in action on [youtube](https://www.youtube.com/watch?v=m6MuiHQmULY). +We created a few videos about Paperproof: +- a super quick 1-minute demo of Paperproof: [youtube link](https://youtu.be/xiIQ0toSpxQ). +- our Lean Together presentation: [youtube link](https://www.youtube.com/watch?v=DWuAGt2RDaM). +- a full Paperproof tutorial: [youtube link](https://youtu.be/q9w1djIcCvc). + Here you can read about Paperproof in context of other proof trees: [lakesare.brick.do/lean-coq-isabel-and-their-proof-trees](https://lakesare.brick.do/lean-coq-isabel-and-their-proof-trees-yjnd2O2RgxwV). In the following tables, you can see what tactics such as `apply`, `rw`, or `cases` look like in Paperproof; and how Paperproof renders real proofs from well-known repos. @@ -449,23 +453,6 @@ Below, you will see a table with the main features of Paperproof. image - - - - To copy text of a particular tactic/hypothesis/goal, right-click on that node. - - - - - - - - image - - - - -