Comment by david-gpu

Good luck writing a Lean proof of a nontrivial theorem by giving a keyboard to a thousand coke-fueled monkeys. If only it was that easy.