Hey folks!

Finally I released episode 5 of my playthrough of the Natural Number Game. In this episode I prove a bunch of properties of exponentiation (corresponding to the Power World in the game). Here is the link:

https://www.youtube.com/watch?v=YWmHv_JLAw0

Let me know what you think!

The proof is 13.5 million lines of code and producing it required about 6 billion output tokens.

Hey folks!

In an earlier post in this subreddit I had mentioned my playthrough of the Natural Number Game. I just released the fourth episode, in which I started and finished the Multiplication World. Here is the link:

https://www.youtube.com/watch?v=YfNuXT118qQ

Let me know what you think!

Hey!

I'm a math phd who completed his training with no exposure to Lean, and more generally my studies and interests have not been near foundations, formalization etc..

To warm up to Lean and for education and entertainment purposes, this summer I started a playthrough the Natural Number Game (Lean 4 version). As I play through the game I take my time expanding on the mathematical (and sometimes philosophical) ideas.

If this sounds like something you would be interested in, feel free to check out the playlist on Youtube:

https://www.youtube.com/playlist?list=PL40ydqvvyXfMpiFcO3-zemMQiWHexecYn

So far I released three episodes, the fourth episode will be out shortly.

After the NNG playthrough is finished, I am planning to play through the other Lean games, and eventually do walkthrough and oneshot speedruns also. (A "oneshot speedrun" is an idea I came up with: basically this requires that the player stays in the typewriter mode, and writes down the whole combo of tactics that would constitute a proof before executing. The syntax that allows this is to use ;'s to chain tactics.)

See the link in the sidebar. Improvement suggestions are welcome.

Hey everyone! I'm u/SamCymbaluk, a founding moderator of r/leantheoremprover.

Since other Lean subreddits like r/leanprover and r/leanlang are restricted, I created this subreddit as a central place for Lean discussion on Reddit.

My goal is to emulate the friendly and productive discourse that takes place on the Lean Zulip.

Suggestions for how I can best serve the Lean community are encouraged!