By having students use a proof assistant instead of just writing proofs and having them graded, the feedback loop between proof ideas and proof verification is tightened, leading to students being better at writing proofs.