Comparator

Comparator is a trustworthy judge for Lean proofs. It relies having an existing Lean installation as well as two additional binaries in PATH:

1. landrun compiled from the main branch's source
2. lean4export at a version that is compatible with whatever Lean version your project is targeting.

The comparator is configured through a JSON file:

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

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.

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 enable_nanoda this can be reduced to "The lean or the nanoda kernel are correct")
6. You are not running this under a privileged user

If the following command succeeds:

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 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 currently supports checking with the nanoda kernel in addition to the builtin Lean one. To do this you need to set the enable_nanoda flag in the JSON configuration to true. Note that this feature currently requires installing nanoda.

To make nanoda available to comparator, you need install a recent Rust version and compile nanoda using cargo build --release. Then you need to add the target/release folder of the nanoda checkout to PATH.

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 definitions:

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"],
    "enable_nanoda": false
}

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

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 mean of attack anyway.