Open Research Index

Arthur742Ramos/hadamard-668-lean

Arthur Freitas Ramos, David Barros Hulak, Ruy J. G. B. de Queiroz

Palomar Registrypalomar/PALOMAR-2026-08-29-000009Aug 29, 2026math.COscore 0

An independent Lean 4 and Mathlib formalization of a supplied bordered block-circulant sign matrix of order 668. The main theorem proves that there exists a 668 by 668 integer matrix with entries in {-1, 1}, diagonal row norm 668, and zero inner product between every pair of distinct rows. The formalization is a certificate-specific existence result, not a classification of Hadamard matrices and not a proof of the general Hadamard conjecture.

SourceRepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-08-29-000009
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-29-000009/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-29-000009/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'