4 ms·
Sounds like a sales pitch for Lean (Microsoft's theorem prover), even though Coq [1] is the standard tool for the UniMath [2] project. [1] https://en.wikipedi
by ukj 7y ago
Sounds like a sales pitch for Lean (Microsoft's theorem prover), even though Coq [1] is the standard tool for the UniMath [2] project.
[1] https://en.wikipedia.org/wiki/Coq https://en.wikipedia.org/wiki/Coq
[2] https://github.com/UniMath/UniMath https://github.com/UniMath/UniMath
- krapht 7y agoWell, 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.