Comparator

Comparator is a trustworthy judge for Lean proofs. It relies on having an existing Lean installation as well as:

1. landrun, compiled from the main branch's source, present in PATH
2. lean4export, at a version that is compatible with whatever Lean version your project is targeting, present in PATH
3. (optional) nanoda, compiled with a recent version of Rust. This is only necessary if you want to check with the nanoda kernel in addition to the builtin one. cargo build --release will place nanoda_bin in the target/release directory of the checked-out directory, this directory must be present in PATH

[!NOTE] Alternatively full paths to these binaries can be specified using the environment variables COMPARATOR_LANDRUN, COMPARATOR_LEAN4EXPORT, and COMPARATOR_NANODA when invoking Comparator.

Comparator is configured through a JSON file:

{
    "challenge_module": "Challenge",
    "solution_module": "Solution",
    "theorem_names": ["todo1"],
    "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"]
}

Where Challenge.lean contains at least a theorem named todo1 that has a sorry (or any other proof) and Solution.lean is provided by a party trying to convince you that they have proven todo1 by writing out the same theorem but with a proper proof attached.

Optional phase measurement adapter

A trusted caller may set measurement_command to a non-empty argv array. For the untrusted solution only, Comparator then invokes the adapter outside Landrun as:

<measurement_command...> --phase build -- <landrun> <args...>
<measurement_command...> --phase checker -- <landrun> <args...>

The build phase is emitted separately for the solution build and export. The checker phase is emitted for each configured external kernel. The adapter must transparently preserve the wrapped command's standard streams and exit status; it may aggregate wall time or performance counters in a location that untrusted code cannot write. Challenge build/export and the built-in kernel are deliberately not labeled as solution build or external-checker cost.

With no measurement_command, Comparator executes Landrun directly as before. An empty adapter argv is rejected rather than silently disabling measurement.

Given the following assumptions:

1. The transitive closure of imports of Challenge.lean as well as lakefile.toml/lakefile.lean are controlled by you or trustworthy.
2. You have not previously tried to compile the Solution file or any other potentially adversarial files (as that might compromise your Challenge file to make it seem like you are looking for a different proof than you actually are)
3. You have the landrun and lean4export binary in PATH
4. landrun works correctly on your system and Solution.lean does not exploit any bugs in landrun that allow a process to escape its sandbox
5. The Lean kernel is correct (with external_kernels this can be reduced to "At least one of the Lean kernel or the external_kernels is correct")
6. You are not running this under a privileged user

If the following command succeeds:

systemd-run --property=RestrictAddressFamilies=~AF_UNIX --user --pty -E PATH="$PATH" --working-directory $(pwd) -- bash -c 'lake env path/to/comparator/binary path/to/config.json'

All theorems in Solution that are listed in theorem_names are guaranteed to:

1. Prove the same statement as provided in Challenge
2. Use no more axioms than listed in permitted_axioms
3. Be accepted by the Lean kernel

[!NOTE] The Trusted Code Base of Landrun naturally includes the operating system and hardware it is running on, plus its sandboxing mechanism. The systemd-run part explicitly guard against a vulnerability in landrun, Comparator's current sandboxing solution, that will be fixed in Linux 7.1

Note that running lake exe cache get to download a Mathlib cache is acceptable before running the comparator if you trust the cache to not be modified as to, e.g. contain different definitions from the one you would expect.

Furthermore, it is possible to avoid trusting landrun's ability to sandbox the Solution.lean file: if you have obtained a fully pre-built .lake directory through other means and without compromising your checking environment, Solution.lean will not be rebuilt.

Checking with Additional Kernels

Comparator can additionally check solutions with external kernels. To do this you must register them in the external_kernels list:

{
    "challenge_module": "Challenge",
    "solution_module": "Solution",
    "theorem_names": ["todo1"],
    "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"],
    "external_kernels": {
        "mykernel": ["kernel_bin", "--threads=4", "--paranoid"]
    }
}

Comparator will execute the command described by the mykernel array and additionally pass a file, containing the solution export to the kernel, in this case: kernel_bin --threads=4 --paranoid export.ndjson

For backwards compatibility reasons users may instead set enable_nanoda: true to obtain a config that calls nanoda_bin. Furthermore, comparator currently attempts to detect nanoda-style kernels by checking whether the name contains the string noda and instead passing a nanoda-style config.json to them. This is only intended as a migration path while the kernel ecosystem moves toward having an option to receive the input file as a CLI argument.

