Applications of a Python ⇄ Lean API?

Stream: general

[Tate Rowney]

Hi everyone! My name is Tate, and I'm a student at Carnegie Mellon University doing research with Dr. Jeremy Avigad and others. I've recently been developing an API for sending data back and forth between Lean and Python (originally for other projects I've helped with). Given Python's large selection of interesting packages, I think this API could support some helpful tools or tactics; for example, I built a tiny proof of concept using Python's SymPy to solve 1d Riemann integrals:
Screenshot 2025-08-14 at 16.42.11.png

[Tate Rowney]

I was wondering whether y'all had any ideas/requests regarding potential use cases. This might entail making automation via computer algebra systems like SymPy, or integrating some simulation libraries from outside of pure math (as unreliable oracles: some applications from physics/chemistry come to mind). Any suggestions are greatly appreciated!

[Weiyi Wang]

:open_mouth:
How does it work? Does the proof use an additional axiom that trusts python result, or does the python side generate a proof using only the standard axiom set?

[Tate Rowney]

Right now it still uses a "trust Python" axiom: the idea (eventually) is to have it be of the form of "got a Python instance of X class with Y attributes => the answer is correct". Unfortunately it turns out that doing it like bv_decide (where computation occurs externally but a proof is reconstructed afterwards) is rather difficult because of how much weird (and not type-theoretically sound) stuff goes on under the hood, but it could be done for some simpler applications

[Jon Eugster]

a bit a different application but I think ot would be cool to have Lean bindings for python's plotting libraries (e.g. matplotlib), probably displaying the resulting plot to the infoview using proofwidgets

[Tyler Josephson ⚛️]

When developing the curriculum for Lean for Scientists and Engineers, we found that a whole category of relevant physics/chemistry problems are awkward to set up in Lean. These are “solve for x” kinds of problems - they are for CAS, but don’t seem like such a good fit for Lean. For instance: https://github.com/ATOMSLab/LFSE2024/blob/master/Lean%20Code/Lecture2.lean

Basically, a Lean version is “state that, given A, B, and C, prove that x=5” but typically, the scientist’s problem is “given A, B, and C, solve for x.” I think it would be neat to have some kind of framework where sympy solves for x, then slides that into the Lean conjecture to complete the theorem statement. If some form of “autocomplete” (e.g. an appropriate tactic or an LLM like AlphaProof) can generate a proof, then we have more confidence in the answer than we have from sympy alone. I wouldn’t know how to ensure no bugs in the sympy output —> Lean translation, though.

[Tyler Josephson ⚛️]

Maybe my specific case isn’t the best situation in Lean for which to build a “solve for x” kind of functionality. Another option might be how #eval can be used for “solving” basic arithmetic but doesn’t work with symbols. I’d like something that can handle this:

https://live.lean-lang.org/#codez=G4QwTgliBGA2CmACAFADwFwDkQBcCUAUAQMTyiyICsA1AOwBUAzPavQExA

[Tate Rowney]

Jon Eugster said:

a bit a different application but I think ot would be cool to have Lean bindings for python's plotting libraries (e.g. matplotlib), probably displaying the resulting plot to the infoview using proofwidgets

I really like this idea. The matplotlib backend should also be pretty trivial once things are set up; I think a #plot will be arriving soon!

[Tate Rowney]

Tyler Josephson ⚛️ said:

When developing the curriculum for Lean for Scientists and Engineers, we found that a whole category of relevant physics/chemistry problems are awkward to set up in Lean. These are “solve for x” kinds of problems - they are for CAS, but don’t seem like such a good fit for Lean. For instance: https://github.com/ATOMSLab/LFSE2024/blob/master/Lean%20Code/Lecture2.lean

Basically, a Lean version is “state that, given A, B, and C, prove that x=5” but typically, the scientist’s problem is “given A, B, and C, solve for x.” I think it would be neat to have some kind of framework where sympy solves for x, then slides that into the Lean conjecture to complete the theorem statement. If some form of “autocomplete” (e.g. an appropriate tactic or an LLM like AlphaProof) can generate a proof, then we have more confidence in the answer than we have from sympy alone. I wouldn’t know how to ensure no bugs in the sympy output —> Lean translation, though.

I think this is a super helpful use case: I've found quite a few pretty simple (in)equalities are quite annoying to solve even with automation, despite CASs making them trivial. While a "find solutions" or "just trust the CAS" strategy would be easy, actually reconstructing a working (and easy to read) Lean proof is more difficult because SymPy and family use a bunch of crazy Grobner basis stuff behind the scenes: however, it is definitely possible.
I do have a friend who was working a bit on integrating Macaulay 2 into Lean for something similar: continuing this could be a promising route if folks were interested.

[Jeremy Avigad]

Here's another thought: if you connect to a Python package that does interval arithmetic or some other sort of validated computation, you can get fairly reliable numerical estimates. These would not be formally verified (there is an industry for formally verified numeric computation, but it's hard), but it could nonetheless be a helpful trusted oracle for lots of scientific and engineering applications. Google turned up this paper, which might be a nice target.

Here is another numeric package that might be helpful. Sicun Gao and @Soonho Kong started working on this at CMU; Soonho was Lean's first developer with Leo, and a couple of years ago he told me that dReal was getting a lot of use at AWS. It's not a Python program, but there are Python bindings.

Plotting in widgets would also be great, as well as symbolic computation of integrals or factorization of polynomials. Finding integer or rational solutions to equations that can be verified automatically would also be great.

[Tate Rowney]

Thanks Dr. Avigad! I love the idea of integrating numerical simulations: interval arithmetic would be a great place to start, and could also help to eventually integrate complex simulation software (I think we discussed this before briefly?). Reliable work by the devs of these packages will be helpful to create reasonable axioms about the error bars of the outputs.

Also polynomial factoring would be a cool place to start as well, since once we've computed a witness creating the proof is just a matter of spamming a small collection of ring identities (quite a bit easier than full systems of equations).

[samuela]

I would be excited to be able to use JAX within lean. Would this be possible in your setup?

[Tate Rowney]

This is a very interesting application! It's most definitely possible (just point it at a Python installation with Jax installed), but with what I have now, it will be difficult to do any verification, etc. of the underlying computations since Jax is implemented informally for obvious reasons.
As a sidenote, Tomas Skrivan's SciLean project is (among many, many things) trying to formalize properties of neural networks in Lean. It's still under development, but could potentially be useful depending on what you're trying to achieve...