I hate the way theorems in lean look, so I’ve been working with an LLM to build something to do a surface syntax that compiles to lean. The inspiration is a “Markdown” like idea that would compile to lean. See pic for a sample. Repo at github.com/dgleich/c… – would love help!