LeanDFumt — Error Database Lean 4 エラー解決データベース — zero-sorry 規律を保つ修正法

Common Lean 4 errors, each with a minimal reproduction and a fix that preserves the zero-sorry, no-Mathlib discipline used by the LeanDFumt library. Examples use DFUMT8 where natural, but each entry stands on its own as a general Lean 4 reference.

Why this exists

LeanDFumt ships 29 zero-sorry theorems for eight-valued logic with no Mathlib dependency. When users extend the library or embed it in their own proofs, the same handful of Lean 4 errors surface repeatedly. This database records those errors and the fixes that keep the discipline intact — no sorry, no new axiom, no Mathlib import.

Errors

• sorry in proof

  declaration uses 'sorry'

  A sorry placeholder remains in a completed proof. Discipline: zero-sorry.

• axiom bypass

  (policy detection — no compiler error)

  A new axiom declaration was introduced to sidestep a proof. Discipline: axiom-minimality.

• Classical.choice smuggled

  (silent — #print axioms reveals Classical.choice)

  A theorem depends on Classical.choice without declaring it, breaking the decide-only constructive discipline.

• native_decide bluff

  (silent — Lean.ofReduceBool appears in #print axioms)

  A proof closes with native_decide outside the numeric-anchor whitelist, silently widening the trust root to the native compiler.

• unsafe escape

  (silent — unsafe modifier / unsafeCast escapes kernel checks)

  An unsafe def, unsafe theorem, or unsafeCast bypasses termination or totality checks in the algebraic core.

• noncomputable ghost

  (silent at decl; #eval or native_decide fails to reduce)

  A noncomputable def passes type-checking but cannot be reached at runtime, breaking the fully-computable promise of LeanDFumt.

• hypothesis stripped

  (silent — cross-version signature diff required)

  A public theorem's signature has become strictly weaker between versions (a hypothesis dropped) while the name stayed the same. Only a baseline diff catches it.

• partial def ghost

  (silent — partial def is opaque; theorems about it are vacuous)

  A partial def in the algebraic core cannot be unfolded in proofs; theorems that reference it slip through with trivially-true bodies.

• @[implemented_by] override

  (silent — decide and native_decide disagree)

  An @[implemented_by native_impl] attribute substitutes a runtime body for the declared one; native_decide proofs about the symbol then trust an unchecked impl.

• initialize env pollution

  (silent — load-time environment mutation)

  A top-level initialize block mutates the elaboration environment (attributes, simp sets, hooks) before downstream files load, invisibly to any per-expression check.

• universe downcast

  (silent at claim; fails at downstream .choose)

  An existence claim proved in Prop (∃) yields no computable witness; downstream .choose uses fail or silently pull in Classical.choice.

• type mismatch (Nat vs Float)

  type mismatch ... has type Nat but is expected to have type Float

  Numeric expression is Nat where Float is required. Common when adding numeric anchors.

• Mathlib dependency introduced

  unknown module Mathlib.… / unknown identifier

  Code was written assuming Mathlib is imported. Discipline: no-Mathlib.

• unassigned metavariable

  don't know how to synthesize implicit argument

  Elaborator cannot infer a type or instance. Explicit annotation resolves.

• unknown constant (after rename)

  unknown constant 'Nat.succ_eq_add_one'

  Lemma or definition was renamed between Lean 4 versions. Discipline: track toolchain pinning.

Detection: CHECKER_SPEC

Each entry maps to a rule in Rei-AIOS's CHECKER_SPEC, which exposes two locators:

• locate_first_error(kind) — position of the earliest fault of the given kind under a stable source-order traversal.
• boundary_report(kind) — enumeration of policy violations at the axiom / import boundary.

The Detection section on each page names the applicable rule and its expected output shape.