Skip to main content

All Questions

13 votes
2 answers
206 views

verifying combinatorial constructions - choice of a proof assistant

The choice of the proof assistant to use for formalisation depends on the area quite a bit; e.g. they say that algebraic topology comes easy in HoTT assistants. What would be the most natural choices ...
Dima Pasechnik's user avatar