School math from scratch

Stream: new members

[Grigoriy Prokhrov]

I am sorry for the overlong post but I feel that I write this.

I have just finished Natural Number Game. And I have caught myself with a thought that this game reimplements primary school math. Maybe it would be a consequent way to continue with middle school program but with lean basis.

I study programming at School 21 in Moscow with p2p system. And I see many people who would like to learn math in a proper way but all education designed to only reproduce itself. A textbook is a tool in the hands of professional teachers and it satisfies only their education process. It is not designed for self-education by default, because mostly it is a product of university lectures.

On the other hand, I have an example when the people reimplement standard c library or even unix shell without any teacher, but before the school they might be absolutely unfamiliar with a computer at all. In my opinion, the interative systems makes this possible. You use compiler, checkers and brain.

I have seen Kevin Buzzard's presentation and I have familiar questions. But does we really need these uninterested mathematicians, when it is possible to open the door for those who really need it and give them a proper map to build their own path?

[Julian Berman]

(I'm not sure I follow the end of that -- it sounds like you're asking whether we can obsolete math professors :)? I have no idea) -- but on the middle part, I think from what I've seen (part? most? some?) of the point of Kevin's Xena project is to cover an undergrad curriculum in math, so yeah it seems to be being worked on quite a bit beyond primary and middle school (and there are some pages that show how much is being covered I think)

[Julian Berman]

Yeah, this page: https://leanprover-community.github.io/undergrad_todo.html

[Julian Berman]

I'm not sure I like the idea of teaching someone computers by having them reimplement libc :D -- but for some people I'm sure it works.

[Grigoriy Prokhrov]

The key idea is that every student constructs its own "copy" of theory from scratch. This conclusion could be achieved if we go backwards from undergraduate math to middle school math and then to the very beginning.

In my opinion, a computer is just a fast and interactive instrument of proof. Nothing more. Nothing less.
Learning C language is just a heritage of classic university approach. In this case it is supposed that the only way you can use language in a proper manner is the actual possibility to reconstruct the key features of that language. And "libc re-implementation" is just another iteration in the process of achieving an optimal course scheme.

[Yury G. Kudryashov]

What exactly do you want? NNG-style games covering other parts of the middle school / high school curriculum (note that these notions depend on your choice of country/school)? A mathlib-style library that doesn't use advanced theory to prove simple lemmas? Something else?

[William Sealy Gosset]

Yury G. Kudryashov said:

What exactly do you want? NNG-style games covering other parts of the middle school / high school curriculum (note that these notions depend on your choice of country/school)? A mathlib-style library that doesn't use advanced theory to prove simple lemmas? Something else?

That's actually quite a good idea. There's a lot to be said for gamification. The key is to find the sweet spot between easy enough that you don't scare people away but hard enough that you are putting people just outside of their comfort zone. I've read a little bit about the creation of video games, and this is exactly one of the things early levels of games focus on: Show the player how to do something and then change the environment a little where they are then forced to use what they just learned in a novel way to advance to the next stage.

[Julian Berman]

At least in the US I don't know that any level of gamification could solve the trainwreck of boredom that is the middle school/high school math curriculum

[William Sealy Gosset]

Do you think that is because the kids are not capable of tackling a more structured approach or because they school system is not capable of teaching a more structured approach, even if that approach is packaged more as a game?

[Julian Berman]

Personally I think it's because the math that's generally part of the curriculum is just not interesting to kids (heck or adults)

[Julian Berman]

I could certainly believe that all the symbol manipulation kids would find more fun to do in lean than what they do by hand on paper, so I could believe it'd help in that sense on getting kids better algebraic skills

[Julian Berman]

But I don't think me personally I'd have found doing the terrible geometry proofs they make 7th graders in the US do any more interesting if I had to do them in lean than on paper, even if they were a game

[Julian Berman]

(I guess it depends heavily on what OP's original goal was too)

[William Sealy Gosset]

My situation is just one data point, but I think it is somewhat applicable here. I have a graduate degree in financial engineering. Pure mathematics is not my background. I find pure mathematics interesting, and while I have experience writing software as well, my first look at Lean turned me off. There were simply too many cognitive hurdles to overcome. I found the Natural Number Game though and it helped me get some momentum. I think that is what the original poster was trying to get at.

[Julian Berman]

Oh I 100% agree with that (I'm likely in close to the same boat you are), something like NNG is amazing for momentum and like finding a route into this complex thing without needing to know a ton of math

[Julian Berman]

I just think if the goal is that that you'd want to gamify some math that's more "interesting" to the target audience

[Kevin Buzzard]

Lean is so axiomatic and precise, and this is not how younger children are taught mathematics. Whether this is for historical reasons or that they are mostly simply not ready is a different question. I could envisage some kind of geometry proving game but I believe that such things might already exist. I have mainly been concentrating on mathematics undergraduate-level games/puzzles because these are simply the people I know best. We have a 1/3-written real number game, a group theory game which accidentally became an ongoing proof of Sylow's theorems, and probably other things will emerge, but basically I'm too busy to work on them properly and the interface is so clunky to set up. The complex number game can't be played online so nobody plays it, but I think it's fun.

[Julian Berman]

Yeah those are all awesome by the way. I didn't know anything beyond the NNG existed until I caught them out of the corner of my eye when you mentioned the group theory one in another Zulip thread -- maybe it's worth mentioning they exist at the conclusion of NNG? (Happy to send a PR to do so if that's a decent idea)

[Yakov Pechersky]

There's this game which is a proving game of logic http://incredible.pm/

[Yakov Pechersky]

And a geometry proof game https://www.euclidea.xyz/

[Yury G. Kudryashov]

euclidea is not about proofs.

[Yury G. Kudryashov]

It's about doing ruler&compass construction in the least possible number of moves.

[Yury G. Kudryashov]

(btw, the same guys do Pythagorea and Pythagorea 60)