This looks interesting. I am not really familiar with lean, etc... Could I use this to formalize/verify a proof from a paper?