I'm working on something similar. Dependently typed, theorem proving, regular syntax, long form english words instead of symbols or abbreviations. It's not very

I'm working on something similar. Dependently typed, theorem proving, regular syntax, long form english words instead of symbols or abbreviations. It's not very well baked yet but claude/codex are already doing really well generating it. I expect that once the repo has been around long enough to be included in training data it'll improve. Probably next year or the year after.