3 ms·
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.
by giraj 6y ago
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.
- auggierose 6y agoAh, 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.