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!
Promising. Where can interested researchers discuss this and what does the question bank look like so far?
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!