I wish I had LLM-built Lean formalisations in university, so much of the math in the slides had errors, and some professors are very bad and ungracious admitting it, while simultaneously rejecting requests for clarifications by saying "the proof is in the slides".

Of course Lean proofs are rarely a good way to understand proofs, but hopefully they can be used to generate more human understandable arguments.