What this programme is about
Many branches of mathematics leave narrow gaps between upper and lower bounds on finite discrete structures. This programme resolves those finite gaps by determining exact integer values for concrete combinatorial objects. It computes the smallest circuit computing an algebraic operator, the fewest vectors admitting a quantum contextuality proof, or the densest graph avoiding forbidden subgraphs.
A resolved number provides a physical floor for applied engineering. Knowing the exact gate count of a Boolean operator prevents hardware designers from hunting for smaller implementations. Knowing the minimum comparator count for median networks guarantees optimal hardware sorting pipelines. These exact bounds also reveal where automated reasoning engines fail, pinpointing the precise structures where Boolean satisfiability solvers hit combinatorial explosions.
What has been settled
For quantum measurement sets, MF-184 eliminated 18-vector systems in C^6, improving the universal lower bound m_d ≥ 18 of Xu-Chen-Gühne (2020) and narrowing m_6 to [19, 21] alongside Lisoněk et al. (2014). MF-195 excluded 19 vectors, pushing m_6 ≥ 20; this proof repaired a constraint set to rule out a spurious (2,1,1) triple by enforcing e_3 = 0 for b' ≤ 1. MF-199 excluded 20 vectors, proving m_6 = 21 exactly, conditional on the Xu-Chen-Gühne lemma. MF-185 proved external rays share non-adjacent basis rays in orthogonality graphs.
In Boolean circuit synthesis, MF-181 proved the resolved-carry family K_m requires exact multiplicative complexity MC(K_m) = 2m + 1. MF-190 fixed the 5-input MOD3,1 B2 circuit size at 9 gates using an explicit circuit and a DRAT refutation of 8 gates; Knuth (TAOCP 7.1.2) solved n ≤ 5 by SAT with no published certificates. MF-189 certified minimal single-output median networks at 13 comparators on 7 channels and 10 comparators for the 6-channel lower median, where Dobbelaere listed 13 with no proof.
In tournament and graph combinatorics, MF-197 verified t(7) > 12 across fourteen amalgam cubes with DRAT certificates, matching Zhang-Szeider (2023). MF-198 proved every 7-universal tournament on 13 vertices has automorphism group order 1 or 3. MF-192 verified structural obstructions against 11-hosts for nine 7-tournaments, noting that t(7) > 11 is counting-trivial. MF-191 certified code size A(11,4,5) = 66 via SAT, checking a value from Brouwer's table and Östergård (2010). MF-186 showed 133-weight 16×17 Zarankiewicz matrices have maximum row degree at most 10, addressing the z(16,17;3) in {132, 133} gap from August 2026. MF-193 produced multiplier-free contraction censuses for CW(112,36), generalizing Arasu-Gordon-Zhang (2021). MF-188 proved (J4,J7;26)-graphs with minimum degree at least 9 uniquely match the vertex-deleted Schläfli complement, extending MR91.
What is still open
Solvers hit scaling barriers across several frontier cells. For tournament universality, ML-090 leaves 13 ≤ t(7) ≤ 15 undecided because CEGAR search times out at order 13. In extremal matrices, ML-091 leaves z(16,17;3) ∈ {132, 133} open; DRAT refutes row degrees 11 through 17, while eight sub-cubes stall at degrees 9 and 10. For sorting networks, ML-092 leaves median sizes open for n ≥ 8 after SAT timeouts; Smith's 1996 claim for n = 9 failed reproduction.
Circuit bounds stall under exponential costs: ML-094 leaves 6-input MOD3,0 open, where Knuth conjectures 12 gates and an 11-gate refutation timed out. In proof complexity, ML-095 leaves h_11 ≥ 28 undetermined above Peitl-Szeider's h_10 = 26, correcting the catalogue to 626,973 candidates. For codes, ML-096 leaves A(13,4,5) ∈ [123, 129] open. In algebra, ML-093 shows CW(112,36) resists DRAT and RoundingSat cutting planes due to a proof-system mismatch.
How to read the evidence
Receipted results and machine certificates dominate this programme, supported by exhaustive checks and written proofs. Machine certificates, including DRAT unsatisfiability proofs and Lean formalizations, warrant the highest trust because independent checkers verify every step without relying on solver heuristics or human referee oversight. Receipted search records guarantee reproducible computational logs. When an entry lists an empirical wall or solver timeout, it marks the technical limit of existing automated reasoning algorithms on that specific structure.