Missing Lean proofs

Scope. integ5 has 499 failing Dafny lines. This report covers the 267 of them where the Lean proof skips only 1–3 source lines at that point (gaps/lines.jsonl: 209 lines miss 1 Lean line, 32 miss 2, 26 miss 3; 192 out-of-resource, 75 errors). Three reviewers had assigned each line a fix task:

How this report was produced (details in §5):

1. The lines were grouped into 37 clusters (c001–c037).
2. Two independent analysts studied each cluster: ROOT asked "why does it fail?" and FIX asked "what closes it?" (gaps/out/*.json, ~2,600 Dafny outputs under gaps/work/).
3. One synthesis per task (gaps/task/<TASK>.md).
4. Two skeptic passes per task tried to refute each synthesis (gaps/task/<TASK>.skeptic*.md).

This report keeps only the mechanisms that the skeptics confirmed or partly confirmed, and says where they corrected something.

Terms used below

• Line lemma. One failing Dafny line cut out of its theorem file into a standalone lemma with the same hypotheses (requires) and goal (ensures). The "trimmed" version keeps only the hypotheses a static trimmer judged relevant.
• Closes. Dafny verifies the line lemma, or a hand-built equivalent, under the corpus flags. Every "closes" in this report is a standalone check. No theorem file was re-verified.
• OOR (out of resource). Z3 used up its budget of 1,000,000 resource units before finishing.
• Matching loop. A universally quantified fact that, each time Z3 uses it, creates a new term that triggers it again. Z3 keeps instantiating it until the budget is gone.
• Trigger. The term pattern Z3 waits to see before it uses a "for all" fact. With no usable trigger, the fact is never used.
• Harvest record. The per-tactic log extracted from Lean's proof term: which lemma was applied, with which arguments. The translator only cites lemmas that a record backs (the "record-only policy").

T1 — Lean's computed values are reduced to a comment (35 lines: mathd_numbertheory_618 ×32, amc12a_2021_p18 ×3)

• What is missing. The numeric fact Lean computed, for example Nat.gcd 691 52 = 1 or (5:ℚ)*5 = 25.
• Why.
  • The harvest has the record, with the numbers. For example isNat_gcd at exec 479 has x=691, y=52, z=1.
  • The translator's loader keeps only the lemma's name for these "internal" norm_num records, throws the arguments away, and prints // UNCITED-APPLIED internal ×N.
  • Dafny can evaluate gcd(691, 52) itself, but only when every argument is a literal. In the file it sees gcd(p(26), 2*26), where p is a local function.
  • For ℚ there is a second problem: Dafny knows two ℚ values have the same real value, but nothing says that makes them equal.
• Where. dafny_emit_v2.py:3005-3024 (the loader drops the arguments and continues); drop_sweep.py:247,636 (writes the comment); the library has no Rat.cast_injective.
• Example. mathd_numbertheory_618-315, the branch n = 26 of an interval_cases:

  Dafny  : assert false;  // sub-goal of norm_num
           (under the guard 1 < gcd(p(26), 2*26), with requires forall x :: p(x) == tsub(x*x,x)+41)
  Lean 45: interval_cases n <;> norm_num [h₀, Nat.gcd_eq_right, …] at h₄ ⊢      -- goal: False
  record : Tactic.NormNum.isNat_gcd (691, 52, z = 1)
  fix    : assert gcd(691, 52) == 1;   // norm_num evaluation (Lean exec 479)

• General fix. Transcribe the numerals that are already in the record into a checked assert <term> == <value>;. Use this only where Dafny cannot evaluate the term itself. For ℚ, add the axiom RatCastInj (= Mathlib Rat.cast_injective) and call it for each isNat_mul/isRat_mul record.
• Correction (skeptic). The fix must transcribe the record's own numerals. It must not fold constants in the translator: gcd(691, 2*26) is OOR, while gcd(691, 52) verifies (runs s01/s02).
• Tests.
  • All 32 branches of 618 close as minimal lemmas, and on the verbatim 40-branch block (669 verified).
  • The skeptic built its own control for n = 38: it fails without the assert and verifies with it.
  • The 3 lines of p18 close with RatCastInj.
  • Caveat: the minimal lemmas for 618-183 and 618-189 also close without the fix, so those two are partly a context effect.
• Corpus.
  • 618-139, the outer by_contra, stays OOR even after the fix.
  • 63 of the 499 failing lines carry IsNat/IsInt/IsRat records. That is an upper bound, and it is untested.
• Effort and risk. Small to medium. Soundness: none, since the asserts are checked. The only new axiom is RatCastInj, which is exact Mathlib and was Lean-checked by the analysts (needs approval).

T2 — Recorded lemma applications that never become a call (10 lines)

• What is missing. A lemma call that Lean made and the harvest recorded. The library has the lemma.
• Why. There are two routes:
  • (a) The loader discards records whose name is not a key of the citation table, before they reach the citation path. The specialised mapping injOn_cos.eq_iff → RealInjOnCosEqIff is therefore dead code. The same filter drops Nat.mod_mod_of_dvd, Int.card_Icc and Finset.Icc_eq_empty_of_lt.
  • (b) The record's arguments do not fit the Dafny signature. In orderOf_eq_iff the ZMod modulus is inside a type. Finset.mul_sum is over a set<nat>.
• Where. dafny_emit_v2.py:3009-3024 (loader); _cite_state_args :5609 / :5543 (projection).
• Example. amc12a_2021_p19-1352:

  Dafny  : assert (x == (Real.pi() / 2.0)) by {…}
           // UNCITED-APPLIED Set.InjOn.eq_iff …: library counterpart RealInjOnCosEqIff … exists
  Lean 126: apply (injOn_cos.eq_iff ⟨…⟩ ⟨…⟩).1        -- goal: x = π/2
  record : Set.InjOn.eq_iff(Icc 0 π, cos, x, π/2), in_table = false (exec 1563)

• General fix.
  • Admit records at load time: re-key them to the specialised entries, and add an alias table from internal names to existing exact lemmas (Nat.mod_mod_of_dvd → NatModModTotal, …).
  • Add argument adapters: take the ZMod modulus from the type; map mul_sum to FinsetMulSumPointwise.
• Tests. Closed: 855, 1352, 1564, 545, 366, 40, 224 (both lenses). 32 is closed only half record-backed (s06). 197 is not closed: the cite is right, but the context is still OOR.
• Corrections (skeptic).
  • mathd_algebra_170-285 has no record: its Lean step is a kernel rfl. Its fix (IntIccCard) is a goal-pattern guess, so it is not T2.
  • imo_1959_p1-32 (labelled LIBRARY) is blocked by the same loader gate. The synthesis did not list it.
• Corpus. The harvest has 12,827 internal, not-in-table records; most are glue.
• Effort and risk. Small (loader, table) to medium (adapters). Sound when existing exact lemmas are used. IntIccCard is a derived axiom, not literal Mathlib. The new Real.div lemmas (div_div, div_mul_eq_mul_div, mul_div_assoc') were Lean-checked. Both need approval.

T4 — One Lean object, two Dafny encodings, and no bridge between them (15 lines)

• What is missing. A trivial fact saying that two Dafny spellings of the same Lean object agree.
• Where the seams are.

  seam	Dafny side	lines
  ℕ product rendered as an int	Dafny then asks to prove 0 <= k*Int.pow(2,n+4), which has no Lean counterpart (lean_expr_ir.py:218, _need_cast)	amc12_2001_p5-11, 3pow… 124/146/177/261/283/314
  use w on a divisibility goal	use w only states b == a*w; Dafny's IntDvd is %-based and there is no Dvd.intro	516 (452: see correction)
  x*x vs Real.pow(x,2)	statements unroll literal exponents to products, but cite arguments and library postconditions keep Real.pow(·,2)	222, 530
  Real.div vs /	LeDivIff is stated with /, the goal uses Real.div	949
  Irrational	the predicate is opaque; exact h ⟨2, _⟩ becomes a GAP comment	198
  Icc membership vs bounds	a ∀ restatement guards with k in IccN(a,b), the facts use a <= k <= b	212
  numeral cast not folded	rpow(2.0, (2 as real)*(m*n)) vs rpow(2.0, 2.0*(m*n)) are different terms	137

• Example. numbertheory_3pow2pownm1mod2pownp3eq2pownp2-124:

  Dafny  : assert NatDvd(Int.pow(2, (n + 4)), (k * Int.pow(2, (n + 4)))) by {…}
           -- the failing check is the hidden "is k*Int.pow(2,n+4) a nat?"
  Lean 52: exact ⟨k, by ring⟩          -- in ℕ, so there is no sign obligation
  fix    : IntMulNonneg(k, Int.pow(2, n+4));   -- verified 51/0

• General fix. One rule: never emit the two sides of a step in different encodings without a bridge.
  • Use IntMulNonneg for ℕ products.
  • Add IntDvdIntro/NatDvdIntro (= Mathlib Dvd.intro).
  • Use one renderer for squares.
  • Restate LeDivIff and its 15 siblings over Real.div.
  • Use NotIrrationalNatCast.
  • Fold numeral casts.
  • Longer term: a nat-valued pow.
• Tests. 13 confirmed closes (516, 198, 137, 11 re-run by the skeptics).
• Corrections (skeptic).
  • aime_1987_p5-452 is not a missing bridge. Its untrimmed line lemma already verifies without any fix. The trimmed lemma fails only because the static trimmer dropped Lean's hypothesis h₂₁₂. In the file it is OOR, so it is a context line.
  • 949 likewise closes standalone without a fix.
  • The fix is a family of seven small rules, not one rule.
• Corpus. 459 non-literal products passed to nat slots in 11 files; 14 failing lines with this nat-subset check.
• Effort and risk. Medium. The new axioms (Dvd.intro, Irrational.ne_rat, le_div_iff over Real.div) are exact Mathlib and were Lean-checked. They need approval.

T5 — A rewrite step is stated without the equality that justifies it (9 lines)

• What is missing. rw, ring_nf or field_simp rewrote inside a function (under √, %, /, or in a hypothesis). Dafny states the result but not the argument equality, and Z3 never connects F(e) with F(e').
• Where.
  • The recorded congrArg is dropped as "no library counterpart" (dafny_emit_v2.py:1402-1406; 1,431–1,433 such comments in 80 files, depending on the grep).
  • @tac-hyp restatements are emitted before the execution's cites (:11747-11823).
• Example. numbertheory_aoddbdiv4asqpbsqmod8eq1-184:

  Dafny  : assert NatDvd(8, ((4 * k) * (4 * k))) by {…}
  Lean 38: ring_nf at *                     -- goal: 8 ∣ (4k)^2
  fix    : assert (4*k)*(4*k) == k*k*16;    -- verified 12/0 (skeptic re-run)

• General fix.
  • Diff Lean's recorded before/after goals and assert each changed argument equality, on literal terms.
  • Emit cites before @tac-hyp asserts.
  • State instances of "for all" hypotheses inside forall-statements.
• Tests. Closed: 192, 415, 184, 945, 213 (which also needs the unrecorded Real.sqrt_one), 181.
• Correction (skeptic). For amc12b_2003_p17-101/-102 and amc12b_2021_p9-412 the instance is present and still useless. They close only when products under functions are rendered through one transparent ghost Mul(a,b), so they are really an encoding seam (T4 family). The ghost-Mul rule changes how library postconditions are rendered. Its effect on the 33,014 obligations that verify today is untested. This is the largest unquantified risk in the TRANSLATOR fixes.
• Effort and risk. Medium to high. Sound, because the asserts are checked and Mul is transparent.

T6 — Quantifiers rendered with nothing for Z3 to match (12 lines)

• What is missing. Nothing is missing as a fact. A "there exists" or "for all" fact is in scope, but its bound variable occurs only inside arithmetic, which Dafny will not use as a trigger. Alternatively, Dafny rejects the natural trigger f(n) as a possible loop, and the side-terms it picks instead never occur at the line.
• Where. lean_expr_dafny.py:556-632 (the ∃ branch never emits a trigger) and expr_render._render_quant :626-674. verify5 reports "Could not find a trigger" on each amc12a_2003_p25 line.
• Example. amc12a_2003_p25-43:

  Dafny  : assert (exists x: real :: (Real.sqrt(((a * (x * x)) + (b * x))) == 0.0));
           // hypothesis h₄ after simp
  Lean 21: simp at h₄ h₅ h₆ h₇ h₈          -- only removes `True ↔` / `True ∧`

  The skeptic's minimal pair, with identical bodies:
  • plain: fails;
  • with the arithmetic body lifted into a transparent ghost function: verifies.
• General fix.
  • (a) Lift each arithmetic subterm that contains a bound variable into a transparent ghost function, named by its structure, so hypothesis, restatement and goal share one name.
  • (b) For shifted recurrences f(n) = f(n-1)+1, assert Lean's instance at each ground f(t) (rule I).
  • Do not pin {:trigger f(n)}: run s08 went OOR.
• Tests. 43–47, 413 and amc12a_2017_p7-28/48/54/67/74 close. Rule I passes 81/0 on the whole helper. Not closed: amc12a_2003_p25-26.
• Corpus. 84 no-trigger warnings in 17 files; 41 loop-rejected triggers in 7 files.
• Effort and risk. Medium. Sound.

T7 — A local step checked against the whole theorem (5 lines; much larger corpus-wide)

• What is missing. Nothing is missing. Lean proves the step from a few named hypotheses. Dafny checks it with every earlier fact of the theorem in scope, and Z3 drowns.
• Where. The v2 emitter inlines every have/@tac-hyp (dafny_emit_v2.py:7745, :11818). Lean's per-step dependency record (have_deps) is harvested for 102 theorems, but v2 never reads it. Only the rules emitter does, opt-in (KMAX_TRIM).
• Example. imo_1992_p1-5471:

  Dafny   : assert (-(1) + p*q*r) == … ;  // hypothesis hk after ring_nf
  Lean 391: ring_nf at hk ⊢
  fix     : a helper lemma that requires only hk, called in place — verified 7/0

• Tests. Closed: 488, 5471. 564 is partial.
• Corrections (skeptic).
  • imo_1984_p2-1725 is only partly closed: its helper is still OOR because of the power loop (L1). That is the same reason imo_1966_p4-174 was moved to LIBRARY.
• Corpus.
  • 160 of 499 failing lines (62 in the gap set) close standalone, so context is a large residual cause.
  • About 60 consensus lines outside the gap set ask for the same isolation.
• Effort and risk. High: a new emission shape. Sound, because helper preconditions are re-checked at the call. The completeness cost was measured on the rules track: KMAX_TRIM took strict-clean files from 29 to 18.

L1 — The library's pow makes Z3 loop (the largest mechanism in the report)

• What is wrong. Nothing is missing. Lean treats 2^n as an opaque value. The library defines Int.pow/Real.pow recursively and repeats the recursion as a postcondition:

  ensures if k == 0 then p == 1 else p == b * pow(b, k - 1)      // MathPrelude.dfy:52-56, :90-96

  This causes three problems:
  • Matching loop. Z3 may apply the postcondition without bound: pow(2,n) produces pow(2,n-1), then pow(2,n-2), and so on, until the budget is gone.
  • Fuel split. Dafny writes the same pow(2,m) as two different SMT terms, one in the goal and one in the facts. Inside cos(pow(2,m)*x), Z3 cannot see that the goal is a fact it already has.
  • Transparent ℂ arithmetic. The ℂ add/mul/of_real bodies are visible and get expanded everywhere.
• Where. Generated from symbol_table.py:117-123, :183-191 and :540-543. The translator's use of ^ → pow is faithful.
• Examples.

  imo_1964_p1_2-95 (OOR)
    Dafny: assert !(((Int.pow(2, n) + 1) % 7) == 0);
           -- linear over the atom 2^n, with 2^n % 7 = 1 in scope
    Lean : a simp step
    Result: closes once the recursive postcondition is replaced.
  
  numbertheory_3pow2pownm1mod2pownp3eq2pownp2-510 (OOR)
    Dafny: assert NatMod(Int.pow(2,n+2) + k*Int.pow(2,n+3), Int.pow(2,n+3))
                  == NatMod(Int.pow(2,n+2), Int.pow(2,n+3)) by {…}
    Lean 141-142: have h₂ … whose nested h₃ is the identical statement
    Result: Dafny's own in-file query with only the recursive conjunct removed is unsat at 53,865
            (base: unknown at 1,008,025).

• Size.
  • Gap set: 43 LIBRARY lines, plus 60 lines filed as SOLVER M1, plus 11 SOLVER Complex lines (M2).
  • Corpus: the recursive-conjunct ablation closes 104 of 499 failing lines; fuel normalisation flips 30 of 45 imo_1966_p4 lines; 191 failing lines sit in procedures with a symbolic-exponent pow.
• The fix is not settled. Three syntheses recommend three different variants:

  variant	what it is	known good	known bad
  U2 (LIBRARY synthesis)	closed forms for k ≤ 6 + {:fuel 1,1}	hoisted imo_1966_p4 block 121/123	leaves imo_1964_p1_1-27 and imo_1966_p4-190 OOR (skeptic); fails pow(x,8)=pow(x,4)^2
  F33 (SOLVER synthesis)	{:fuel 3,3} + k==0 ⇒ p==1	0 of 12 regression probes fail	leaves amc12a_2021_p14-542/-548 and in-file 329/364 OOR
  W33 (preferred by the SOLVER skeptic)	non-recursive wrapper over a {:fuel 3,3} recursive pow	closes 542, 548, 535, 175-107	1 probe regression (x^3, symbolic base); untested on the imo_1966_p4 block

  All three variants are sound: they only remove a postcondition that Dafny proves, or change fuel. No axiom and no assume. Recommendation. Remove the recursive postcondition, adopt W33 or F33 plus emitting the existing PowSucc/IntPowSucc cites where Lean's ring normal form has pow(b,k+1), then decide by a whole-corpus run. A whole-corpus run is the only way to measure regressions, and it was not allowed here.
• Library integrity finding. The shipped MathPrelude does not prove its own Real.pow postcondition: a standalone check gives 136 verified and 1 error at :55. Nobody sees this, because included files are not verified. Both skeptics confirmed it.
• Complex part (SOLVER M2, 11 lines).
  • Cause: the visible bodies of Complex.add/mul/of_real, not Complex.pow (refuted in three lenses).
  • Fix: opaque Complex operations with proved field postconditions.
  • Tests: 7 closed, 3 partial, 1 untestable.
  • Corpus: 10 more failing lines outside the gap set close in raw replay with only the mul body removed.
• Effort and risk. About 6–15 lines in symbol_table.py plus ~30 for ℂ. Needs the user's corpus re-verify before adoption.

L2 — ℚ cannot conclude equality from equal values (5 lines; +12 with the same axiom)

• What is missing. Mathlib Rat.cast_injective. Dafny's ℚ operations are known only through their real value. A second layer: an always-on nonlinear postcondition to_real == num/denom on every ℚ term.
• Example. aime_1984_p1-35:

  Dafny  : assert (u(0) == Rat.add(u(0), Rat.of_int(0)))
  Lean 16: norm_num          -- internally add_zero

  It closes with RatCastInj.
• Fix (libB2, tested).
  • Add the axiom RatCastInj.
  • Drop the always-on to_real postcondition.
  • Make Rat.of_int/Rat.neg axiom functions with the exact Mathlib statements. Seven statements were Lean-checked (rc 0).
  • Translator: emit RatCastInj(lhs, rhs) before each ℚ equality, and make the ring-identity exemption sort-aware.
• Tests. All 5 close. The skeptic re-ran 35 and 1170 under libB2 as well. 12 more lines close with RatCastInj alone (aime_1984_p1 ×6, aime_1999_p11-1161, amc12a_2009_p2 ×2, amc12a_2021_p18 ×3).
• Corrections (skeptic).
  • The analysts' first version (libB) had 2 postconditions Dafny cannot prove. libB2 fixes that.
  • Unmeasured: the cost to ℚ order facts once to_real's postcondition is gone.
• Effort and risk. About 20 library lines plus one emitter rule. Axioms → needs approval.

L3 — The lemma Lean used exists in the library only at another type (18 lines)

• What is missing. A library lemma at the right type. For example, Finset.sum_singleton exists only for ℝ and ℤ, but every recorded use is at ℕ. Also missing: Nat.gcd_self_add_right, and Complex.re_sum/im_sum/ofReal_mul.
• Example. algebra_sum1onsqrt2to1onsqrt10000lt198-167:

  Dafny: assert Real.sum(IccN(2,2), k => 2.0*(Real.sqrt(k as real) - …))
                == 2.0*(Real.sqrt(2 as real) - Real.sqrt(1.0))
  Lean : norm_num, internally Finset.Icc_self + Finset.sum_singleton at ℕ

  Adding FinsetSumSingletonNat closes it (trimmed 8/0, original 14/0).
• Fix. Exact Mathlib axioms at the missing type, registered in the citation table. Decide in_table at emit time instead of freezing it at harvest time.
• Correction (skeptic). Of the "14 closed":
  • 7 close with new lemmas alone.
  • 1 (462) closes with an existing lemma, so it is a translator cite gap.
  • 6 (amc12a_2009_p15) close only together with hiding Complex ops (L1c) and a translator restructuring.
  • 4 are not closed (546, 1801, p15-45, p15-183 → SOLVER).
• Effort and risk. Small per lemma. Axioms → needs approval.

L4 — A library conclusion built in a shape Z3 cannot match (5 lines)

• What is wrong. A lemma builds a term inside its conclusion that Z3 cannot identify with the goal's spelling of it. For example, FinsetSumAddDistribRat concludes about the lambda x => Rat.add(f(x),g(x)), and Dafny lambdas are not extensional.
• Example. aime_1984_p1-175:

  Dafny  : assert Rat.sum(range(98), k => Rat.add(u(0), …)) == Rat.add(Rat.sum(range(98), k => u(0)), …)
  Lean 43: rw [Finset.sum_add_distrib]
  fix    : the proved twin FinsetSumAddDistribRatH(s, h, f, g), called with the goal's own lambda — closes

• Fix. Proved "argument-form" twins. The skeptic verified all four twins: they need no new axiom.
• Correction (skeptic). The library-shape diagnosis holds cleanly for 175 and 466 only:
  • 22 and 495 also need new axioms;
  • amc12a_2009_p6-28 closes standalone in base, so it is not a library gap.
• Effort and risk. Moderate (about 10 twins plus one argument kind). Low risk.

Do not adopt as written. The skeptic found that the analyst axiom NatAddMulModSelfLeft is ill-formed: it is a possible division by zero. Nobody saw this, because included files are not checked. It is not in any recommended fix.

The SOLVER label turned out to be mostly a symptom label. In 81 of the 87 lines Z3 is not missing a fact; a library or translator defect makes the query expensive.

Skeptic corrections.

• (a) For 44 of the 62 power lines, the unchanged library's line lemma already closes standalone. For those lines the evidence for S-M1 is only the in-file query replay. So "context size" and "power loop" are both sufficient explanations, and neither is necessary. The power fix is still the better one: a single library edit with no per-line scoping.
• (b) Some "symbolic-exponent" lines actually involve literal pows such as Int.pow(16,502).
• (c) The recommended fix should be W33 or reopened (see L1).
• (d) S-M6's 698 closed only with the cite placed by hand. The analyst's translator variant did not close it.

S-M3 example. algebra_abpbcpcageq3_sumaonsqrtapbgeq3onsqrt2-1725:

Dafny      : assert (2.0*Real.sqrt(2.0)) * (…sum…) >= (2.0*Real.sqrt(2.0)) * (3.0/4.0) by {…gcongr…}
Lean 146-148: gcongr <;> linarith

• The in-file call gcongr_mul_le_mul_left(3/4, S, 2*sqrt 2) fails, even though its conclusion is the goal verbatim. Dafny binds the arguments to temporaries, so the conclusion is "temp × temp". Dafny 4.11 also forces Z3's legacy arithmetic solver.
• Stating the same lemma as a ghost-function postcondition verifies 14/14.
• Corpus: 566 cite sites in 55 files have this shape. Inlining the temporaries in raw replay closes 36 failing lines.

S-M6 example. amc12b_2020_p21-569:

Dafny  : assert ((k as real)+15.0)*((k as real)+15.0) <= (n as real)
Lean 74-75: nlinarith [Real.sq_sqrt …, h₉]

• Lean's certificate pieces are called only under if (premise), even though the premise is a hypothesis.
• Asserting the guard and calling unconditionally: 14/14; without that change the same lemma fails.
• Corpus: 466 guarded calls in 37 outputs.

H4 — Lemmas used as bare constants are never recorded (8 lines, all amc12a_2021_p19)

• What is missing. cos 0 = 1, sin 0 = 0, cos(π/2) = 0, sin(π/2) = 1. The library has all of them (RealCosZero(), …), but they are called 0 times in all 101 outputs.
• Why. In Lean's proof term these theorems appear as bare constants, not applications. The harvester's walker ignores every node that is not an application.
• Where. harvest_goal_states.py:631: the catch-all | _ => pure ().
• Example. amc12a_2021_p19-1556:

  Dafny   : assert (Real.cos(x) == Real.cos(0.0));
  Lean 154: norm_num [h₅₁₅₄]        -- goal: cos x = cos 0; the proof term contains bare Real.cos_zero
  fix     : RealCosZero();          -- 29/0; without it: 28 verified, 1 error

• Skeptic controls.
  • The wrong constant (RealSinPiDivTwo() on line 1722) does not close the line. The fix is specific, not "any extra axiom".
  • On line 1668, a goal-pattern rule fails, because sin(π/2) appears only after rewriting. That is why the fix belongs in the harvest, not in a translator guess.
• Fix. A .const case in walkT that emits a zero-argument record. The existing translator path then cites it.
• Effort and risk. Small, plus a re-harvest. No new axiom.

H5 — simp's _auxLemma hides the user's hint lemma

• Example. amc12b_2020_p21-1245:

  Dafny   : assert (20 as real) <= Real.sqrt(400.0)
  Lean 258: norm_num [Real.le_sqrt, Real.sqrt_lt]
            -- simp wraps the hint as _auxLemma.1 := propext (Real.le_sqrt …)
  fix     : RealLeSqrt(20.0, 400.0)   -- 8/0; control: 1 error

• Skeptic addition. A Lean probe shows that aime_1987_p5-495 (labelled LIBRARY) is the same mechanism. Its _auxLemmas come from dvd_add_right and from a Mathlib-module simp lemma (dvd_mul_left). So the fix must also unfold Mathlib-module _auxLemmas, not only the user's hints.
• Corpus. 4 more lines of amc12b_2020_p21 outside the gap set close the same way. There are 898 "arguments unknown" comments in 63 files.
• Fix. When the head is _auxLemma.N, unfold it to the underlying theorem with its arguments.
• Effort and risk. Small, plus a re-harvest.

H1 — class-field aliases are dropped (mathd_algebra_156-251, -313; aime_1990_p4-205)

Dafny: assert ((x*x-2.0)==0.0) || ((x*x-3.0)==0.0)
Lean : apply eq_zero_or_eq_zero_of_mul_eq_zero h₇₂

• Why. The Lean constant is the class field NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero, which the harvester filters as a "projection".
• Fix. Map table keys to their resolved constants (an alias map). The FIX lens ran the patched harvest through the unmodified translator, and exactly these 3 lines gained the call.
• Tests. Controls fail without the call and verify with it. 205 already verifies standalone, so for that line the fix is plausible but unproven.

H2 — hypothesis-side records missing (5 lines)

Facts.

• Only 10 of 100 record files were made by harvest4, the version that records hypothesis rewrites. amc12a_2019_p21 has no record at all.
• There are 2,795 @tac-hyp asserts and 54 failing @tac-hyp lines.

Re-harvesting alone closes none of the 5 lines.

• mathd_algebra_756-231:

  Dafny: assert (a*Real.log(2.0)) == Real.log(32.0);  // h₄ after rw
  Lean : rw [Real.log_rpow …] at h₄

  The cite is in the file, 3 lines too late. The skeptic found that the record is mis-attributed to a later execution, not absent. Closing the line also needs a translator rule: emit cites before the @tac-hyp restatement.
• The 4 amc12a_2009_p15 lines also need term-bound ∀ instances (TRANSLATOR) and the Complex fix (LIBRARY).

H3 — one line (amc12a_2009_p9-388)

• linarith [h₅ 0, h₅ 1, …] after simp_all produces Eq.mp … h₅ 0. The harvester's instance test needs a bare hypothesis head, so nothing is recorded.
• Asserting h₅ 0 and h₅ 1 closes the line.

3.1 Lines that moved between tasks

The script gaps/g3_corrected_tasks.py writes gaps/corrected_tasks.jsonl (one row per line, with the reason). Every move comes from a synthesis or skeptic finding cited above.

Lines needing more than one task. Primary task first, with the co-fix in brackets.

• LIBRARY [+TRANSLATOR] ×5: imo_1966_p4-174, -196, amc12_2001_p5-31, aime_1984_p1-192/-484.
• HARVEST [+LIBRARY] ×3: p15-496, -537, aime_1987_p5-495.
• SOLVER [+other] ×2: 546, p15-183.
• The 5 H2 lines need HARVEST plus a translator reorder, and for p15 also the Complex library fix.
• Context-modulated lines are kept under their stated task, but scoping (T7) may be what actually decides them in-file: 452, 949, 564, 618-183/-189, aime_1990_p4-205.

Interpretation. The consensus over-counted SOLVER by a factor of almost 9. Most "Z3 gives up" lines were caused by the library's power encoding. LIBRARY becomes the largest task, but it is dominated by one edit.

What was done.

• 37 clusters, each with two analysts (ROOT, FIX), except c006 (FIX output missing): 73 analyses.
• 4 syntheses (TRANSLATOR, LIBRARY, SOLVER, HARVEST).
• 2 skeptic passes per task.
• About 2,600 Dafny outputs stored under gaps/work/ and gaps/task/*runs*.

Flags. Every Dafny check used dafny verify --isolate-assertions --resource-limit 1000000 --allow-warnings --cores 2 with Dafny 4.11 (~/opt/dafny/dafny), the corpus flag set. Some checks also used --filter-symbol.

Skeptic run counts.

What "closes" means here. One standalone Dafny check of a line lemma (original or trimmed), a hand-built minimal lemma, or a hoisted helper.

• Fixes add only calls or checked asserts.
• A contract-diff check over about 100 TRANSLATOR fix files found the requires/ensures identical to the extracted lemma. Two variants removed requires, which only weakens the hypotheses and stays sound.
• No fix weakens a goal or strengthens a hypothesis.
• No assume was used.
• New axioms were Lean-checked by the analysts (lake env lean in ~/mathlib410). They were not re-checked in this stage.

What was NOT done, by rule or for lack of budget.

• No theorem file was re-verified. So no fix has an in-file result, and no regression on the ~33,000 obligations that verify today was measured. This matters most for the power fix (#1), Complex opacity (#4), ghost Mul (#9), ℚ libB2 (#2) and scoped emission (#11).
• No translator, library or harvester source was changed. Fixes were simulated by editing extracted lemmas or copied libraries.
• No re-harvest was run for H1, H3, H4 or H5. The FIX lens patched and ran the harvest for H1 only.
• Some in-file evidence is a raw SMT replay of Dafny's own query with one axiom conjunct removed (c018–c020), not a Dafny run. fxeq-318 is the case where the Dafny-level check timed out (2400 s).
• The power-fix variant (U2, F33 or W33) was not decided. Each has known lines it misses.

Why "closes standalone" is weaker than it sounds.

• 160 of 499 failing lines (62 in the gap set) close standalone without any fix. For those lines a standalone "closes with fix" proves nothing.
• The syntheses and skeptics flagged these cases:
  • 452 and 949: base closes;
  • 205: closes without the cite;
  • 44 of the 62 power lines: the base line lemma already closes.

Open contradictions (carried, not resolved here).

• The power-fix variant.
• aime_1983_p1-507: two different roots (call temporaries vs cast products); both fixes close it.
• imo_1984_p2-1685: reproducibility.
• fxeq-189/-229: the c019 replay says still failing; c020 says closed.

Files.

• gaps/GAPS_REPORT.md (this file) and gaps/GAPS_REPORT.html (same content, self-contained, not published).
• gaps/corrected_tasks.jsonl, written by gaps/g3_corrected_tasks.py.
• Inputs: gaps/task/*.md|json, gaps/out/*.json, gaps/lines.jsonl, SUMMARY.md, BLOCKSIZE*.md.