[logicchains]

For me, C++ as its implementation language is one of the most promising things, as I suspect it's a significant reason why it's so much faster to check things than Idris. The speed difference is significant enough that I prefer it over Idris in spite of Idris' broader feature set: <1 second vs 10 seconds makes a huge difference to workflow when proving small lemmas (although it's possible I've somehow set up Idris wrong).

[unboxed_type]

I would love Lean to become both reliable and fast tool. I suggest, it is in its infancy right now to judge it seriously. As for now, I would rather invest in well established tools.