Using lean 4 with python

Stream: lean4

[Kind Bubble]

I have some projects featuring Boltzmann machines, D_KL bounds, Shannon entropy, and error-bias tradeoff. I'm interested in using both python and Lean.

What are some ways Lean 4 can interact with python libraries such as numpy and scipy? I am interested especially in Lean 4 tactics which facilitate interactions with other programming languages such as Z3.

[James Gallicchio]

Lean's only interfaces with external world right now are the C foreign function interface (https://leanprover.github.io/lean4/doc/dev/ffi.html?highlight=import#foreign-function-interface) and command-line processes via IO (https://leanprover-community.github.io/mathlib4_docs/Init/System/IO.html#IO.Process.run)