axiom bypass 証明を回避するために axiom が追加された

Error message

Lean itself emits no error. This is a policy-level detection: any new axiom declaration outside the whitelisted set is flagged by boundary_report.

Lean 4 accepts axiom declarations silently. That is intentional — an axiom is a legitimate mechanism for asserting a primitive. But it is also the easiest way to bypass a hard proof, and the compiler will not warn about it. Auditing has to happen elsewhere.

Minimal reproduction

-- File: BadAxiom.lean
-- A user cannot prove `DFUMT8.and .BOTH .FALSE = .FALSE` cleanly,
-- so they assert it as an axiom.
axiom and_both_false_bypass : DFUMT8.and .BOTH .FALSE = .FALSE

-- Now depend on it as if it were proven:
theorem downstream : DFUMT8.and .BOTH .FALSE = .FALSE :=
  and_both_false_bypass

Build output: clean. No warning, no error. The bypass is invisible without an external checker.

Why it matters

Every axiom is a trust root. The LeanDFumt library's soundness claim reduces to: "given the axioms of Lean 4 core, these 29 theorems are true." Introducing a new axiom silently widens that trust root without acknowledgement. A downstream user has no way to know their proof depends on and_both_false_bypass rather than on decide-verified computation.

In practice, the FALSE-absorption case above is provable by decide. The bypass exists only because the author did not try the right tactic.

Fix

Delete the axiom and prove the statement. For LeanDFumt claims on the finite DFUMT8 type, decide is almost always sufficient:

-- Deleted: axiom and_both_false_bypass : ...

theorem and_both_false : DFUMT8.and .BOTH .FALSE = .FALSE := by decide

If a statement genuinely cannot be proved from Lean core — e.g. it encodes a physical postulate or an external oracle — the axiom must be declared in a designated whitelist file with a written justification. In LeanDFumt this whitelist is currently empty; the library is Lean-core-axiom-only.

Detection: CHECKER_SPEC

v0 primitive (available today — spec §4, Appendix A): not directly detectable through verify() alone. A file that declares a new axiom to close a goal still compiles, so verify() returns VALID on the downstream theorem. Enforcement in v0 is a pre-check that runs before handing the file to verify(): enumerate axiom declarations and reject any not in the project's AxiomWhitelist.lean. Rejected files never enter stats(), keeping decision_rate an honest measure of what was verified rather than accepted-by-policy.

Post-v0 Layer 2 (planned — spec §13): boundary_report(kind = "axiom") enumerates every axiom declaration in the project (via Lean.Environment.axioms) and filters out those in Lean core. Any remaining declaration is a policy violation and must appear in the project's AxiomWhitelist.lean to be accepted. Cross-check with #print axioms <theorem> at build time to verify each theorem's actual axiom dependencies match the whitelist. Layer 2 is a thin wrapper over v0 and does not introduce independent decision logic.

See also