An open-weight model proves a logic theorem — and shows its work

EnvironmentConstraints that shaped the work

The core argumentsExact, not gestured

Completeness — the measure argument

Proof search must terminate, and that requires a measure that strictly decreases on every rule's premises. Plain formula size does not work: the De Morgan rules (¬(φ∧ψ) → ¬φ, ¬ψ) preserve raw connective count (1 neg + 1 and = 2 negs). The fix is a negation-weighted degree: deg(¬φ) = 1 + 2·deg φ, deg(φ∧ψ) = deg(φ∨ψ) = 1 + deg φ + deg ψ, deg(atom) = 0. Under this weighting De Morgan strictly decreases (decreases by 1), double negation decreases, and everything else decreases under any positive weighting. The sequent measure is the sum over both lists; the 10 per-rule measure_* lemmas each prove strict decrease, and completeness is strong induction on that measure over the 12-way decompose disjunction.

Completeness — the canonical countermodel

The refuting valuation for a saturated sequent reads from the antecedent only: truth-support ts := atom p ∈ Γ, falsity-support fs := ¬p ∈ Γ, mapping (T,T)→b, (T,F)→t, (F,T)→f, (F,F)→n. This was re-confirmed twice by exhaustive evaluation over all four (ts,fs) cells. Reading falsity from the succedent is mathematically wrong: the saturated sequent {p,¬p} ⇒ {} would map p to t and leave the antecedent ¬p undesignated. Do not re-litigate — the failure log records the one time this was doubted, and it was a tactic bug, not a design bug.

Decidability — why the decision had to be proved in Prop

The decision argument mirrors completeness: strong induction on the measure, casing on decompose. The initial branch is derivable; the saturated branch is underivable (the refuting valuation + soundness); each rule branch recurses on its premises. The underivable branches close by the sound → invert → complete loop: if S were derivable it would be valid (soundness), so its premises would be valid (the matching inversion lemma), so they'd be derivable (completeness) — contradicting the recursive underivability result. No cut-admissibility is needed; the loop supplies it. The full reason the result is stated as a Prop disjunction rather than a PSum/Decidable value is failure #2 below.

Scope note (redlines from external review, conceded): this is decidability as a theorem, not an executable checker. Deriv is Prop-valued, so the Decidable instance is noncomputable and does not execute (verified: decide fails with dependsOnNoncomputable). Nothing here produces a runnable Bool-valued proof-search function; that would require Deriv in Type with its own termination proof — a separate, strictly stronger construction that is future work, not claimed.

Correction (2026-08-11) — the choice attribution: an earlier note here (and in the README) said the Classical.choice in decidable_deriv came solely from the Decidable lift. Wrong: derivable_or_not (the pure Prop proof) already carries [propext, Classical.choice, Quot.sound] because its negative branches call completeness. The lift adds nothing. The choice is inherited from completeness, not introduced by the instance.

Failure logOrdered, dated, with the fix

1. 2026-08-08 — False W from stale cache. A full lake build reported "Build completed successfully (8658 jobs)" while Completeness.lean had ~20 live errors; every job was a cache hit. Fix: module-targeted builds as the standing verification rule.
2. 2026-08-08 — replace_all corruption. A patch-tool replace_all on a perm-orientation fix matched an overlapping live pattern and clobbered 12 call sites. Fix: revert the whole region to the checkpointed green state; never replace_all a pattern that is a substring of another live pattern; one explicit patch per site when sites differ.
3. 2026-08-08 — Misdiagnosis trap. A mechanical case split produced an "unprovable" goal; the canonical valuation was doubted and nearly redesigned. Exhaustive #eval ground-truthing over all (ts,fs) cells confirmed the antecedent-only reading was correct — the bug was a <;> branch leak in the tactic block, not the design. Fix: when a "mechanical" split yields an unprovable goal, suspect tactic structure first, definitions last.
4. 2026-08-09 — Degraded tool-result channel (×2). A tool_call_id collision meant edits executed but results returned empty; the session could act but not see. Fix: stop proving immediately (never write Lean blind), write an early handoff marked "written blind — confirm intact before relying on it," and let a fresh session resume. The project survived two dead sessions on handoffs, not memory.
5. 2026-08-10 — Decision procedure eliminated into Type (×3). Tried to build the FDE decision as a value: PSum via Nat.strong_induction_on, PSum via WellFounded.fix, Decidable via strong_induction_on — all failed because Lean's Or/∃ recursors only eliminate into Prop, and decompose is a 12-way Or/∃. Fix: prove the decision as a Prop disjunction (⊢ₛ S) ∨ (¬ ⊢ₛ S) by strong induction, then lift to a Decidable instance via Classical.choice (the sole source of that axiom in decidable_deriv).
6. 2026-08-10 — Library root didn't import the new modules. FDE.lean originally imported only through Soundness, so the default target never compiled Completeness/Corollaries — the reason module-target builds were load-bearing. Fix: added both imports so the default build covers everything (job count 8658 → 8660 confirms).

Recreation recipeRebuild it from scratch

# 1. toolchain
export PATH=/opt/data/home/.elan/bin:$PATH
cd /opt/data/fde-lean

# 2. full build (all 5 modules — FDE.lean imports them)
lake build                       # → "Build completed successfully (8660 jobs)"

# 3. sorry scan — must be empty across all modules
grep -nE ":= *(by *)?sorry|admit|sorryAx|native_decide" FDE/*.lean   # → no output

# 4. axiom audit — run #print axioms on each theorem
#    expected: Deriv.sound [propext]
#              completeness, decidable_deriv, deriv_iff_valid [propext, Classical.choice, Quot.sound]
#              no_valid_formula, disjunction_property [propext]

Known limitsStated, not buried

The kernel-checked result and the faithfulness of the FDE encoding are separate claims. The encoding choices (designated = truth-support, the NNF-based invertible calculus, list-based sequents with explicit exchange) are documented in the source and the main page's design notes, but they are argued, not proved. A domain-expert audit of the encoding would strengthen the second claim and is an open invitation.

Scratch files (FDE/Scratch*.lean) are unreferenced leftovers outside the build — safe to delete, kept as a record of the probe-first workflow.