It warms my heart every time I see an interactive proof assistant being used to improve rather than simply slow down mathematical thinking.

After years of using the things, I believe not enough focus is given to high-velocity uses of proof assistants for prototyping. They can altogether replace scratch paper for fumbling around with new concepts.

WIP, but that is the target ethos in the prover I'm building:

https://github.com/ityonemo/bpa

Its painfully verbose and explicit but its designed to let you cut down to the structure of the proof with a query language