The question bank doesn’t exist yet because the language to ask the questions doesn’t exist yet. I spent a few weeks after writing this post trying to familiarize myself with Lean as quickly as possible and I found out that people in the Lean community simply haven’t formalized most of the objects I’d want to talk about (probabilistic networks, computational complexity, Nash equilibria, etc.). I tried to get a project off the ground formalizing these objects—you can see the GitHub repository here and the planning document here. Unfortunately this project quickly ballooned beyond what I can handle alone—I’m just an undergraduate student and winter break is over now. I still think it’s insane that some kind of crash formalization program isn’t currently underway. If you’re interested in pursuing a project like this then I’d be happy to talk through where I left off and what the next steps could look like!
The question bank doesn’t exist yet because the language to ask the questions doesn’t exist yet. I spent a few weeks after writing this post trying to familiarize myself with Lean as quickly as possible and I found out that people in the Lean community simply haven’t formalized most of the objects I’d want to talk about (probabilistic networks, computational complexity, Nash equilibria, etc.). I tried to get a project off the ground formalizing these objects—you can see the GitHub repository here and the planning document here. Unfortunately this project quickly ballooned beyond what I can handle alone—I’m just an undergraduate student and winter break is over now. I still think it’s insane that some kind of crash formalization program isn’t currently underway. If you’re interested in pursuing a project like this then I’d be happy to talk through where I left off and what the next steps could look like!