Lately, I've been reading Mario Carneiro's PhD thesis on Metamath Zero (MM0) and watching his tutorial. I want to use MM0/MM1 and Lean for developing my educational video game.

• Git repository: github.com/digama0/mm0
• PhD thesis: github.com/digama0/mm0/tree/gh
• Tutorial: youtu.be/A7WfrW7-ifw?si=Y-abW0

0

If you have a fediverse account, you can quote this note from your own instance. Search https://mathstodon.xyz/users/chabulhwi/statuses/115976100226248726 on your instance and quote it. (Note that quoting is not supported in Mastodon.)