Draft issue for leanprover/comparator — elaboration divergence field report (for review before filing)

comment-context.md

Context for reviewer

What this is

A proposed GitHub comment on leanprover/comparator#58 ("Comparator generates different instance names for problem and solution files"), cross-linking #59 ("Proof irrelevance is not respected in statements").

The reviewer who assessed our previous draft recommended this approach over filing a new issue.

Why a comment on #58, not a new issue

• The limitation is real — upstream comparator at 8d84e67 rejects our capstone theorem.
• But the upstream problem is already documented. #58 covers elaborator-generated names; #59 covers proof irrelevance. A new issue would mostly duplicate those discussions.
• A PR is premature — our local patches combine several equivalence mechanisms and need redesign before upstreaming.
• A field report comment adds evidence to the existing discussion and asks for guidance without claiming to have the fix.

What the previous draft got wrong (now corrected)

1. "Statement.lean doesn't help." → Now says the workaround would require a substantial refactor and has not yet been tested.
2. 10/19 → 19/19 from three patches → Corrected to 6/19 → 10/19 → 14/19 → 19/19, noting significant Challenge source alignment alongside comparator patches.
3. _proof_N all the same mechanism → Now distinguishes: one investigated pair had identical types+values under different names; a later _proof_8 involved differing types.
4. expectationL2 passes via comparator tolerance → Now explains it passes because it was added to definition_names, which stops checking its body, and notes this stretches the definition-hole contract.
5. "0-sorry" → Now qualified: the Malliavin library and Solution are zero-sorry; the Challenge intentionally contains sorries.
6. "structurally correct" → Replaced with "kernel-equivalent but structurally distinct."

What the comment deliberately leaves out (per reviewer recommendation)

• comparator-proof-bypass repo (the security pitfall story — only relevant if they ask about implementation approaches)
• The closed #85 / #86 (our retracted issue and PR — don't draw attention to the mistake)
• Detailed patch descriptions (save for a PR if invited)

Upstream context from #58 and #59

#58 (7 comments): Active discussion. hargoniX says auto-generated names can differ across files and the shared Statement.lean workaround only fixes one instance, not the general problem. eric-wieser distinguishes content-based vs non-content-based divergence. tadamcz agrees the workaround is a significant imposition.

#59 (1 comment): hargoniX calls it a "well known limitation" and recommends a separate Statement.lean.

Tone to match: Technical, matter-of-fact. The existing commenters (eric-wieser, tadamcz) share real project experiences with concrete details. Our comment follows that pattern.

What we want the reviewer to check

1. Is the comment factually correct given the corrections above?
2. Does it accurately describe what upstream does vs what our workarounds do?
3. Is the tone appropriate — a field report adding evidence, not claiming a fix?
4. Is the ask calibrated — minimal reproducer OR narrowly scoped PR, not both?
5. Should we mention the exact rejection message, or is pointing to the repo sufficient?

gist-context.md

Context for reviewer

What this is

A proposed GitHub issue for leanprover/comparator — the structural equality checker used by the Palomar platform to verify Lean 4 formalization submissions.

We're asking a reviewer to check the issue draft (in the companion file proposed-issue.md) before we file it. The previous version was filed and immediately closed because it misidentified the problem — see "What we got wrong" below.

What we're trying to accomplish

Build goodwill with the comparator maintainers (hargoniX / Henrik Böving, nomeata / Joachim Breitner) by sharing a real-world field report. We want to:

1. Show that we're a serious user who built a real formalization and hit a real limitation
2. Share what we learned — including a security pitfall — so others benefit
3. Open the door for future contributions (patches, PRs) once they signal interest

Our project

lean-clark-ocone: a 58-file, 0-sorry Lean 4 formalization of the Clark-Ocone representation theorem (stochastic analysis / Malliavin calculus). 19 target theorems, capstone: naturalClarkOcone_condExp_of_generated.

We tried to submit it via Palomar and the upstream comparator rejected several theorems due to elaboration divergence — same mathematics, different internal representation across import graphs.

What we built to fix it

We patched our local copy of the comparator (comparator-tool) with three layers:

1. Delta-reduction (constantInfoDeltaEq, constantValDeltaEq) — unfold definitions before comparing, so expectationL2's body, which elaborates differently across import graphs, matches after unfolding
2. Universe-alpha-equivalence — positional universe-param matching instead of name-based, so u.1 vs u.2 doesn't cause false rejections
3. Proof irrelevance — two theorem constants with the same type are equal regardless of proof term, so auto-generated _proof_N constants with divergent elaboration paths match

These got lean-clark-ocone from 10/19 to 19/19.

What we got wrong (first attempt)

We filed issue #85 and draft PR #86 claiming that upstream's Compare.loop accepted value substitutions on non-sorry'd definitions. This was wrong.

The vulnerability existed in our local patches, not in upstream. Upstream 8d84e67 already rejects any challengeConst != solutionConst — it has no type-only fallback. Our patches added the fallback, our adversarial testing found it was too permissive, we fixed it with a sorryAx guard, and then we incorrectly filed the fix against upstream as if the bug were theirs.

An independent review caught this before the maintainers saw it. We closed both within minutes with apologies. The closing comments are visible on the issue and PR.

What we got wrong (test case)

The comparator-proof-bypass example repo also has a factual error: test-2-value-cheat uses secret := 42 with secret % 2 = 0, but 42 is even — the statement is true, not false. The test case doesn't demonstrate a false statement being proved. This needs correction (e.g., use secret := 41 where 41 % 2 = 0 is false).

What the issue should actually say

The reframing: this is a field report / feature request, not a bug report. The comparator works as designed — it just can't handle real submissions with elaboration divergence. Our experience is valuable because:

