Cheating detection in Lean?

Stream: new members

[Adomas Baliuka]

Suppose some evil person wroteEvilStuff.lean and is trying to trick you into giving them a prize because they proved the Riemann hypothesis. Their EvilStuff.lean is maybe millions of lines long and you'd rather not even open it. They give you a file like this to look at in order to convince you:

import Mathlib
import EvilStuff

theorem proof_of_riemann_hyp : RiemannHypothesis := by
    exact Evil.actual_proof

What are the possible ways that the evil person could cheat? How can you detect it?

I can think of the following things the evil person could do:

• using axiom => Look at the output of #print axioms (But for some reason it doesn't work for me: "unknown constant 'axioms'")
• using macros (lots of ways) => detect how?
• redefining RiemannHypothesis => Prefix it by the explicit Mathlib namespace?
• Trick you installing a modified version of Mathlib (e.g. some man in the middle attack) => hash it and check against GitHub?
• Find a bug in Mathlib (e.g. RiemannHypothesis isn't actually the Riemann hypothesis) => Read all the definitions in Mathlib leading up to it? (no easier way I guess?)
• find a bug in the kernel => admitted. Congratulations to the evil person.
• More ways???

I think being very clear about this question (ideally, having an exhaustive list) can be very useful and might also be worth a page in the tutorial. Maybe there have been discussions about this before; sorry if I failed to find them.

[Johan Commelin]

#print axioms proof_of_riemann_hyp should work

[Johan Commelin]

You might be interested in https://www.brics.dk/RS/97/18/BRICS-RS-97-18.pdf

[Johan Commelin]

ab said:

• Find a bug in Mathlib (e.g. RiemannHypothesis isn't actually the Riemann hypothesis) => Read all the definitions in Mathlib leading up to it? (no easier way I guess?)

Another option is that people prove conditional results using RiemannHypothesis. If a buggy RiemannHypothesis still allows people to deduce some really nice consequences, then the bug is not a bug but a feature. But the more likely option is that such bugs will be quickly found if we try to use RiemannHypothesis.

[Adomas Baliuka]

@Johan Commelin Thanks for the paper. I guess that I want to follow the suggestion there and "import the proof object from Evil without importing any macros or definitions". Then, have the Lean kernel check the proof. Is there a way to do that? Is it enough to replace import EvilStuff by something that doesn't leak any macros or other definitions into my namespace?

[Johan Commelin]

No, that isn't really possible in Lean afaik.

[Johan Commelin]

But what you can do, is import EvilStuff and import Mathlib.

[Johan Commelin]

If EvilStuff tries to shadow definitions in mathlib then Lean will complain. And since Mathlib has a statement of RiemannHypothesis, you should be able to prove that statement easily from the version that EvilStuff has proven. If that is not possible, then the authors of EvilStuff have more homework to do.

[Johan Commelin]

So now you are reduced to trusing Mathlib. That's a different question. Depending on your level of paranoia, it should be relatively easy to convince yourself that the statement in Mathlib is correct.

[Adomas Baliuka]

Let's say I trust Mathlib and only deeply distrust EvilStuff. You're saying I should reverse the order of imports? That still doesn't take care of evil macros, right?

[Adomas Baliuka]

Is there something I can read about how this shadowing works?

[Eric Wieser]

EvilStuff can call arbitrary C code at import time which could presumably interfere with the memory space used by the kernel

[Eric Wieser]

Regarding macros, I thing the solution is to load the lean file from within another lean program, and extract the proof by reflection rather than attempting to use syntax to verify it

[Adomas Baliuka]

Eric Wieser said:

Regarding macros, I thing the solution is to load the lean file from within another lean program, and extract the proof by reflection rather than attempting to use syntax to verify it

Sounds interesting. Can you point me towards any resources on how to do that?

[Adomas Baliuka]

I would have thought that it should be possible to "save a proof to a file". If EvilStuff has a proof of RiemannHypothesis, no definitions within EvilStuff need to be visible to the outside. So that proof term should be just a data blob, which could be stored to a file and read in by another Lean program without allowing it to execute arbitrary code?

[Jason Rute]

As for saving a proof to a file, I think that is what the export format is for. The proof can then be checked by an external checker, and one wouldn't have to worry about macros and such. Only the pure kernel proof is exported. Also an external checker would also help check possible bugs coming from Lean 4's implementation of its kernel.

[Jason Rute]

I could be mistaken, but I also thought there was a way for Lean 4 to read it's own exported proofs (and that an early version of Mathport did this to convert Lean 3 to Lean 4 at the level of the kernel proofs). Maybe that is what @Eric Wieser meant with "reflection".

[Jason Rute]

Of course practically, if a proof was particularly important like the RH, I assume the community would put a lot of work into checking not only the Lean proof, but also the statements of the theorem to ensure that no funny business was going on. For a good idea of how that might look, see the discussion on checking the definitions in the Liquid Tensor Experiment.

[Jason Yuen]

Johan Commelin said:

#print axioms proof_of_riemann_hyp should work

axiom prοpext : False

theorem my_proof : 2 + 2 = 5 :=
  prοpext.elim

#print axioms my_proof  -- 'my_proof' depends on axioms: [prοpext]

Please ignore the fact that prοpext uses the omicron ο.

[Jason Yuen]

Of course, computers can tell ο and o apart, so this trick wouldn't fool a computer.

[Jason Yuen]

Jason Rute said:

As for saving a proof to a file, I think that is what the export format is for. The proof can then be checked by an external checker, and one wouldn't have to worry about macros and such. Only the pure kernel proof is exported. Also an external checker would also help check possible bugs coming from Lean 4's implementation of its kernel.

This command isn't working for me. Do you have an updated version of the command?

> lean --export=export.out --recursive
C:\Users\jason\.elan\toolchains\leanprover--lean4---nightly-2023-07-12\bin\lean.exe: unknown option -- export=export.out
Unknown command line option
Lean (version 4.0.0-nightly-2023-07-12, commit 6e904421304c, Release)
Miscellaneous:
  --help -h          display this message
  ...

[Jason Rute]

Sorry that was Lean 3. This might be the lean 4 version: https://github.com/Kha/lean4export