Hacker News Reader

Comment by ookdatnog | Hacker News Reader

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_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).

View on HN

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.

> 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.

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.

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.

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.

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.

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.

I find that the simplest way to understand P => Q is to express it as (!P or Q).

Reply on news.ycombinator.com