Jupyter notebooks might be a better target than Latex. One could conceivable verify proofs in the _small_, leaving some big reasoning steps out of the verification process. Then export the development to Latex, where it is automatically typeset.