Challenge status — openai/math @ adc7f124

One row per Comparator challenge (405). Build: the solution module compiled on the reviewer's machine. Closure: every constant in the challenge statement's transitive closure found alpha-equivalent to the solution's, no instance shadowing, only the three standard axioms (checker/). Comparator (laptop): the real leanprover/comparator accepted the solution on the reviewer's laptop, run with its development landrun shim (no sandbox). Comparator (Linux VM): the same check on an isolated Ubuntu VM with the real landrun (Landlock) sandbox, the citable configuration. Logs are in reviews/openai-math/evidence/lean_checks/.