1. lean-clark-ocone is evidence that the problem occurs in practice
2. Our patches show one approach to solving it
3. The security pitfall we hit (type-only fallback accepting value substitutions) is a trap anyone extending the comparator should know about

Upstream repo conventions

From reviewing issues and PRs:

• Successful issues (#64, #68): title is the bug statement, body has a minimal reproducer with all files, observed vs expected, root cause pointing to exact code, suggested fix
• Feature requests (#79, #33): shorter, more discussion-oriented
• PRs: minimal, conventional-commit style (fix:, chore:, feat:), body is often just Fixes: #N
• Maintainers: hargoniX (member, does the code), nomeata (contributor, reviews and security triage)
• Related open issue: #59 (proof irrelevance not respected in statements) — hargoniX's response: "well known limitation, recommend a separate Statement.lean"
• Tone: technical, matter-of-fact. No framing around "we found a vulnerability" — just facts

What we want the reviewer to check

1. Is the proposed issue factually correct? (We got this wrong once already.)
2. Does it accurately describe what upstream does vs what our patches do?
3. Is the tone appropriate — sharing a field report, not claiming a bug?
4. Does the structure follow the repo's conventions?
5. Would the corrected comparator-proof-bypass repo be useful to link, or is it better to leave it out?
6. Should we reference the closed #85/#86 for transparency, or leave them unmentioned?

proposed-comment-58.md

Proposed comment on leanprover/comparator #58

Post as a comment on: leanprover/comparator#58

---

Comment:

Field report from a multi-file submission hitting this.

We maintain lean-clark-ocone — a 58-file Lean 4 formalization of the Clark-Ocone representation theorem (stochastic analysis). The underlying Malliavin library and Solution are zero-sorry; the Palomar Challenge intentionally contains sorries. Running the upstream comparator at 8d84e67 against the current repo rejects Malliavin.naturalClarkOcone_of_generated (our capstone) and several others.

Two categories of divergence:

1. Auto-generated _proof_N constants. The elaborator picks different _proof_1 constants for the same proposition (Nat.AtLeastTwo (0+2+0)) depending on which files are imported. One investigated pair had identical types and values under different names. A later _proof_8 failure involved differing types — so these are not all the same mechanism.

2. Definition bodies that elaborate differently across import graphs. Malliavin.expectationL2 has a concrete body in both Challenge and Solution, but the body elaborates differently because the import graphs diverge. The types match; the values are kernel-equivalent but structurally distinct. We currently work around this by listing it in definition_names (commit), which stops checking its body — but this stretches the definition-hole contract, which expects holes to be sorried and requires additional verification.

The shared Statement.lean workaround from #59 addresses cases where the submitter controls the diverging term. For our submission, the divergence is in auto-generated constants and definition bodies produced by the elaborator — a shared statement file would require a substantial refactor of the import graph, and we have not yet tested whether it would resolve the _proof_N divergences specifically.

The progression was 6/19 → 10/19 → 14/19 → 19/19, with significant Challenge source alignment alongside local comparator patches. Our comparator patches (delta-reduction, positional universe-param matching, proof irrelevance) addressed the remaining structural mismatches, but they are broader than what's needed for this issue alone and need redesign before they'd be suitable for upstreaming.

Would it be useful if we prepared a minimal reproducer isolating the _proof_N case? Or would you prefer a narrowly scoped PR addressing just one of these divergence categories?

Related: #59

proposed-issue.md

Proposed issue for leanprover/comparator

Title: Elaboration divergence causes false rejections on structurally correct submissions

---

Body:

We hit a limitation while preparing lean-clark-ocone — a 58-file, 0-sorry formalization of the Clark-Ocone representation theorem — for Palomar submission. Several of our 19 target theorems are rejected because constants that are mathematically identical elaborate differently across import graphs.

What diverges

Two categories of constants cause false rejections:

1. Auto-generated _proof_N constants. The elaborator picks different _proof_1 constants for the same proposition (Nat.AtLeastTwo (0+2+0)) depending on which files are imported. Both are theorems with identical types — only the proof term differs. This affects 5 of our 19 theorems (the Clark-Ocone family).

2. Non-sorry'd definitions with different elaboration. Malliavin.expectationL2 has a concrete body in both Challenge and Solution, but the body elaborates differently because the import graphs diverge. The types match; the values are mathematically equal but structurally distinct.

Why Statement.lean doesn't help

The recommended workaround from #59 (import statements from a shared file) addresses cases where the submitter controls the diverging term. In our case, the divergence is in auto-generated constants and definition bodies that the submitter cannot control — the elaborator makes different choices depending on the import graph.

What we tried

We patched a local copy of the comparator with three changes:

1. Delta-reduction — unfold definitions before comparing, so bodies that elaborate differently can match after unfolding
2. Positional universe-param matching — compare universe parameters by position instead of name, avoiding u.1 vs u.2 mismatches
3. Proof irrelevance — treat two theorem constants with the same type as equal regardless of proof term (directly addresses #59)

These got lean-clark-ocone from 10/19 to 19/19 with the patched comparator.

Security pitfall we discovered

When we first added a type-only fallback for mismatched values, it was too permissive — a submitter could redefine a non-sorry'd definition's body while preserving its type, effectively proving a different statement than the challenge intended. We caught this through adversarial testing and fixed it by conditioning the fallback on whether the challenge-side value references sorryAx: only sorry'd definitions get the type-only path.

We mention this because anyone extending the comparator's tolerance will hit the same trap. The sorryAx guard is the fix.

What we're asking

Not a PR yet — we wanted to share the experience first. The patches change the comparator's trust model (especially delta-reduction), so we'd welcome your perspective on the right approach before proposing code. Our local patches are available if useful.

Related: #59