[heathsanchez]

MathGraph Check for Open Math Model — bounded claim assurance (draft)

This PR extends the existing registered MathGraph Check App additively. The original L4YAML /pilot page, examples, Worker and live Check routes are unchanged; the entire changed-file list contains only new omm-v1 content and five OMM-specific Actions workflows. No OMM community installation, outbound post, general source execution or automatic repair is enabled.

A concrete claim-versus-proof experiment

The source-pinned, published Artin exercise has two frozen first-party control PRs:

Owned PR	Lean candidate	Original [Group] target consumer
#239 strengthens the premise to [CommGroup]	Compiles	NOT_ESTABLISHED_IN_THIS_REPLAY
#240 restores the original premise	Compiles	CONSUMER_ACCEPTED

Lean 4.28.0 and Mathlib 8f9d9cff6bd728b17a24e163c9402775d9e6a365 ran these exact native controls in a separate no-secret job. The existing registered-App run #41916425178 passed 6/6 jobs, re-derived the immutable evidence manifest, and updated the same #239 Check 126876654761 and #240 Check 126876680794. Independent GitHub readback confirmed App ID 5308912, neutral conclusions and exact source heads. A further exact-head full rerun #41922969572 passed all six jobs; a fresh public API read returned exactly one same-ID OMM App Check on each frozen PR head.

Consumer compilation is not a theorem about the paper's meaning; consumer rejection is not a general inequivalence proof. Human mathematical intent, formal statement equivalence, candidate necessity and independent semantic warrant remain UNKNOWN.

Actual App source-withdrawal qualification

A separate first-party intake Check carries UNKNOWN on every proof dimension. It tests transport and source freshness only, with no Lean execution.

• Run #41920410063 created genuine neutral Check 126891175327 at owned PR270 head 6a236fa8....

• Run #41920899155 explicitly SUPERSEDED that same Check, naming new head ac7ab4df..., and created new Check 126892881018.

• Run #41922158367 repeated the transition: old Check 126892881018 became SUPERSEDED, and current neutral Check 126897218711 was created at 803fdf3a34b4338c8be803b136214b370bebf9f1.

• Run #41922969172 then superseded Check 126897218711 and created current neutral Check 126900063252 at exact head c502c629b67d2aa91d12e2a4a806af36510cc808.

These are independent GitHub API readbacks of real App-owned Checks, not simulated HTML. The gate is WARRANTED_BOUNDED to this controlled immediately preceding owned PR head, not general historical revocation.

Operator opt-in admission and native isolation

• @MathGraph -claim now has an independently qualified, first-party, owned-comment-to-native-to-App replay, initiated by a push-triggered workflow that fetches and reauthenticates one actual owner-written comment. The admission parser alone still yields at most SOURCE_ADMITTED_ONLY; a separate no-App-secret Lean job produces a native receipt, and an App-only job requalifies the same-run receipt before publishing a neutral result. This is not a default-branch issue_comment listener or general community intake.
• Native sandbox run #41922969262 passed first-party positive and negative Lean 4.28.0 fixtures plus an actual container isolation probe. The image gets one read-only source file, no network/default route, UID 65534, read-only root filesystem, no privileges, limited CPU/memory/PIDs, bounded output/time, and no App/model credentials. Artifact 13367129475 preserves the observation and image identity; GitHub reports ZIP SHA-256 276aac4ee0e54cd52198e5075809b63d612ee227dfa77d9fb8e8844146d1ecbd. The hardening revision also uses uniquely named containers and forces exact-container cleanup after each invocation, returning UNKNOWN if cleanup cannot be confirmed (timeout cleanup was unit-tested, not live-stress-tested). This is WARRANTED_BOUNDED owned-fixture smoke, not a secure community Lean runner: the container base image is not yet digest-pinned, and arbitrary malicious Lean has not been admitted or independently adversarially qualified.

The latest additive CI run #41922969457 passed 49/49 new OMM tests, plus 485 passing existing Check tests, 11 declared skips, zero failures across 496 discovered tests, including byte-for-byte protection of the L4YAML pilot runtime and page. PR CI also passed.

