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...