hrmacbeth / math2001 Goto Github PK

Hello

Thank you very much for the awesome book!

When filling out the proof of example 4.4.5, I am getting an error, which I having trouble debugging.
I am trying to apply the theorem abs_lt_of_sq_lt_sq' in order to show
$c < 3 \wedge c > -3$.

The error turns up here:

when I try to use the following theorem:

having these hypotheses:

Using my hypotheses h2 and h3c should allow me to conclude the result of the theorem.
However, it seems as if some of the types are making it throw an error.

Could anyone guide me on how to resolve this?

Thank you very much!

Nice to meet you．I am learning Lean by reading this material. Thank you for creating nice book!

I have a question about Lean's automated grading.

I am thinking of using Lean to organise private maths competitions. However, I'm faced with the problem of how to automate grading.

The Note for instructors in this material states that Gradescope is used for automatic grading. Could you tell me how to grade Lean code using Gradescope?

Alternatively, please let me know if you know anything about automatic grading of lean codes, not just Gradescope.

Thank you for reading.

1. The solution of Example 2.4.2 starts with "We have that p^2 \le 8 = 3^2".
   
2. Problem 3 of Exercises 3.1.10 says "Prove that if the integers m and m are even, then m + n is odd". It should be "if m is odd and n is even ...".