AI Proof WatchKeep up with AI contributions

AI-assisted Hadamard constructions cover eight orders

Using periodic T-matrix quadruples of orders 103 and 163 and symmetric-circulant Williamson quadruples of orders 7, 11, 13, 17, 19, 23 and 29, a formalized Cooper–Wallis construction gives Hadamard matrices at orders 2884, 4532, 7004, 7172, 7828, 8476, 9476 and 11948. A separate parity result rules out Miyamoto’s displayed C2-matrix ingredient at positive block orders not congruent to 1 mod 4.

Sources for this record

What was already known

Cooper–Wallis and Goethals–Seidel supplied the general constructions. Cati and Pasechnik’s cited table did not record these eight output orders; Schneider’s human matrix supplied the source behind the order-103 T data.

AI involvement AI-centered

JD Jones selected and managed the project. Claude agents produced the source mathematics and the C2 obstruction; Codex agents formalized selected witnesses and constructions. Schneider retains credit for the matrix behind the order-103 source data, and Cooper–Wallis for the classical construction.

AI search and mathematical work supplied the retained T163 witness and the erratum obstruction, and AI agents formally checked the eight applications; T103 partly derives from Schneider’s separately credited human matrix.

Importance Notable

Provides eight explicit constructions and identifies a limit of one printed C2-based route.

Limitations

The C2 obstruction invalidates that displayed route, not Hadamard existence at order 2060 by other means. The eight-order baseline is tied to a dated table, and interpreting Miyamoto’s printed premise is outside the machine proof.

Technical verification Formal (Lean 4/Mathlib kernel with finite decide checks, transitive axiom audit and Comparator statement matching)

The cited project reports kernel-checked finite T and Williamson predicates, formal generic Cooper–Wallis and obstruction proofs, plus axiom and Comparator audits. The historical database status and printed-text interpretation are documentary, outside the machine proof.

Formal checking

kernel reduction of concrete predicates, formal symbolic construction and parity proofs, selected statement and axiom checks

Checker
Lean 4 kernel and project axiom audit
Scope
The two periodic T witnesses, seven Williamson witnesses, eight selected Hadamard existence theorems, and handshake/C2 obstruction declarations
Basis
Reported by the linked checker
Evidence source

Checking a formal statement does not establish that it matches the original problem.

Human understanding Few

The source-side explanations and external reviews are AI-generated; the human audit concerns source transcription, not a documented human explanation of the complete construction or its verification. Few is the evidence-gap default.

Correction and publication history

2026-10-18 · publication

Provides eight explicit constructions and identifies a limit of one printed C2-based route.

Read this published revision