I encourage you to try Metamath. When starting a new axiom system from scratch, I found that I was not capable of writing anything that would cause lag; I wasn't able to make Metamath the slow part of my workflow. No matter how I approached it, the slowest parts of my work were my typing (with my fingers) and my typing (with my mind and whiteboard).
No other formal proof assistant has been this fast for me. The next closest one is Idris, which is type-theory-driven (fancy phrase for "slow") and it takes a few moments to round-trip between the REPL and the text editor.