Comment by ndriscoll

I have hopes that this is primarily a matter of needing more engineering work on ergonomic formal languages and better building a language that "looks like math." e.g. when doing linear algebra stuff, a linear combination might be defined as a finitely supported function from an index set to your space, which is fine, but ugly and maybe conceptually overwhelming on first meeting, so I did some toying with little macros and eventually a small python Lean -> HTML renderer to do some basic transformations to make it look more like typical math notation with like \Sigma_{i \in I} a_i, or with a_0+...+a_n, etc. (to... not fantastic success, but I think there's still something to the idea).

I think a lot of math notation isn't wrong given a context, so in theory we should be able to translate it into something formal. Maybe also generate living documents where you can e.g. write `h : some_claim := by details(by rw[nat_mul_comm]; ...)` and the renderer hides details just like you'd write "obviously" in a traditional text. If the reader wants, they could then expand the details. etc. I found that many codex-generated proofs could be improved by telling it that I want a sequence of steps

  have next_step := by <I don't care>
  have therefore := by <still don't care>

So that the human proof appears as the left side, and I just ignore the right side as petty details. Again, not fantastic success, but better. Otherwise it goes very... Leanish by default.

Lean's VSCode plugin is I think only starting to explore the idea of a proper IDE for math. There's probably still tons of unexplored potential for like that fused with Matlab or whatever.