I just discovered Lean and using computers for stating and proving theorems. The first question that came to my mind, can we write any proof with Lean? Or are there limitations (something that you can write a proof for on paper but not in Lean)?
I'm not talking about practicality or feasibility. But does the Lean system have the capability?
Edit: I posted the same question on proofassistants.stackexchange.