For development purposes, comparator supports overriding nanoda specifically using the COMPARATOR_NANODA environment variable.

Definition Holes

Sometimes challenges want to leave open definitions for solutions to fill in. This can range from simple things like filling in a Prop valued definition to resolve whether a conjecture is true or false, all the way to constructing complex mathematical objects. For these types of solutions, comparator can guarantee that:

1. They use no more axioms than listed in permitted_axioms
2. They are accepted by the Lean kernel
3. The name, type, universe levels and safety levels of all definition holes match

Crucially, many definition hole challenges can be gamed without additional oversight. For example, given a conjecture-style challenge:

def ChallengeSolution : Prop := sorry
theorem challenge : RiemannHypothesis ↔ ChallengeSolution := sorry

a solution could define ChallengeSolution as:

def ChallengeSolution : Prop := RiemannHypothesis

and conduct a simple proof of challenge by reflexivity. The intention of the challenge though was of course to ask for a True or False value for ChallengeSolution. For this reason, all definition hole solutions must always be checked with an additional (potentially human) verifier.

To establish a definition hole, the challenge must provide it as a sorried definition:

def large : Nat := sorry

theorem large_lt : 37 < large := sorry

All of the holes must then be put into the definition_names field in configuration.json:

{
    "challenge_module": "Challenge",
    "solution_module": "Solution",
    "theorem_names": ["large_lt"],
    "definition_names": ["large"],
    "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"]
}

For all definition_names, comparator ensures that in the solution:

• the name, type, universe levels and safety level match
• the constant does not (transitively) refer to non-permitted axioms
• the constant type checks

Thus, the following solution would be accepted:

def large : Nat := 38

theorem large_lt : 37 < large := by decide

Development

The scripts/fake-landrun.sh can be used to replace Landrun in development if you are not on a Linux system that supports landrun.

The following commands, starting from the root directory of a fresh git checkout, will build and run comparator on one of the test examples:

lake build lean4export comparator

cd tests/projects/simple_mismatch

cat > lakefile.toml <<EOF
name = "comparatortest"
version = "0.1.0"

[[lean_lib]]
name = "Solution"

[[lean_lib]]
name = "Challenge"
EOF

COMPARATOR_LANDRUN=$(realpath ../../../scripts/fake-landrun.sh) COMPARATOR_LEAN4EXPORT=$(realpath ../../../.lake/packages/lean4export/.lake/build/bin/lean4export) lake env ../../../.lake/build/bin/comparator config.json

The following commands, starting from the root directory of a fresh git checkout, will build and run the tests:

lake build lean4export comparator
COMPARATOR_LANDRUN=$(realpath scripts/fake-landrun.sh) COMPARATOR_LEAN4EXPORT=$(realpath .lake/packages/lean4export/.lake/build/bin/lean4export) lean --run runtests.lean

Replace the landrun and lean4export arguments as needed, or place the binaries in PATH.

Internals

We generally adopt a policy of not loading olean files as they just get mmaped into our address space and then dereferenced and are as such a potential point of attack for sophisticated adversaries.

The comparator performs the following steps to ensure these properties:

1. Build Challenge using lake in a landrun sandbox that has:
   • read access to the entire file system and write access to /dev
   • write access to the .lake directory of the project
2. Run lean4export on the produced Challenge.olean in a landrun sandbox that has:
   • read access to the entire file system and write access to /dev
3. Repeat the same build sandboxed and export sandboxed steps with Solution
4. Verify that all declarations used in the statement of all relevant theorems in Challenge are the same as in the Solution environment. This always includes the declarations from Init with special meaning to the kernel. Both Challenge and Solution therefore need to import the default prelude.
5. Verify that the body of all relevant theorems in the Solution environment only uses axioms listed in permitted_axioms
6. Replay the Solution environment into the Lean kernel. Doing this within the same process as the comparator should be safe as the worst thing that can happen at this point is an exploit that makes the kernel accept when it should reject and that same exploit should also be applicable from within an external process.

Note that as Challenge is trusted, both the sandbox and lean4export step for Challenge are not necessary to the best of our knowledge. We still adopt these rather free measures as additional paranoia in case an adversary comes up with a means of attack anyway.

Acknowledgement

Comparator was originally developed by Lean FRO, with feedback from the AIMO team, in support of the AIMO series of competitions and their goal of enabling trustworthy LLM Lean evaluation on Kaggle.