Comment by bhouston

Why not? It seems like this should sort of be the standard now? Or is it hard to make lean proofs in all fields?