Wang Hadamard Permanent Nonvanishing

Every real sign Hadamard matrix of order > 2 has nonzero permanent; encoded over integers, without a Sylvester or circulant restriction. See the sources in the module documentation.

$994 bounty

Solve it

Nobody has attempted this. A complete proof or refutation takes the whole bounty.

Submit a proof

Where this lives

conjectures-tasks

The pinned statement, the Lean challenge file and the exact bundle you build against.

versions/fc-v2-wanghadamardpermanentnonvanishing-conjecture-5f0551dde92c57fbf12e4df4-formalized →

Formal statement

Proof target

import Mathlib
import FormalConjectures.HistoricalOpen.WangHadamardPermanentNonvanishing
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "FullOldProblemsCatalog.WangHadamardPermanentNonvanishing.conjecture" := by
  sorry

end Bounty

Open this target’s Challenge.lean Task bundle on GitHub

Original conjecture (Lean type)

FullOldProblems.WangHadamardPermanentNonvanishing

Original conjecture source: FormalConjectures/HistoricalOpen/WangHadamardPermanentNonvanishing.lean

The audit patch changes this file, so the upstream version can differ from the statement above.

Source type SHA-256: sha256:7ffca3ce495f615e44f8bafb96cef55149d1d4214cf5970127676b8fc6cf5b80
Task id: fc-v2-wanghadamardpermanentnonvanishing-conjecture-5f0551dde92c57fbf12e4df4-formalized
Task commitment: sha256:79e9829193391c82e178407ae7a61a1bec333d41ace22d5a073cf5b68c18177a

References

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.

Our channel is in the Bittensor Discord server. Join the server first, then open the channel to send your report.

Bittensor Discord

import Mathlib import FormalConjectures.HistoricalOpen.WangHadamardPermanentNonvanishing import TaskSupport namespace Bounty theorem target : fcTypeOfName% "FullOldProblemsCatalog.WangHadamardPermanentNonvanishing.conjecture" := by sorry end Bounty