Lean is getting the most math buzz of late. The HoTT people instead use Coq, which has to be adapted to their purpose. The differences could be its own thread.

Lean is getting the most math buzz of late. The HoTT people instead use Coq, which has to be adapted to their purpose. The differences could be its own thread. I love how you allow that dependent types are now "vanilla"; perhaps more people will migrate from Haskell to Idris. The HoTT book is the trippiest read. I said "perhaps", and what's an opinion worth if it's not obviously an opinion? Eilenberg has category theory and homological algebra to his credit, those are entire subjects that have shaped the last seventy years of mathematics. I'm happy to throw him into the debate.