I replied to the other stuff elsewhere, but FWIW for the amount I've played with typing up undergrad tier knowledge in Lean, I've found it to be pretty straightforward. Fully formalized math isn't dense. Actually it's the opposite: full of tedious bookkeeping that you learn how to formalize in an intro logic/proofs course. The hard part is making it more dense so that you can read it, and something like Lean actually makes things surprisingly less tedious than you'd expect.