# Source report — MAIS open problems An index over the MAIS agenda **works** — the agenda files and problem pages whose statements the atlas transcribes — generated from [`conjectures.yaml`](../../../conjectures.yaml) and keyed by printed problem, because a row's problem number is what crosses agendas. **This is not a coverage report against MAIS.** The master list at [MAIS](https://github.com/lionellevine/MAIS) is catalogued as a *directory* — a curated map of numbered questions, which states nothing of its own — so nothing is graded against it and **its problem count is never a denominator here**. The `Graded against` column names the work each row actually answers to, which is the only kind of source a statement-match grade may cite; `validate_conjectures.py` rejects a graded row that cites only directories. An open problem is a question, not an asserted theorem, so a MAIS row is a conjecture-ledger row rather than a registry claim. **A row here is never headline coverage**, and `RESOLVED` means the atlas settled the printed question it transcribes — sometimes negatively, by refuting it. A problem the atlas cannot state carries no row at all and is recorded against its source instead, so absence from this table is not a gap in it. Submitted solutions and what checking them found are a separate page: [MAIS submitted solutions](../mais-solutions.md). | Problem | Agenda | Row | Kind | Status | Graded against | Scope / fidelity | Graded declarations | Submitted | |---|---|---|---|---|---|---|---|---| | MAIS-O7 | A7 | `CONJ-027` | answer | `RESOLVED` | `mais-issue-5-2026` | Same/Literal | `AISafetyAtlas.Conjectures.MAIS.IsO7Counterexample`
`AISafetyAtlas.Conjectures.MAIS.O7CounterexampleAtEveryScale` | [`CHECKED`](https://github.com/lionellevine/MAIS/issues/5) | | MAIS-O23 | A2 | `CONJ-004` | claim | `RESOLVED` | `mais-a2-2026` | Same/Selected | `AISafetyAtlas.Conjectures.MAIS.maisO23_marginsDoNotSuffice` | [`PARTIAL`](https://github.com/lionellevine/MAIS/issues/6) | | MAIS-O24 | A2 | `CONJ-012` | target | `RESOLVED` | `mais-a2-2026` | Same/DetermineProblem | `AISafetyAtlas.Causal.O24Solution` | [`CHECKED`](https://github.com/lionellevine/MAIS/issues/7) | | MAIS-O25 | A2 | `CONJ-006` | claim | `OPEN` | `mais-a2-2026` | Same/Selected | `AISafetyAtlas.Conjectures.MAIS.maisO25_exactQueryRate` | — | | MAIS-O26 | A2 | `CONJ-003` | claim | `RESOLVED` | `mais-a2-2026` | Same/Literal | `AISafetyAtlas.Conjectures.MAIS.maisO26_exactRate` | — | | MAIS-O27 | A2 | `CONJ-013` | target | `OPEN` | `mais-a2-2026` | Same/DetermineProblem | `AISafetyAtlas.Conjectures.MAIS.IsO27EdgeSurvivalRegion`
`AISafetyAtlas.Conjectures.MAIS.IsO27FirstOrderConstantFunction`
`AISafetyAtlas.Conjectures.MAIS.IsO27RadiusVanishingCriterion` | — | | MAIS-O29(a) | A2 | `CONJ-008` | claim | `RESOLVED` | `mais-a2-2026` | Same/Selected | `AISafetyAtlas.Conjectures.MAIS.maisO29_boltzmannNotInjective` | — | | MAIS-O29(b) | A2 | `CONJ-016` | target | `OPEN` | `mais-a2-2026` | Same/DetermineProblem | `AISafetyAtlas.Conjectures.MAIS.IsBoltzmannRiskRate`
`AISafetyAtlas.Conjectures.MAIS.boltzmannMinimaxRisk` | — | | MAIS-O31 | A2 | `CONJ-010` | answer | `OPEN` | `mais-issue-8-2026` | Same/Literal | `AISafetyAtlas.Conjectures.MAIS.maisO31_chainClassificationCandidate` | [`STATED_ONLY`](https://github.com/lionellevine/MAIS/issues/8) | | MAIS-O31 | A2 | `CONJ-017` | target | `OPEN` | `mais-a2-2026` | Same/DetermineProblem | `AISafetyAtlas.Conjectures.MAIS.IsO31IdentifiableSetAlmostEverywhere` | [`STATED_ONLY`](https://github.com/lionellevine/MAIS/issues/8) | | MAIS-O33 | A2 | `CONJ-023` | answer | `RESOLVED` | `mais-a2-2026` | Same/DetermineProblem + Selected | `AISafetyAtlas.Conjectures.MAIS.maisO33_etaStarIsZero`
`AISafetyAtlas.Conjectures.MAIS.maisO33_etaStarIsZeroGivenBaseline` | [`CHECKED`](https://github.com/lionellevine/MAIS/issues/9) | | MAIS-O34(a) | A2 | `CONJ-005` | claim | `RESOLVED` | `mais-a2-2026` | Same/Selected | `AISafetyAtlas.Conjectures.MAIS.maisO34_marginAloneDoesNotIdentify` | [`CHECKED`](https://github.com/lionellevine/MAIS/issues/4) | | MAIS-O34(a) | A2 | `CONJ-009` | answer | `RESOLVED` | `mais-issue-4-2026` | Same/Literal | `AISafetyAtlas.Conjectures.MAIS.maisO34_exactFiberCandidate` | [`CHECKED`](https://github.com/lionellevine/MAIS/issues/4) | | MAIS-O38 | A3 | `CONJ-025` | claim | `RESOLVED` | `mais-a3-2026` | Same/Selected | `AISafetyAtlas.Conjectures.MAIS.maisO38_polynomialSamplesSuffice`
`AISafetyAtlas.Conjectures.MAIS.o38PolynomialSampleCandidate` | [`CHECKED`](https://github.com/lionellevine/MAIS/issues/30) | | MAIS-O70 | A6 | `CONJ-026` | target | `OPEN` | `mais-o70-2026` | Same/DetermineProblem | `AISafetyAtlas.Conjectures.MAIS.IsO70AWValueStratumTable`
`AISafetyAtlas.Conjectures.MAIS.IsO70RankTable`
`AISafetyAtlas.Conjectures.MAIS.O70DependsOnRanksOnly` | [`CONDITIONAL`](https://github.com/lionellevine/MAIS/issues/3) | | MAIS-O77 | A7 | `CONJ-028` | target | `OPEN` | `mais-o77-2026` | Same/DetermineProblem | `AISafetyAtlas.Conjectures.MAIS.IsO77MinimizerCharacterization`
`AISafetyAtlas.Conjectures.MAIS.IsO77SourceFiberVolumeOrderTable`
`AISafetyAtlas.Conjectures.MAIS.O77AllSaddlesHavePairOne` | [`PARTIAL`](https://github.com/lionellevine/MAIS/issues/12) | ## Assumed propositions Some results above are **conditional**: proved over a `Prop` the atlas states and does not prove. A theorem `frontier → X` reads exactly as strong whether the frontier is true or false, and neither a green build nor a clean axiom audit distinguishes the two — so the assumptions are listed here rather than left to be discovered in a binder. `Owed to` is the distinction that must not be collapsed. **candidate** means the submitted solution cites the proposition rather than deriving it, so assuming it leaves that submission's own derivation intact. **source** means the printed problem asserts it. **atlas** would mean we chose a formulation the source did not — the expensive kind. Never report a total across the three. | Frontier | Proposition | Owed to | Decision | |---|---|---|---| | `O70-EIGEN-LAW` | `AISafetyAtlas.SingularLearning.EigenvalueLawStatement` | candidate | `hold` | | `O70-EXACT-LOCAL` | `AISafetyAtlas.Conjectures.MAIS.O70ExactLocalPairsExist` | candidate | `hold` | | `O70-ZETA-BRIDGE` | `AISafetyAtlas.Conjectures.MAIS.O70ZetaPoleBridge` | source | `hold` | | `A7-ZETA-BRIDGE` | `AISafetyAtlas.Conjectures.MAIS.A7ZetaVolumeBridge` | source | `hold` | Each carries a frozen specification surface, an entry in [the frontier manifest](../../provenance/frontier-manifest.md), and unconditional stress artifacts, all checked by `scripts/check_frontier_evidence.py`, which prints the reasons in full on every run. **Passing that check is not evidence a frontier is true.** An artifact may only probe a formula or rule out a cheap branch.