search

hrmacbeth / math2001

Lecture notes for a course on writing proofs, on paper and in the Lean proof assistant
184 stars 82 forks source link

Errata chapters 1–5 #7

Closed dfpetrin closed 8 months ago

hrmacbeth commented 8 months ago

Should be fixed in 6898669c90f6f55d521e13d57e42f686f115439d. Thanks for your careful reading!

dfpetrin commented 8 months ago

Great! I'm glad you found these useful, and good luck with the quarter. :)

I got a bit halfway through the text (through the Number Theory chapter) before the quarter started. I'll need to pause for now since I'm taking a high workload class this quarter, but I'll pick back up where I left off after that and have another batch for you.

dfpetrin commented 8 months ago

One thing I did find, which wasn't captured well in a git commit, is that for the solution to exercise 8 in the section 6.3 exercises (tighter upper and lower bounds for the Fibonacci sequence), I needed to use norm_cast to finish off the calculation blocks in the inductive step, which I only figured out after you later used that tactic in the proof of the corollary to pascal_eq in 6.5.3.

It may be that I missed something for pushing through that proof without norm_cast, or you may need to introduce that tactic for that exercise, or change or drop the exercise.