A covering array with 86 rows, 40 columns, and three symbols

Previous record

A strength-three ternary covering array has 40 columns whose entries come from three symbols. For every choice of three columns, all 27 ordered symbol triples must appear among its rows. The goal is to minimize the number of rows.

At the November 14, 2026 research cutoff, the best qualifying bound located in the maintained covering-array table was 87 rows, using Bai XunDi’s 87×40 construction. An 86-row predecessor with 39 columns was also known, but does not cover the required 40 columns. The challenge was to give an explicit valid array with fewer than 87 rows and all 40 columns.

Improved construction

The explicit construction has 86 rows and 40 columns, with symbols 0, 1, 2. Every one of the 9,880 increasing column triples realizes all 27 symbol triples: 266,760 of 266,760 required interactions are present.

In Lean, ColdHarvest.coldharvest_CA_86_3_40_3 proves that the certificate is a covering array. The theorem ColdHarvest.CAN_3_40_3_le_86 then establishes CAN(3,40,3) ≤ 86, where CAN denotes the minimum feasible number of rows. This is an improved upper bound, not a proof that 86 is optimal or that 85 rows are impossible.

Canonical certificate SHA-256: 7dc7ab1e231dce3cde5cc1c6b35c4911f34145fd4dfe5d80f8ea26b235b27f8a.

How the construction was obtained

The array was obtained by AI-assisted postoptimization of Bai’s 87-row construction. One row was removed, initially leaving 31 uncovered interactions. A coordinated-cell search reduced these to three; recognizing their shared aligned-column structure led to whole-pattern repair moves that eliminated the remaining gaps.

Row deletion, tabu search, and postoptimization are established techniques; the claimed contribution is the smaller explicit construction, not a new general-purpose optimization method. The provenance report describes the handoffs and limits of the preserved search history. The published certificate and Lean proof can be verified without rerunning the search.

Lean verification

The main Lean file proves coldharvest_CA_86_3_40_3 : IsCoveringArray certificate and CAN_3_40_3_le_86 : CAN₃ 40 3 ≤ 86. A proved Boolean-checker soundness theorem connects generated row witnesses to the quantified covering-array property; the checks themselves use decide +kernel, rather than native evaluation. An independent statement audit restates the theorem’s dimensions and minimum-row-count semantics.

The recorded clean build and fresh leanchecker --fresh kernel replay passed on Lean 4.28.0. The coverage theorem depends only on propext and Quot.sound; the minimum-row-count theorem additionally uses Classical.choice. There are no sorry declarations, added axioms, or native_decide dependencies in the proof. A separate Python checker exhaustively enumerates the original text matrix, and a deliberately invalid all-zero array is rejected.

Reproduction: see REPRODUCE.md and run ./verify.sh with the pinned Lean toolchain. The verification report and recorded transcript preserve commands, outcomes, timing, and resource measurements. Formal verification proves the stated mathematical upper bound; it does not establish novelty or optimality.

Prior art and record status

A wide prior-art investigation with a November 14, 2026 cutoff concluded LIKELY NOVEL for the numerical bound. It examined maintained and historical covering-array tables, original construction datasets, derived bounds, indirect algebraic constructions, research papers, supplementary materials, and public repositories. No prior result establishing an upper bound of 86 or fewer rows at these parameters was located.

The nearest verified predecessors include an 89-row bound for 40 columns, the Shokri–Moura 87×39 family member, and Bai XunDi’s deposited 87×40 and 86×39 arrays. The 86×39 case cannot imply this 40-column result merely by permuting rows, columns, or symbols. The full audit documents the searches, checked transformations, source citations, and access limitations.

Neither an exhaustive mathematical certificate nor a broad literature search proves worldwide historical priority. No optimality result for 86 is asserted.

Provenance

Chris Ozols, with AI-assisted construction, independent computation, and Lean 4 formalization. The explicit construction was developed on November 14, 2026 using Bai XunDi’s published 87-row array as the starting point, itself extending the strength-three construction lineage of Kianoosh Shokri and Lucia Moura. Both predecessors are credited in the repository.

The provenance and citation metadata describe attribution, source data and licenses, retained source handoffs, and independent checks. No submission to the record-table maintainer is represented as having occurred.

Sources, verification, and records

Original records and cited constructions

• Pinned ca-tools covering-array record table
• Bai XunDi’s 2026 deposited covering arrays
• Shokri–Moura strength-three construction paper

New construction and Lean proof

• Complete GitHub repository
• Explicit 86×40 array
• Readable mathematical proof
• Main Lean theorems (CA86.lean)
• Exact theorem and minimum-semantics audit (Verification.lean)

Reproduction, novelty, and provenance

• Reproduction instructions
• Verification report
• Recorded verification transcript
• Independent computational check
• Prior-art analysis and search limitations
• Full wide-RAG prior-art report (PDF)
• Construction provenance
• Citation metadata