Explicit release boundary

This draft is not general @MathGraph -check for the Open Math Model community. Before enabling community intake: digest-pin and adversarially qualify the sandbox and its artifact publisher; authenticate claim ownership and intended statement; establish permissions/cost limits and exhaustive stale-result withdrawal; connect a trusted default-branch opt-in listener; and independently requalify the complete user-facing flow on owned PRs. No semantic gold oracle is currently admitted.

Real owner comment → Lean receipt → registered-App Check (5 November 2026)

On our own Artin PR #239, Heath posted one actual opt-in comment @MathGraph -claim. The new workflow fetches that GitHub comment afresh and independently checks the author, PR, source SHA and frozen candidate; no synthetic comment event or external installation is used.

• Initial run #41938543754 passed comment admission and credentialless Lean replay, but App publication failed: its HTTP helper inadvertently issued GET rather than POST to the check-runs endpoint. This failure remains part of the qualification history.
• After the transport fix at exact head 3230827ad472afc121772a8ae3ac778bc41ee879, run #41939111450 passed all three jobs. The Lean source compiled; the original [Group] consumer was NOT_ESTABLISHED_IN_THIS_REPLAY. Semantic equivalence and mathematical intent remain UNKNOWN.
• Independent GitHub GET confirms real neutral Check #126956089184 for source SHA 2f6aaba0d71f1c0b4c0db58618a8981ccd59dc17, registered App ID 5308912, bound to that owner comment and the same-run native receipt SHA-256 889a21eaab13a54f0063f198a4f97c3461ecabb89b294b0e0275ba554c6cf352. The App offers no mathematical warrant or repair authorization.
• Current additive CI #41939111290 passed 64/64 OMM controls, plus existing Check 485 passed / 11 expressly skipped / zero failures across 496 discovered; protected pr-pilot-v1 diff is empty.

This closes the first-party end-to-end transport experiment, not the community-release gate. The default-branch listener, authenticated community claim-owner policy, pinned/adversarially qualified sandbox, semantics/intent review and broader stale-Check revocation all remain open. This PR is deliberately draft, with no live L4YAML pilot edits, deployment or outside-community interaction.

Real retry/idempotence qualification: Re-running the completed publisher job produced run #41939111450 attempt 2. The publisher returned mode:UNCHANGED, Check ID 126956089184; independent public GitHub GET still returned exactly one matching completed, neutral registered-App Check. The new App readback artifact 13376220809 has ZIP SHA-256 a9710c7058ac7536cdb2b7f1124fb989a4a3ec6f6016b5cd0f19bddb2ba700e8. This is WARRANTED_BOUNDED for repeat publication of the same first-party request and frozen source; it is not community intake, source deletion withdrawal or general stale-check revocation. Documentation-only head 90348a51bbbf7b1409a866f3f3feb86a481d07f1 preserves the result in the README. Follow-up CI/lifecycle qualification is running; no merge/deployment is authorized.

Final current-head reconciliation (5 November 2026)

At documentation-only head 90348a51bbbf7b1409a866f3f3feb86a481d07f1, additive push CI #41940237694 and PR CI #41940243964 both passed: 64/64 OMM tests, existing Check 485 pass / 11 declared skip / 0 fail, and clean L4YAML pilot diff.

Lifecycle #41940237691 independently withdrew predecessor Check 126955095476 at 3230827... and published current neutral Check 126959000468. Independent GitHub GET confirms both bodies and App ID 5308912. A read-only census of all 12 commits in PR270 found exactly seven OMM intake Checks: six superseded in the linear sequence and exactly one current. This closes observed historical applicability on this owned branch, not all future/check-deletion events.

The six-job native Artin/App run #41940237648 passed. Live GitHub readback shows exactly one registered-App claim Check per frozen PR239 and PR240 source SHA, respectively the original 126876654761 and 126876680794, both updated (not duplicated), completed neutral, and run-bound. These remain separate from the real owner-comment Check 126956089184.

