Comment by JonChesterfield

Metamath is superb. Linear time proof checking is especially good. I haven't got past the distinct variable side conditions, though it's an interesting take on the variable free in term / capture avoiding substitution equivalent in lambda calculus.