4 ms·
Well, having used both, Lean really is a lot more ergonomic. Unimath is mostly category theory; other parts of mathematics are woefully underdeveloped.
by krapht 7y ago
Well, having used both, Lean really is a lot more ergonomic. Unimath is mostly category theory; other parts of mathematics are woefully underdeveloped.
- ukj 7y agoThat's fair. I actually find Coq rather painful to use. It gives me the distinct impression that it has been designed/implemented by somebody who has never written human-computer interfaces before. When it comes to adapting humans to Mathematics, or adapting Mathematics to humans - I prefer the latter.