Python library for lean3

Stream: Machine Learning for Theorem Proving

[秋天]

Is there a python library that can verify the correctness of a lean3 theorem? I'd like to integrate it in my autoformaliztion program.

[Eric Rodriguez]

Why aren't you using lean4?

[Jason Rute]

The two easiest ways to use Lean 3 or Lean 4 from Python are (1) by just making a Lean file and running lean as a subprocess on that file or (2) by using the Lean language server. The latter has a light weight wrapper around it in https://github.com/leanprover-community/lean-client-python. It is for Lean 3, but you could adapt it to Lean 4. Honestly the most important part of that previous project is just to handle the asynchronous communication correctly. The rest is just unnecessary converting the JSON API into Python types. (Unfortunately I don’t think the Lean server protocol is well documented for either Lean 3 or Lean 4.)

There are also projects like Lean-Gym (Lean 3) and Lean Dojo (Lean 3 and Lean 4) and Lean REPL (Lean 4), but these are very specific to a particular task, so may not fit your use case. You could also use Lean’s meta programming to build your own custom interface. LeanAide (Lean 4) did this for autoformalization and was able to use information about Lean’s library and type checker as feedback in the autoformalization process. But this is more work.

[Jason Rute]

Eric Rodriguez said:

Why aren't you using lean4?

While it is good to push people to Lean 4 I don’t think this community fully appreciates how much trouble that is for AI research. There has been a lot of work already done in Lean 3 and many of the LLMs still spit out Lean 3 instead of Lean 4.

[秋天]

oh thank you so much. as some dataset is only availble in lean3 . have no choice :face_in_clouds: