Repair + gate the Isabelle GroupTheory and Mizar self-proof corpora #280

Tracking the two self-proof corpora that the weekly verification-proofs-cron does not
yet gate, because they have genuine (not config) verification errors. They need dedicated,
locally-tested repair — both toolchains' download hosts (isabelle.in.tum.de,
mizar.org) are 403-blocked from the dev sandbox, so they can only be iterated on CI,
which is too slow/uncertain for proof repair. Context: the proof-CI sweep (#234, #275, #276,
#277, #278, #279) gated Coq, Lean 4, Agda, Idris2, and the Isabelle base (Basic,
EchidnaList, EchidnaNat, Propositional). These two are the remainder.

1. proofs/isabelle/algebra/GroupTheory.thy (excluded from proofs/isabelle/ROOT)

"ML training corpus" material that was never checked. On Isabelle2025-2 it has genuine bugs:

• mul_right_inv, mul_right_id: omit assumes "group G" but use assms → "Undefined fact: assms".
• center_closed: proved with group.m_comm, which holds only for comm_group, not a bare group.
• Dubious notation / lemma names: (⊕ₘ) for power, Prod.mult_def/Prod.inv_def/Prod.one_def, power_add/power_0/power_1.
• Uses the deprecated path import ~~/src/HOL/Algebra/Group (already changed to HOL-Algebra.Group).

Needs each lemma's statement + proof checked against HOL-Algebra. Once green, re-add an
Echidna_Isabelle_Algebra session (parent HOL-Algebra) to proofs/isabelle/ROOT and a
just proofs-isabelle target.

2. proofs/mizar/*.miz

Mizar is the project's mock-only Tier-4 tail. The cron's Mizar install fully works
(resolves + downloads mizar-8.1.15 from mizar.uwb.edu.pl, binaries on PATH via
MIZFILES), but the .miz files have genuine, heterogeneous errors:

• propositional.miz: 24 errors — every thus A c= B; thus B c= A set-equality
  double-inclusion step (code 51) and let x be object (code 55). Likely a missing
  definitions environ item, but unconfirmed.
• basic.miz: a makeenv error in the Notations phase.
• numbers.miz, mvp_basic.miz: not yet diagnosed (mvp_basic is trivial, likely fine).

The just proofs-mizar recipe (makeenv + verifier, failing on a non-empty .err) remains
for local use. Once the files verify, re-add the mizar job + proofs/mizar/** trigger to
.github/workflows/verification-proofs-cron.yml.

Suggested approach

Repair in an environment where Isabelle2025-2 and the Mizar system are installable and
runnable locally (the sandbox here cannot reach either host), then re-gate via the weekly cron.