Interesting also prompt of the python formalization (and the blog post) mentions the julia-in-lean:

https://github.com/Broyojo/python-formalization/blob/main/AG...