4 ms·

At Imperial College London there's an intro to proofs course taught with interactive exercises supported by a proof assistant, Lean. The exercises (and the proo

At Imperial College London there's an intro to proofs course taught with interactive exercises supported by a proof assistant, Lean. The exercises (and the proof assistant) are freely available online at https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/ https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_g.... Disclaimer: I didn't fully work through this game, I never studied at ICL and I can't vouch for its effectiveness, I simply heard about it and thought it was interesting and relevant to your question. (Here's also a talk by the professor about his rationale for using Lean: https://youtu.be/Dp-mQ3HxgDE https://youtu.be/Dp-mQ3HxgDE).

martincmartin 4y ago
This might not be the best introduction for someone who hasn't proved "a = b iff a - c = b - c", and e.g. may not be familiar with "if and only if," or the fact that P => Q is considered true if P is false, even if Q is also false.
- CoastalCoder 4y ago
  Tangent: ever since highschool I've wondered about the schism between (a) the elements of "showing one's work" for algebra / calculus problems and (b) formal syllogisms to justify each step. I have to wonder if highschool math would make more sense to some students if (a) and (b) were taught together.
  - Ericson2314 4y ago
    I think the way society conceives if grade school math is pretty rotten, and we need to shake things up if only to build a new cultural relationship with it. Common core focusing on intuition is actually good, and someday throwing in theorem provers will add back a good challenge while keeping things approachable. I might even cut polynomials entirely to make room for the new stuff and do informal calculus earlier.
    - Ericson2314 4y ago
      Or like, just straight up get people to practice being shape rotators lol. Do picture of something in art class, ask them to draw it from a different perspective. Math is ultimately about bridging the gap between fuzzy warm intuition and and cold artificial rigor. Focusing on either in isolation defeats the purpose.
- puffoflogic 4y ago
  > P => Q is considered true if P is false, even if Q is also false It's a good thing then that this framing is rather unlike the intuitionistic mathematics actually suggested.
- ookdatnog 4y ago
  That may be the case. Otoh, this is being used as an intro course for first year college students, who don't have any background in logic afaik. So perhaps it could work. I don't have enough information to say either way.
- Ericson2314 4y ago
  On the contrary wrestling with the computer allows one to internalize those things through experience. For anyone that struggled with pure math because memorizing seemed less "big brained" than informal proofs, computers making thing concrete let alone gamified can help immensely.
- omegalulw 4y ago
  I find that the simplest way to understand P => Q is to express it as (!P or Q).

martincmartin 4y ago

This might not be the best introduction for someone who hasn't proved "a = b iff a - c = b - c", and e.g. may not be familiar with "if and only if," or the fact that P => Q is considered true if P is false, even if Q is also false.

CoastalCoder 4y ago
Tangent: ever since highschool I've wondered about the schism between (a) the elements of "showing one's work" for algebra / calculus problems and (b) formal syllogisms to justify each step. I have to wonder if highschool math would make more sense to some students if (a) and (b) were taught together.
- Ericson2314 4y ago
  I think the way society conceives if grade school math is pretty rotten, and we need to shake things up if only to build a new cultural relationship with it. Common core focusing on intuition is actually good, and someday throwing in theorem provers will add back a good challenge while keeping things approachable. I might even cut polynomials entirely to make room for the new stuff and do informal calculus earlier.
  - Ericson2314 4y ago
    Or like, just straight up get people to practice being shape rotators lol. Do picture of something in art class, ask them to draw it from a different perspective. Math is ultimately about bridging the gap between fuzzy warm intuition and and cold artificial rigor. Focusing on either in isolation defeats the purpose.
puffoflogic 4y ago
> P => Q is considered true if P is false, even if Q is also false It's a good thing then that this framing is rather unlike the intuitionistic mathematics actually suggested.
ookdatnog 4y ago
That may be the case. Otoh, this is being used as an intro course for first year college students, who don't have any background in logic afaik. So perhaps it could work. I don't have enough information to say either way.
Ericson2314 4y ago
On the contrary wrestling with the computer allows one to internalize those things through experience. For anyone that struggled with pure math because memorizing seemed less "big brained" than informal proofs, computers making thing concrete let alone gamified can help immensely.
omegalulw 4y ago
I find that the simplest way to understand P => Q is to express it as (!P or Q).