I feel like this aged like milk because it assumes a human mathematician writing the proof but many people are now generating Lean proofs with LLMs.