debug.skipKernelTC true

Stream: lean4

[Kevin Buzzard]

I had thought that any bogus proof of FLT would be spottable with #print axioms, but this was just pointed out to me on the Xena Discord:

import Mathlib

section

set_option debug.skipKernelTC true
elab "so_sorry" : tactic => do
  Lean.Elab.Tactic.closeMainGoal `so_sorry (Lean.mkConst ``trivial)

def f : False := by so_sorry

end

theorem easy : FermatLastTheorem := f.elim

#print axioms easy -- 'easy' depends on axioms: [propext]

I am surprised that debug.skipKernelTC true isn't "infectious" like partial or native_decide. This means that I cannot trust any proof, even if #print axioms only mentions the standard three which are allowed in mathlib/FLT? I need to run it through a typechecker? (which will of course spot this hack).

[Bhavik Mehta]

See also #general > PSA about trusting Lean proofs, it looks to me like similar stuff is going on. That is, closeMainGoal is also adding a decl to the environment, and the debug option is turning off kernel-checking at that point

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

I would say you should run it through a typechecker because axioms can also be redefined, so even without skipKernelTC just checking #print axioms is insufficient.

[Kevin Buzzard]

OK the message has finally sunk in :-)

[Niels Voss]

Here's an example of adding a bad declaration without using the debug.skipKernelTC option:

import Mathlib.NumberTheory.FLT.Basic
import Lean

open Lean

def myBadTheorem : TheoremVal where
  name := `bad
  levelParams := []
  type := Lean.mkConst ``False
  value := Lean.mkConst ``trivial
  all := []

#eval show CoreM Unit from do
  let currentEnv ← getEnv
  match Lean.Kernel.Environment.addDeclWithoutChecking currentEnv.toKernelEnv (.thmDecl myBadTheorem) with
  | .ok env =>
    setEnv (Environment.ofKernelEnv env)
  | .error _ => throwError "didn't work"

theorem flt : FermatLastTheorem := bad.elim
#print axioms flt -- 'flt' depends on axioms: [propext]

[Kevin Buzzard]

Thanks Neils (nb who was the person who brought this to my attention on Discord). Yes I had suspected that "grep for debug.skipKernelTC" would not be enough.

[Kim Morrison]

We really need to make lean4checker a default part of the CI runs for new projects...

[David Renshaw]

I just want to mention here that the existence of debug.skipKernelTC is what made me doubt the validity of grind proofs here: #Machine Learning for Theorem Proving > A (semi)-autoformalization challenge: 650=>448 @ 💬

[David Renshaw]

Ah, I had been under the impression that debug.skipKernelTC was enabled by default for bv_decide, but apparently it's not: https://github.com/leanprover/lean4/blob/b7b95896aa6466eede97ccdc54e36e73d1e0c524/src/Lean/Elab/Tactic/BVDecide.lean#L32-L34

I would be uncomfortable if tactics in the core library relied on environment hacking by default. Fortunately, it seems that's not the case. :)

[Henrik Böving]

David Renshaw said:

Ah, I had been under the impression that debug.skipKernelTC was enabled by default for bv_decide, but apparently it's not: https://github.com/leanprover/lean4/blob/b7b95896aa6466eede97ccdc54e36e73d1e0c524/src/Lean/Elab/Tactic/BVDecide.lean#L32-L34

Why's that?

[David Renshaw]

Discussion on the Xena Discord that I had skimmed. (And poor reading comprehension on my part.)

[Eric Wieser]

bv_decide does use ofReduce(Bool|Int) though

[Henrik Böving]

We only have ofReduceNat not for Int unfortunately, bv_decide also only uses ofReduceBool.

[Eric Wieser]

So you can't distinguish a "safe" bv_decide application from one of the things in #general > Using `native_decide` to prove False? from the axioms alone

[Eric Wieser]

Henrik Böving said:

We only have ofReduceNat not for Int unfortunately, bv_decide also only uses ofReduceBool.

Can you remind me when ofReduceNat is used? Int was indeed a typo :)

[Henrik Böving]

Nobody uses it

[Eric Wieser]

Is it even possible to use by hand?

[Henrik Böving]

Totally

[Asei Inoue]

@Niels Voss

Your example now does not work. Does this mean that the issue was addressed by an update to Lean?

[Mario Carneiro]

No, the interface changed but you can still do basically the same thing:

import Mathlib.NumberTheory.FLT.Basic
import Lean

open Lean

def myBadTheorem : TheoremVal where
  name := `bad
  levelParams := []
  type := Lean.mkConst ``False
  value := Lean.mkConst ``trivial
  all := []

#eval show CoreM Unit from do
  let currentEnv ← getEnv
  match currentEnv.addDeclCore 0 (.thmDecl myBadTheorem) none (doCheck := false) with
  | .ok env => setEnv env
  | .error _ => throwError "didn't work"

theorem flt : False := bad.elim
#print axioms flt -- 'flt' depends on axioms: [propext]

[Asei Inoue]

No, the interface changed but you can still do basically the same thing:

Thank you!!! :slight_smile:

Is the important point in this example the use of addDeclWithoutChecking?
Does this make it possible to do something similar to skipKernelTC?

[Niels Voss]

Yes, addDeclWithoutChecking is what skips the kernel type checking. However, there are probably other ways to do the same thing, so just removing addDeclWithoutChecking won't actually fix the core issue.

[Asei Inoue]

Is the following understanding correct?

• It is not considered a bug that APIs like skipKernelTC allow one to easily bypass Lean's kernel type checker and write fake proofs.

• Apart from using lean4lean, there is no known automatic method for checking fake proofs. In particular, there is no automatic way to check for fake proofs in editor environments like Lean 4 Web.

[Niels Voss]

Yes I think that is correct. At the same time, metacode could redefine the #print axioms command or modify the pretty printer to show misleading output, or execute malicious code that modifies the behavior of the Lean program to not track axioms.

[Niels Voss]

So really, no matter what you do, there's no way to verify the integrity of a lean proof from the web editor and I don't see how Lean could ever be changed for this to become possible

[Sebastian Ullrich]

Asei Inoue said:

• Apart from using lean4lean, there is no known automatic method for checking fake proofs.

This is incorrect. Any external checker will do, such as lean4checker already being run on Mathlib.