Post #4301116

In a previous wave of Lean discourse, there was discussion about the fact that type-checking a Lean file can run arbitrary code. There are pros and cons to this, but one particularly obvious con is, well, let's just hear Kevin Buzzard's version: "One cannot trust AI-generated code so I ran [the AI-generated formalization of the Erdős unit distance conjecture counterexample] in a sandbox on my machine (malicious Lean code can run arbitrary commands on your computer — Lean is a programming language, after all)." (https://xenaproject.wordpress.com/2026/07/20/human-mathematicians-are-being-outcounterexampled/) My beloved LaTeX is another example of a tool in which you can write arbitrary code that generates a document of some kind, but in this case it can only do real damage if you pass the `--shell-escape` flag. As far as I can tell, Lean doesn't have an equivalent "sandboxed" mode. Am I missing something? Why isn't this something people want?