[universa1]

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

[zitterbewegung]

With Aristotle you could formalize a proof from only the text of a paper.

[trenchgun]

Yes, assuming the stuff it depends on is already formalized.