i wanna make a computer game that uses proof assistants and their addictive properties to tell stories about the wonderful world of mathematics that many usually don’t get to experience at all

perhaps due to a dose of perfectionism on my part, i consider this to only have a chance of properly succeeding if the plan involves a bunch of UX-gendered effort that basically requires PhD-level expertise in the field of interactive theorem proving to carry out

perhaps thanks to just the right amount of hubris on my part (or, indeed, maybe due to said hubris), my preferred course of action upon realising this is to strive to become an expert in said field, rather than to discontinue the goal