unchecked-proof

A Lean proof that Lean takes on trust rather than checks.

Group

Lean proofs

Runs

On by default

Level

warning

Reads

Every file

Fix

None: a proof is the author's to write

Why

Lean's kernel checks every proof, except where the code asks it not to: sorry and admit accept a goal without a proof, an axiom assumes its statement, native_decide, decide +native, and bv_decide trust the compiler and the code it runs, @[implemented_by] runs other code in place of a definition, and set_option debug.skipKernelTC true skips the kernel. A theorem that relies on one is not proved, whatever its build says. Files of tests, which use sorry on purpose, are not reported.

The fix, as Ur suggests it: write the proof, or prove the goal with a tactic the kernel checks.

For agents

Prove every Lean theorem: leave no sorry or admit, declare no axiom, and prove decidable goals with decide rather than native_decide.

def balance (entries : List Int) : Int :=
  entries.foldl (· + ·) 0

theorem balance_append (xs ys : List Int) :
    balance (xs ++ ys) = balance xs + balance ys := by
  sorry

$ ur lint --rule unchecked-proof
warning[unchecked-proof]: `sorry`: Lean accepts the goal without a proof
  --> ./Ledger.lean:6:3 `sorry` in theorem `balance_append`
  = hint: write the proof, or prove the goal with a tactic the kernel checks
0 clone classes and 1 proof finding in 1 file
Lean proofs: 0 of 1 theorem proved (0%), 1 unproved