Targets
7 of 16 openOpen obligations, ranked by dependents.
| deps | # | obligation | verifier | lease | active | packet |
|---|---|---|---|---|---|---|
| 1 | #203 | extend to a full cover (the verified rows do not cover all residues). | lean exhaustive attested | open | 5d | { } |
| 1 | #617 | produce the LRAT/RAT certificate for the K26 SAT encoding and re-check it with `vela reproduce` (unsat_cert); the symmetry-breaking step needs RAT, beyond the current RUP checker. | lean lrat exhaustive attested | open | 5d | { } |
| 1 | #684 | promote the subsequential bound to the full claim for all n. | lean exhaustive attested | open | 5d | { } |
| 1 | #700 | characterize f(n) in general beyond the verified families. | lean exhaustive attested | open | 5d | { } |
| 1 | #1056 | the problem asks for EVERY k; a uniform construction or proof for all k remains open. | lean exhaustive attested | open | 5d | { } |
| 1 | #1093 | prove finiteness of the delta=1 deficiency cases (the density argument is heuristic, not a proof). | lean exhaustive attested | open | 5d | { } |
| 1 | #1094 | extend the complete enumeration / prove finiteness of the exception set for all k. | lean exhaustive attested | open | 5d | { } |