From db1ecc2ff1e8ab39380395e0048bf564359a217a Mon Sep 17 00:00:00 2001 From: Evgenia Karunus Date: Sat, 13 Jan 2024 10:29:52 +0400 Subject: [PATCH 1/4] README.md - change goal username --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 7af7f93..6fa047a 100644 --- a/README.md +++ b/README.md @@ -5,7 +5,7 @@ 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. From 43407b500ce2731243a4f3dc6e1facc293e9ec53 Mon Sep 17 00:00:00 2001 From: Evgenia Karunus Date: Sat, 13 Jan 2024 10:31:24 +0400 Subject: [PATCH 2/4] README.md - image update --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 6fa047a..37c501b 100644 --- a/README.md +++ b/README.md @@ -5,7 +5,7 @@ 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. From 2e0b5fdb649afb3dc3c11e91ad469089e98d8b7e Mon Sep 17 00:00:00 2001 From: Evgenia Karunus Date: Sat, 13 Jan 2024 11:03:27 +0400 Subject: [PATCH 3/4] README.md - new video link --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 37c501b..5ae2b8c 100644 --- a/README.md +++ b/README.md @@ -10,7 +10,7 @@ A new proof interface for Lean 4. 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). +You can see Paperproof in action on [youtube](https://youtu.be/xiIQ0toSpxQ). 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. From a390825649693dad70dc72e9e9b092d133390437 Mon Sep 17 00:00:00 2001 From: Evgenia Karunus Date: Sat, 13 Jan 2024 12:52:38 +0400 Subject: [PATCH 4/4] Update README.md --- README.md | 23 +++++------------------ 1 file changed, 5 insertions(+), 18 deletions(-) diff --git a/README.md b/README.md index 5ae2b8c..b1cbcf8 100644 --- a/README.md +++ b/README.md @@ -10,7 +10,11 @@ A new proof interface for Lean 4. 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://youtu.be/xiIQ0toSpxQ). +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 - - - - -