Python <-> Lean

Stream: Is there code for X?

[Andre Graubner (安德)]

Hey everybody, I hope this is the right place to ask about this - if not, please point me to the correct place. Is there any work on some sort of bridge between the Lean ecosystem and the Python ecosystem? Given that e.g. the ML ecosystem is highly centered around Python, it would seem useful to have some sort of package that would enable for example the ‘importing’ and ‘manipulation’ of mathematical objects (from mathlib). This might make this area a bit more accessible for the masses… I don’t even know what something like this would look like (obviously one wouldn’t want to just write a Lean interpreter in Python), but if there has already been some sort of effort in that direction I don’t have to figure it out myself :) Thanks for any hints or comments in advance!

[Julian Berman]

Hello! There's indeed been some work done by Patrick Massot and Jason Rute and a few others. It lives here -- https://github.com/leanprover-community/lean-client-python/ there are some examples there, and indeed Jason and others in the ML community have successfully used that to wire Lean up to ML libraries (there's a #Machine Learning for Theorem Proving stream if you haven't seen it which may interest you)

[Johan Commelin]

Can you add a bit more details about what you expect to come out on the Python side? Do you want polynomial ℤ to translate to some notion of polynomials in python? Or do you want arbitrary terms and types to be translated to some sort of abstract-syntax-tree-expression-dump?

[Johan Commelin]

As in: do you want to do computer algebra in python, or do you want to work on proofs and the like?

[Andre Graubner (安德)]

Definitely the latter! I haven’t thought about the details yet, but I imagined the sort of Bridge that would for example enable a machine learning engineer build for example an OpenAI Gym environment based on some aspect of proof search or the like. It appears like how to do this is not really clear, but if nobody has done this before I might have a look at it :) I’ll have a look at the git repo you shared @Julian Berman, maybe that’s exactly what I’m looking for! Thanks a lot.

[Johan Commelin]

Yes, in that case you should look at what Jason Rute has been doing!