My work is related to homotopy type theory. There are mathematicians working in Agda and Lean (2, but also 3) as well, but it certainly is a niche field.

Ah, makes sense. By being able to express "abstract and correct thought" I mean being able to express myself in a system much like a mathematician would. Coq for example is too constructively oriented for my taste to make that possible (I know, you can "just add an axiom" ...), and its automation is also (therefore?) not good enough.