qedbot

Wikipedia·wikipedia:Hadamard

Hadamard's conjecture

conjecture formal record: mixed F3 anchored

Machine-checked by Palomar.

Fidelity F3: The project checks its proof with Comparator against a statement from a corpus written separately from the proof, and held here.

Source

AI activity

How grades work

No AI contribution recorded against this statement.

Fidelity

How fidelity is graded

F3 anchored. The project checks its proof with Comparator against a statement from a corpus written separately from the proof, and held here.

Anchored to google-deepmind/formal-conjectures/blob/abe6ef73129989fb8cf94edb72b1ac21d30a411b/FormalConjectures/Wikipedia/Hadamard.lean

declares divergences from its source reviewed by its authors only

Checks

1
  • verified·Palomar

    Registered by Palomar at 46544fab: Comparator confirmed 12 theorems prove the recorded statement within Palomar's axiom policy, replayed through Lean's kernel and the independent nanoda kernel

    project registered at a pinned commit·2026-08-31·commit 46544fab662e

    PALOMAR-2026-08-31-000001

Declared by the projects

1

As each project's formalization.yaml states it.

hadamard-formal: eight Hadamard orders unrecorded in the Cati-Pasechnik database, and the Miyamoto-erratum obstructionJD-Jones-ASES/Hadamard-formal · joined by anchor · Palomar

Read formalization.yaml

authors
JD Jones
method
agent — Claude Code (Fable 5), Codex (GPT 5.6 Sol), GPT 5.6 (external source review), Grok (external review; exact model not recorded)
review
self-assessed (JD Jones)
axioms
Classical.choice, Quot.sound, propext
sorry
0 unproved goals declared
results
12 main results named, checked with Comparator, with an alignment table
sources
Hadamard-T: T-matrix witnesses and the Hadamard orders they close — formalizes, authors participated; Hadamard-M: an erratum at order 515, and an explicit Hadamard matrix of order 7796 — formalizes, authors participated; A construction of Hadamard matrices — background; A database of constructions of Hadamard matrices — background
related
leanprover-community/mathlib4/blob/v4.33.0/Mathlib/LinearAlgebra/Matrix/HadamardMatrix.lean — builds-on; google-deepmind/formal-conjectures/blob/abe6ef73129989fb8cf94edb72b1ac21d30a411b/FormalConjectures/Wikipedia/Hadamard.lean — other; Lu-Ming Zhang, Formal Verification of Constructions and Theorems on Hadamard Matrices, MSc dissertation, University of Oxford, 2021 — other
divergences
The formalization uses the periodic T-matrix predicate required by the Cooper-Wallis construction, not the stronger aperiodic T-sequence notion, and it proves existence without materializing the resulting large matrices. On the erratum, the displayed C2 form, the pairing consequence of the paper's hypothesis (4.1), and the emptiness of the class at every positive block order not congruent to 1 mod 4 are formalized, which closes both printed readings of the corollary's output order; what remains informal is the transcription of the printed text, human-audited in Hadamard-M, and the bibliographic propagation from the unsupported order-103 entry to the order-515 list entry and its order-2060 claim.
checked by
Palomar

Follow and discuss

All discussion

Discussion and bounties for this problem load here.

Something wrong or missing here? Request a correction or add a claim, with its sources.

Formal material

Formal statements · 1
Cited proofs · 0

No proof artifact cited by the formal record.

Also known as · 2
  • https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Wikipedia/Hadamard.lean
  • FormalConjectures/Wikipedia/Hadamard.lean

Cite this record

qed.bot, “Hadamard's conjecture”, https://qed.bot/s/wikipedia-hadamard, as of 30 Sep 2026.

This record as plain text, with each claim, its grades and its sources.