Release boundary unchanged: no automatic OMM community comment listener, externally admitted mathematical intention, arbitrary untrusted Lean execution, external installation, repair authorization, pilot alteration or production deployment.

Canonical OMM slash commands — staged and qualified (5 November 2026)

The OMM claim-admission interface now recognizes the exact @MathGraph /check as its canonical form and retains @MathGraph -claim as the legacy alias. Both enforce identical authenticated source/owner conditions, issue only SOURCE_ADMITTED_ONLY, and leave mathematical intent, independent warrant and repair permission UNKNOWN/DENIED. The existing @MathGraph -check / -fix generic default-branch demo is unchanged and deliberately not double-routed to OMM. OMM /explain and /fix remain reserved and unavailable, with strict refusal of trailing instructions or malformed spellings.

At exact draft head 9a202e30c25451b5d5bffc792b664732c09023a8, additive CI #41942715465 and PR CI #41942721138 passed: 67/67 OMM tests, 485 baseline Check tests passed / 11 explicitly skipped / zero failed and clean L4YAML pilot diff. The new slash-admission tests demonstrably failed before the shared command predicate was added, passed afterwards, and failed again under a deliberate no-slash mutation.

The unchanged historical -claim owned-comment run #41942715363 passed all three jobs; independent GitHub GET confirms exactly one registered-App neutral owner-opt-in Check #126956089184, with App ID 5308912 and the current run evidence. Fixed Artin run #41942715322 passed all six jobs, updating the same original neutral App IDs for #239 and #240. Lifecycle run #41942715320 withdrew prior Check 126959000468 and published current neutral Check 126967314218; GitHub readback confirms both.

Prior-checkpoint scope (superseded by the live run below): This qualifies the exact first-party parser and historical alias transport; no authentic /check comment has yet triggered an OMM run. There is still no OMM default-branch slash listener, outside install, general Lean executor, claim-intent certificate, semantic equality warrant, authorized fix, production deployment or modification to the L4YAML /pilot page and examples. PR remains draft.

Live first-party slash event — qualified

WARRANTED_BOUNDED for exactly one owner-authored, frozen PR239 /check request (not a community release): the separately scoped single-file listener PR #271 merged into default main at d2797794debcbd89b32d16260926770d4b3f2990, pinning implementation SHA 079f0a6c7802f2a4482c9e3778e801a6880c86dd from this still-draft, unmerged PR.

• Real exact command: owner comment 6647212168 by heathsanchez / GitHub ID 32909488.
• Issue-comment workflow #41949744744: 3/3 jobs passed, independently authenticating unchanged comment and source, executing frozen Lean 4.28.0/Mathlib in a credentialless job, then requalifying the receipt in a separately scoped App publisher. Three source/native/App artifacts saved. Original generic -check/-fix workflow skipped this event.
• Registered MathGraph App Check #126991454434: CREATED, App ID 5308912, exact frozen PR239 head 2f6aaba0d71f1c0b4c0db58618a8981ccd59dc17, completed/neutral; independent GitHub source-commit Check-list readback confirmed name, owner, source and summary. candidate_proof=LEAN_COMPILED, original_target=NOT_ESTABLISHED_IN_THIS_REPLAY, intent_fidelity=UNKNOWN, repair=DENIED.
• The earlier historical -claim Check #126956089184 remains separate and neutral, with its original external ID and no duplicate. Local 72/72 OMM + workflow tests passed; exact branch CI #41949476342 passed.

Still out of scope: no community intake, arbitrary Lean execution, general mathematical-intent warrant, automatic repair, /fix or /explain. The full OMM feature branch remains draft/unmerged. The L4YAML Worker, public /pilot page/examples and legacy Check routes were not changed.

[vercel]

The latest updates on your projects. Learn more about Vercel for GitHub.

Project	Deployment	Actions	Updated
mathgraph	Ready	Preview	Nov 8, 2026 7:29am UTC