math2001
math2001 copied to clipboard
hrmacbeth
Lecture notes for a course on writing proofs, on paper and in the Lean proof assistant
It's jarring to open this repository and have my theme change. Removing this line keeps the theme to what the user has already set.
Add the `by` keyword to two proofs where it seemed to be missing. Without these the student might be confused by errors messages in their editor that don't make it...
Hi, I am learning Lean4 for the purpose of LLM accelerated proof writing, thank you so so much for writing this book and posting it online open sourced. This book...
The blue box states a different problem than the example. In the blue box, you have {n:Z s.t. n = 1 zmod 5} intersected with {n:N s.t. n = 1...
There is a theorem gcd_dvd starting about line 60 of this file. It's not clear if the reader should resolve the 8 sorries or not. I think not since gcd_dvd_right...
Lemma `le_or_gt` is used in example 2.5.2 without comment. Only further down in exercise 6, a short explanation is provided: > As in Example 2.5.2, I used the lemma le_or_gt,...
Given the ways that we see `cancel` being used in the book, and given some discussions in the Zulip lean community, I think maybe there is a bug in the...
I'm aware that some of the tactics in this course are specifically created by you to aid learning - thank you! I'm trying to create a small task and proof...
The prose uses variables `x` and `t` but the sample code uses `a` and `t`. I think this is a typo. (confused me for half an hour - i'm a...