This is a special post for quick takes by Milo Moses. Only they can create top-level comments. Comments here also appear on the Quick Takes page and All Posts page.
An open question to Anthropic employees involved in the recent formalization of Fermat's Last Theorm:
In the official FLT Lean certificate on Github, why was the sandbox in the Lean comparator disabled, using the "fake-landrun.sh" command?
The sandbox on the comparator makes so malicious code in the proof can't mess up the statement of the theorem during the elaboration/compilation process. Without the sandbox one can imagine that instead of proving FLT, the agent swarm just learned to trick the comparator into mis-elaborating the theorem statement.
Yesterday I re-ran the FLT Lean certificate with the sandbox enabled (this just required changing a few lines of code) and everything seemed to check out, but I find it weird that the official version doesn't have the sandbox. It seems to point to Anthropic not using the sandboxed comparator in their broader use of Lean, which seems unsafe because one should expect that reward-hacking agent swarms might choose to trick the elaborator instead of proving theorems.
The relevant comment from the Github repo (in fermats-last-theorem/verification/comparator/run.sh) is attached below, which seems to assert that the proof is trusted so there's no need to consider the possibility that it includes malicious code. Maybe I have a different view of "trusted" as the person/agent who wrote the comment?
