# MAIS submitted solutions, and what checking them found Solutions other people filed against the [MAIS](https://github.com/lionellevine/MAIS) open-problems agenda, which this repository transcribed and checked. **9** are recorded: **5** `CHECKED`, **2** `PARTIAL`, **1** `CONDITIONAL`, **1** `STATED_ONLY`. This is other people's mathematics. Checking it is not co-authorship, and a verdict here is a machine check against a pinned artifact -- never peer review, and never a statement that a submission is accepted upstream. Issue bodies are editable in place, so every row rests on a recorded body hash and an edit invalidates it. ## Reading the columns **Verdict** is whether the mathematics checks: - `CHECKED` — the submission's own claim is transcribed and proved outright - `PARTIAL` — some of it is proved and some is not, or what is proved is narrower than what is claimed - `CONDITIONAL` — proved, but under propositions the submission cites rather than derives - `STATED_ONLY` — transcribed at the submission's own quantifiers and not proved **Grade answers to** is a different question: which artifact the ledger row *transcribes*. A row names one graded source, because one fidelity grade cannot answer to two artifacts of different genre at once. A row graded against the submission is a verdict on its own wording; a row graded against the printed problem is a verdict on print that cites the submission for a witness or an argument. **The two columns are independent** — issue #30 is graded against the agenda and its submitted claim is proved anyway. | Issue | Problem | Filed by | Verdict | Grade answers to | Rows | |---|---|---|---|---|---| | [#3](https://github.com/lionellevine/MAIS/issues/3) | MAIS-O70 | Sneiderman | `CONDITIONAL` | the printed problem | `CONJ-026`, `CONJ-028` | | [#4](https://github.com/lionellevine/MAIS/issues/4) | MAIS-O34(a) | Robby955 | `CHECKED` | the submission | `CONJ-009` | | [#5](https://github.com/lionellevine/MAIS/issues/5) | MAIS-O7 | — | `CHECKED` | the submission | `CONJ-027` | | [#6](https://github.com/lionellevine/MAIS/issues/6) | MAIS-O23 | — | `PARTIAL` | an artifact row, not a graded claim | `LAND-CAUSAL-COLLISION-001` | | [#7](https://github.com/lionellevine/MAIS/issues/7) | MAIS-O24 | kumino | `CHECKED` | the printed problem | `CONJ-012` | | [#8](https://github.com/lionellevine/MAIS/issues/8) | MAIS-O31 | kumino | `STATED_ONLY` | the submission | `CONJ-010` | | [#9](https://github.com/lionellevine/MAIS/issues/9) | MAIS-O33 | kumino | `CHECKED` | the printed problem | `CONJ-023` | | [#12](https://github.com/lionellevine/MAIS/issues/12) | MAIS-O77 | — | `PARTIAL` | the printed problem | `CONJ-028` | | [#30](https://github.com/lionellevine/MAIS/issues/30) | MAIS-O38 | 26david26 | `CHECKED` | the printed problem | `CONJ-025` | ## MAIS issue #3 — MAIS-O70 - **Locator:** - **Verdict:** `CONDITIONAL` - **The submission, transcribed:** `AISafetyAtlas.Conjectures.MAIS.o70Pair` - **Body sha256:** `405c8cb324884607f3e827cdd915d8ac10ce01b969a7739616474b3fb8401cbe` **Submitted.** A complete solution: the local learning coefficients of reduced-rank regression at every rank stratum, with the residual threshold restated as a discrete minimisation over an integer index. **Checked.** The rank table is transcribed as o70Pair and machine-checked, but under two propositions the candidate cites rather than derives: the real-Wishart eigenvalue law and the existence of exact local pairs. Both are recorded as frontiers with their own evidence, and NC-011 shows that none of the six baseline formalization corpora supplies the first. The discrete minimisation behind Corollary 1.3 is closed unconditionally, as residualMinCost_eq_argmin. The candidate's own section 13 states that exactness at every radius is not claimed, and the atlas matches that co-countable form rather than strengthening it. ## MAIS issue #4 — MAIS-O34(a) - **Locator:** - **Verdict:** `CHECKED` - **The submission, transcribed:** `AISafetyAtlas.Conjectures.MAIS.maisO34_exactFiberCandidate` - **Body sha256:** `f425da83395b457feb5615c9beed703675a977967890ebe1b97dd61efdd0b328` **Submitted.** A complete criterion for when the global behavioural fibre is a singleton, on the source's real three-parameter two-variable chart, together with a first-order radius constant, a singular classification, and a graph-threshold program. **Checked.** The criterion is transcribed at the source's own quantifiers and proved, as maisO34_exactFiberCandidate_holds. Separately the atlas settles the margin-sufficiency subquestion negatively: positive margin alone does not force a singleton fibre. The rest of part (b) — the radius constant, the singular classification, the graph-threshold program — is not transcribed and carries no verdict here. ## MAIS issue #5 — MAIS-O7 - **Locator:** - **Verdict:** `CHECKED` - **The submission, transcribed:** `AISafetyAtlas.Conjectures.MAIS.O7CounterexampleAtEveryScale` - **Body sha256:** `edbaf2f2435c8854ce681a19cc2f5da10474e944fc2c9254624f0db50b5061fa` **Submitted.** A negative resolution: in the scalar instance the rank-zero critical set has local pair (1,1) while the terminal fibre has (1/2,1), reversing the conjectured strict increase. **Checked.** Confirmed and strengthened, though not in quantifier strength: the note already proves the pair at every point of the terminal rung and states that both infima are attained. o7CounterexampleAtEveryScale makes the two-rung certificate a single unconditional object -- the exact exponent set on each rung, attainment as a proposition, and every positive target. The conjectured increase is false. What was checked is the note's claim, not its argument: the note routes the rank-zero pair through the analytic Morse lemma at signature (2,2) and the atlas proves it by an explicit integral instead, so the note's own step is unverified. A 2026-09-06 audit added the two identifications the certificate rests on -- that its rank-zero rung is MAIS-A7's C_0 and its terminal rung that frame's exact-factorization fibre -- which had been transcriptions no check could see, and the descending-loss step that puts the instance inside print's stated setting. ## MAIS issue #6 — MAIS-O23 - **Locator:** - **Verdict:** `PARTIAL` - **The submission, transcribed:** `AISafetyAtlas.Examples.Causal.margin_class_not_identifiable` - **Body sha256:** `4fd639c4322a3a3bd1b27fe6f14ee3de902961e0013485395e461d7cdc739a9b` **Submitted.** Filed as a full solution pending review: three models on two binary variables sharing a behavioural transform, making the MAIS-O23 consequence explicit across all three graphs. **Checked.** The construction machine-checks, and the atlas goes past it: a positive-dimensional colliding family rather than a point, a narrower two-graph reading that does not depend on the edgeless model being admissible, and transport to the source's real chart rather than a rational restriction. What is verified is narrower than what is claimed. A collision at one skeleton is a possibility result, not the general question, so the atlas does not endorse the full-solution framing; the printed question is answered separately and graded against the agenda. The issue credits its own construction to MAIS issue #4, and the atlas claims no priority for it. ## MAIS issue #7 — MAIS-O24 - **Locator:** - **Verdict:** `CHECKED` - **The submission, transcribed:** `AISafetyAtlas.Examples.Causal.O24Refutation.not_o24_identifies_and_excluded` - **Body sha256:** `68e65b119a8923dd997e2ea75daea5331145706674a44ecc6d3f7c7b89a80ee7` **Submitted.** A negative resolution: clauses (a) and (c) of the printed problem cannot both hold, so it has no solution. **Checked.** The incompatibility holds and is machine-checked. The argument as written had a circular step in its choice of measure, which the atlas repaired before checking rather than reproducing. AISafetyAtlas.Causal.O24Solution is the solution type with the proof obligations as fields, and it is empty. ## MAIS issue #8 — MAIS-O31 - **Locator:** - **Verdict:** `STATED_ONLY` - **The submission, transcribed:** `AISafetyAtlas.Conjectures.MAIS.maisO31_chainClassificationCandidate` - **Body sha256:** `8e2e688eaac1a72f915aa787ad1e74676e6b72eff4f2796394e95b0a83fb8a96` **Submitted.** A complete solution: four affine diagnostics and a generic chamber classification for one intervention in a binary chain. **Checked.** Transcribed at the issue's own quantifiers — every threshold in the open unit interval, all four binary local interventions, literal coordinate equality, and the issue's own scope exclusions as the chamber disjunct — and it is not proved. The embedding into the printed margin class is proved in both directions, so the statement is not left semantically detached. The atlas separately refutes the printed heuristic's claim that the endpoint marginal is recoverable, on an explicit box of Lebesgue measure 1/500. ## MAIS issue #9 — MAIS-O33 - **Locator:** - **Verdict:** `CHECKED` - **The submission, transcribed:** `AISafetyAtlas.Conjectures.MAIS.maisO33_etaStarIsZero` - **Body sha256:** `9ff124f8cd8fb65d7393780384776f87a42a5870ce477b50da8dd9c315e9bd25` **Submitted.** A negative resolution: the persistent-corruption threshold is zero. **Checked.** The submitted value is confirmed, with a caveat the ledger states rather than hides. The upper half is the proved content; the lower half follows from the sign clause together with the supremum of the empty set being zero, not from a proof that the printed zero endpoint is tolerable, and the graded correct answer is the baseline-relative form. An independent audit of the note found no error. The issue reports that its mathematics was generated by an AI system with no human referee review claimed. ## MAIS issue #12 — MAIS-O77 - **Locator:** - **Verdict:** `PARTIAL` - **The submission, transcribed:** `AISafetyAtlas.Conjectures.MAIS.O77AllSaddlesHavePairOne` - **Body sha256:** `c0a2c0a8cb66858ca0160765b1465fb1f55bdd9be47edf79283d43e82af6c984` **Submitted.** A complete solution to both clauses: the local pair at every exact factorization together with the minimal stratum, and the pair at every point of every nonterminal critical set. **Checked.** Part (b) is proved unconditionally at print's own quantifiers, as o77AllSaddlesHavePairOne_holds, following the candidate's five printed steps rather than substituting a shortcut; two results it needs — the splitting of its equation (9) and its Lemma 2 — are absent from the Mathlib revision pinned here and were built here; NC-012 is that search, and it covers Mathlib alone, so it is not a claim about every formalization corpus. Part (a) is verified only under the eigenvalue-law frontier inherited from MAIS issue #3; that covers its minimal stratum too, checked at the germs rather than against the table. Four defects surfaced while checking, all of them the atlas's own -- each a statement that compiled, was axiom-clean, and was about something weaker than print. None was a defect in the submission; no error was found in it. The complete-solution claim is therefore not verified. The note's argument is followed, not replaced. Its equation (9) already writes the generalized splitting -- L - L(w) = Q_alpha(xi) + g(zeta) with g(0) = 0 and no nondegeneracy asked of g -- which is a Gromoll-Meyer splitting, and that is what was built. Only the name it gives the tool, the analytic Morse splitting lemma, is loose. Two departures are worth stating: the atlas proves the splitting C-infinity rather than analytic, which is all the note's Lemma 2 consumes, and loss_quartic_on_degenerateNull rules out a Morse-Bott normal form, which (9) does not claim and does not need. A 2026-09-06 audit closed the remaining prose step in part (a) by proving that the discrete minimisation the atlas computes with is the note's printed four-case closed formula, and pinned the note's own ten check-table values. ## MAIS issue #30 — MAIS-O38 - **Locator:** - **Verdict:** `CHECKED` - **The submission, transcribed:** `AISafetyAtlas.Conjectures.MAIS.o38PolynomialSampleCandidate` - **Body sha256:** `6e2db10eb10242c075ca331fcf87a604511b9b31df3d55a5c4b0d2d2d95d05ab` **Submitted.** A complete solution in two theorems: that a polynomial number of fixed codes depending only on the dimension and the sparsity suffice below the sparsity bound, and a boundary theorem above it. **Checked.** The main claim is transcribed and proved, and resolves the graded row at every non-degenerate dimension; its codes being independent of the ambient dimension is one axis on which it is stronger than the claim being graded. The boundary theorem is proved here independently and without one of its hypotheses. The atlas has posted this machine-check on the issue itself. The issue reports that its mathematics was produced and checked entirely by AI systems with no human verification.