Hacker News Reader

Comment by _jcrossley | Hacker News Reader

I wish I had the free time to keep up with the mathlib project - this is so cool. Is there any way someone can get involved in a super hands-off way?

View on HN

You could start with the Natural numbers game.

https://adam.math.hhu.de/#/g/leanprover-community/NNG4

Well, thanks a lot! One minute I'm setting up a monitoring system and then ... I've just proved two is the number after the number after zero \o/ 8)

Hope you keep going with it, it’s a blast!

I read "GEB" by Hofstadter after I finished my A levels (UK, aged 18). I picked up a random book in the school library to fill in 20 mins before going out on a pub crawl (as you do). Once we had finished off the Abingdon Ock Street crawl in fine style and the hangover had subsided, I devoured it. I'd never read anything like it before - what a communicator of ideas.

A few unwise life style choices later and I find myself running a small IT company for the last 25 odd years.

I'll never get beyond undergrad engineering maths n stats but it's works like GEB and the Natural Numbers Game (and I see there are more) that allow civilians like me to get a glimpse into the real thing. There is no way on earth I could possibly get to grips with the really serious stuff but then the foundations are the really serious stuff - the rest simply follows on (lol)

Whom or whoever wrote the NNG tutorials are a very good communicator. The concepts are stripped to the bare essentials and the prose is crystal clear and the tone is suitably friendly.

Top stuff.

Yea I’ve run through that a couple of years ago - was brilliant, had a lot of fun. But I mean to stay up to date and somehow contribute from the sidelines

Wow, that's actually really fun. Is this what "proofs" are in math classes?

Sort of. Except for "weird logic classes", people would not bother to informally prove (i.e. no computers / strict system) such elementary things. But we can and should ask whether in fact that is the best curriculum structure.

(My making an easy fun game of proofs, I hope we can introduce them far earlier in the school curriculum. How many people in this world really understand the difference between reasoning and charismatic rhetoric? I don't blame anyone that isn't given the way we are taught.)

Reply on news.ycombinator.com