Can Lean REPL/LeanInteract be sandboxed?

Stream: Machine Learning for Theorem Proving

[Niels Voss]

I was wondering if on Linux it was possible to invoke Lean Interact or the Lean REPL in a sandbox like landrun or firejail or even docker. The use case is that we are taking user-generated natural language, feeding it to an LLM, and then running the generated Lean code, and I suspect that this is capable of arbitrary code execution.

[Sebastian Ullrich]

Mathlib CI uses landrun, you should be able to use that for inspiration

[Luis Scoccola]

I am using the Docker approach to play around with agents for autoformalization here. See in particular the Docker file.