Existence of monochromatic quantum graphs

Stream: Formal conjectures

[Mario Krenn]

I would like to start formalizing the problem I posted as issue 2205. Even before starting, I have two question:

The conjecture is (details omitted) that a certain system of equations (parametrized by an integer N and an integer c, where N denotes the number of vertices and c the number of colors) with ( O(c^2 n^2) ) complex variables and d^N equations has no solutions for any N > 6 and c > 3.

There are no known proofs (either for the existence or non-existence of solutions) for any such N and c. This means that, in fact, there are infinitely many open problems, and progress on any specific pair (N,c) would already be interesting.

Thus, my first question: What is best practice for adding an open problem that has infinitely many open subproblems?

In addition, the systems of equations become very large. I generated the full explicit system, and for

• N = 6, c = 3: 350 kB
• N = 6, c = 4: 1.9 MB
• N = 8, c = 3: 28.7 MB

This means I obviously cannot write out the full system explicitly. So I am wondering -- my second question: Is the enormous size of these equation systems a problem when working in Lean?

[Franz Huschenbeth]

Hello Mario,

Regarding your first question I would generally go with adding the easiest of the problems. Meaning here it would probably be (6, 3) and maybe 1-2 other variants that you think are the easiest. Another option would be to ask for a proof for the existence or nonexistence of a pair (N, c). That would make sure that non-intuitive easier solutions can also be provided, such as Dimension 8 / 24 in the Sphere Packing Problem. I would recommend simply doing both methods.

Regarding your second question, it might be a problem. I am not sure if Lean has good API to take in large systems of equations in some format (other than writing them out). You could ask in some relevant channels. Is there some other way in which you could formulate the conjecture? I think the graph theoretic formulation is probably better for Lean. Mathlib already has quite a bit on graph theory, you can ask an AI Model to search in Mathlib or use moogle.ai / Lean-Explore.

[Snir Broshi]

I'm confused at the response to the second question. I don't know the details, but if you "generated the full explicit system" I'm assuming that means there's code that does that. So shouldn't writing that same code in Lean give you exactly what you want, without any size blowup?

[Franz Huschenbeth]

Sounds like a valid idea, just using Lean's Metaprogramming. Might work well enough, but makes me wonder how it would affect compile time, when generating such big systems of equations.

[Paul Lezeau]

I haven’t looked at the MO post too carefully, but it seems that your family of equations has a closed form formula. I’d suggest formalising the problem(s) using that (and specialising down to explicit N and c when necessary)

[Snir Broshi]

Franz Huschenbeth said:

Sounds like a valid idea, just using Lean's Metaprogramming.

I'm not talking about metaprogramming, just regular programming

[Snir Broshi]

There's no reason to generate theorems when you can just talk about a function mapping (N, c) to a set of equations

[Mario Krenn]

I started with this now (super fun!). I created a proof that solution exist for N=4, d=3 (by explicitly giving the solution), and i expressed the same system for N=4, d=4 - in a way that no solution exists (with a sorry, because no proof is known).

Before moving further, could you please check the code and check whether it makes sense or you suggest some adaptations?

This is the case N=4 d=3 which exists:

import Mathlib

/-
Indices 0,1,2 as `Fin 3`.
We encode the different “edge types” as an inductive, and weights are just `Edge → ℕ`.
-/

inductive Edge : Type
  | ab (a b : Fin 3)
  | ac (a c : Fin 3)
  | ad (a d : Fin 3)
  | bc (b c : Fin 3)
  | bd (b d : Fin 3)
  | cd (c d : Fin 3)
deriving DecidableEq

open Edge

abbrev Weights := Edge → ℂ

/-- Your d=3 equation template:
For all a,b,c,d ∈ {0,1,2}:
  w_ab(a,b)*w_cd(c,d) + w_ac(a,c)*w_bd(b,d) + w_ad(a,d)*w_bc(b,c)
    = 1  iff  a=b=c=d
    = 0  otherwise
-/
def EqSystem (W : Weights) : Prop :=
  ∀ (a b c d : Fin 3),
    W (ab a b) * W (cd c d) + W (ac a c) * W (bd b d) + W (ad a d) * W (bc b c)
      = (if a = b ∧ b = c ∧ c = d then (1 : ℂ) else (0 : ℂ))

/-- Your example assignment (all other weights = 0):

w_a0b0 = 1
w_a1c1 = 1
w_a2d2 = 1
w_b1d1 = 1
w_b2c2 = 1
w_c0d0 = 1
-/
def exampleW : Weights :=
  fun e =>
    if e = ab 0 0 then (1 : ℂ) else
    if e = ac 1 1 then (1 : ℂ) else
    if e = ad 2 2 then (1 : ℂ) else
    if e = bd 1 1 then (1 : ℂ) else
    if e = bc 2 2 then (1 : ℂ) else
    if e = cd 0 0 then (1 : ℂ) else
    (0 : ℂ)

/-- The system is satisfiable over ℕ (witness: `exampleW`). -/
theorem eqSystem_has_solution : ∃ W : Weights, EqSystem W := by
  refine ⟨exampleW, ?_⟩
  intro a b c d
  fin_cases a <;> fin_cases b <;> fin_cases c <;> fin_cases d <;>
  simp [exampleW]

This is the case N=4 d=4 for which no solution is known (and probably none exists):

import Mathlib

/-
N = 4 vertices a,b,c,d
local dimension d = 4  (indices 0,1,2,3 as Fin 4)
weights are complex numbers
-/

inductive Edge : Type
  | ab (a b : Fin 4)
  | ac (a c : Fin 4)
  | ad (a d : Fin 4)
  | bc (b c : Fin 4)
  | bd (b d : Fin 4)
  | cd (c d : Fin 4)
deriving DecidableEq

open Edge

abbrev Weights := Edge → ℂ

def EqSystem (W : Weights) : Prop :=
  ∀ a b c d : Fin 4,
    W (ab a b) * W (cd c d) + W (ac a c) * W (bd b d) + W (ad a d) * W (bc b c)
      = (if a = b ∧ b = c ∧ c = d then (1 : ℂ) else (0 : ℂ))

/-- Conjecture: for d=4, there is no complex solution. -/
theorem eqSystem_no_solution_conjecture :
  ¬ ∃ W : Weights, EqSystem W := by
  sorry

[Mario Krenn]

Note, someone has performed a Gröbner basis computation and shown that no solution exists for N=4, d=4, but i never verified the assumption of the code or implementation - thus i would still keep the case N=4,d=4 as a quasi-open case, maybe some future AIs find a different proof that relies less on computation (for any N>=6, d>=3, no solution is known or can be proven).

[Mario Krenn]

I do have now two codes (spending lots of time with GPT 5.2 Pro), one for N=4 (with 2 theorems using witnesses for d=2 and 3, and one conjeture for d=4) and one for N=6 (one theorem with a witness for d=2 and a conjecture for d=3).

I am able to validate by hand the two codes, i would still be very happy if someone could look at it and check whether i do something weird with them.

This is for N=4:

import Mathlib

/-!
N = 4 (vertices a,b,c,d).

We sum over the 3 perfect matchings of K₄:
(ab)(cd), (ac)(bd), (ad)(bc)

Generalization parameters:
- local dimension `D : Nat` (indices in `Fin D`)
- coefficient type `α` with `[Semiring α]` (weights in α)
-/

/-- Edge labels for K₄, carrying the two local indices at their endpoints. -/
inductive Edge4 (D : Nat) : Type
  | ab (a b : Fin D)
  | ac (a c : Fin D)
  | ad (a d : Fin D)
  | bc (b c : Fin D)
  | bd (b d : Fin D)
  | cd (c d : Fin D)
  deriving DecidableEq

open Edge4

/-- A weight assignment for N=4. -/
abbrev Weights4 (D : Nat) (α : Type) := Edge4 D → α

/-- Sum over the 3 perfect matchings of K₄ (for fixed indices a b c d). -/
def pmSum4 {α : Type} [Semiring α] (D : Nat) (W : Weights4 D α) (a b c d : Fin D) : α :=
  W (ab a b) * W (cd c d)
  + W (ac a c) * W (bd b d)
  + W (ad a d) * W (bc b c)

/-- The N=4 equation system for local dimension D. -/
def EqSystem4 {α : Type} [Semiring α] (D : Nat) (W : Weights4 D α) : Prop :=
  ∀ a b c d : Fin D,
    pmSum4 (D := D) W a b c d
      = (if a = b ∧ b = c ∧ c = d then (1 : α) else (0 : α))

/-! ## d = 2 : witness & proof (works over any semiring α) -/

section D2
variable {α : Type} [Semiring α]

def Witness4_d2 : Weights4 2 α :=
  fun e =>
    if e = ab 0 0 then (1 : α) else
    if e = ac 1 1 then (1 : α) else
    if e = bd 1 1 then (1 : α) else
    if e = cd 0 0 then (1 : α) else
    (0 : α)

theorem eqSystem4_has_solution_d2 : ∃ W : Weights4 2 α, EqSystem4 (D := 2) W := by
  classical
  refine ⟨Witness4_d2 (α := α), ?_⟩
  intro a b c d
  fin_cases a <;> fin_cases b <;> fin_cases c <;> fin_cases d <;>
    simp [pmSum4, Witness4_d2]
end D2

/-! ## d = 3 : witness & proof over ℂ -/

def Witness4_d3 : Weights4 3 ℂ :=
  fun e =>
    if e = ab 0 0 then (1 : ℂ) else
    if e = ac 1 1 then (1 : ℂ) else
    if e = ad 2 2 then (1 : ℂ) else
    if e = bd 1 1 then (1 : ℂ) else
    if e = bc 2 2 then (1 : ℂ) else
    if e = cd 0 0 then (1 : ℂ) else
    (0 : ℂ)

theorem eqSystem4_has_solution_d3 : ∃ W : Weights4 3 ℂ, EqSystem4 (D := 3) W := by
  classical
  refine ⟨Witness4_d3, ?_⟩
  intro a b c d
  fin_cases a <;> fin_cases b <;> fin_cases c <;> fin_cases d <;>
    simp [pmSum4, Witness4_d3]

/-! ## d = 4 : conjecture (no solution) over ℂ -/

theorem eqSystem4_no_solution_conjecture_d4 :
    ¬ ∃ W : Weights4 4 ℂ, EqSystem4 (D := 4) W := by
  sorry

This is for N=6:

import Mathlib

/-!
N = 6 (vertices a,b,c,d,e,f).
We sum over the 15 perfect matchings of K₆ (each term is a product of 3 edge weights).

Generalization parameters:
- local dimension D : Nat  (indices live in Fin D)
- coefficient type α with [Semiring α] (weights in α)
-/

/-- Edge labels for K₆, each carrying the two local indices at its endpoints. -/
inductive Edge6 (D : Nat) : Type
  | ab (a b : Fin D) | ac (a c : Fin D) | ad (a d : Fin D) | ae (a e : Fin D) | af (a f : Fin D)
  | bc (b c : Fin D) | bd (b d : Fin D) | be (b e : Fin D) | bf (b f : Fin D)
  | cd (c d : Fin D) | ce (c e : Fin D) | cf (c f : Fin D)
  | de (d e : Fin D) | df (d f : Fin D)
  | ef (e f : Fin D)
  deriving DecidableEq

open Edge6

abbrev Weights6 (D : Nat) (α : Type) := Edge6 D → α

/-- Sum of weights of all 15 perfect matchings of K₆. -/
def pmSum6 {α : Type} [Semiring α] (D : Nat) (W : Weights6 D α)
    (a b c d e f : Fin D) : α :=
    W (ab a b) * W (cd c d) * W (ef e f)
  + W (ab a b) * W (ce c e) * W (df d f)
  + W (ab a b) * W (cf c f) * W (de d e)

  + W (ac a c) * W (bd b d) * W (ef e f)
  + W (ac a c) * W (be b e) * W (df d f)
  + W (ac a c) * W (bf b f) * W (de d e)

  + W (ad a d) * W (bc b c) * W (ef e f)
  + W (ad a d) * W (be b e) * W (cf c f)
  + W (ad a d) * W (bf b f) * W (ce c e)

  + W (ae a e) * W (bc b c) * W (df d f)
  + W (ae a e) * W (bd b d) * W (cf c f)
  + W (ae a e) * W (bf b f) * W (cd c d)

  + W (af a f) * W (bc b c) * W (de d e)
  + W (af a f) * W (bd b d) * W (ce c e)
  + W (af a f) * W (be b e) * W (cd c d)

/-- The N=6 equation system for local dimension D. -/
def EqSystem6 {α : Type} [Semiring α] (D : Nat) (W : Weights6 D α) : Prop :=
  ∀ a b c d e f : Fin D,
    pmSum6 (D := D) W a b c d e f
      = (if a = b ∧ b = c ∧ c = d ∧ d = e ∧ e = f then (1 : α) else (0 : α))

/-! ## d = 2 : satisfiable (your witness), works over any semiring α -/

section D2
variable {α : Type} [Semiring α]

/-- Your d=2 witness: 6 weights = 1, everything else = 0. -/
def Witness6_d2 : Weights6 2 α :=
  fun ed =>
    if ed = ab 0 0 then (1 : α) else
    if ed = af 1 1 then (1 : α) else
    if ed = bc 1 1 then (1 : α) else
    if ed = cd 0 0 then (1 : α) else
    if ed = de 1 1 then (1 : α) else
    if ed = ef 0 0 then (1 : α) else
    (0 : α)

/-- The system is satisfiable for d=2. -/
theorem eqSystem6_has_solution_d2 : ∃ W : Weights6 2 α, EqSystem6 (D := 2) W := by
  classical
  refine ⟨Witness6_d2 (α := α), ?_⟩
  intro a b c d e f
  -- 2^6 = 64 cases
  fin_cases a <;> fin_cases b <;> fin_cases c <;> fin_cases d <;> fin_cases e <;> fin_cases f <;>
    simp [pmSum6, Witness6_d2]
end D2

/-! ## d = 3 : conjecture (no solution), stated over ℂ -/

theorem eqSystem6_no_solution_conjecture_d3 :
    ¬ ∃ W : Weights6 3 ℂ, EqSystem6 (D := 3) W := by
  sorry

Now, for larger (even) N, it gets highly unconvinient to write the pmSumN function by hand, thus i try to generalize this approach to arbitrary even N.

I have 3 questions:
1) Do the two codes look reasonable?
2) For contributing to formal_conjectures, would you prefere the hardcoded codes (as above), or do you prefere one general expression and then deriving numerous special cases from there?
3) I am trying to generlize with GPT Pro such that i understand it. After long time of fixing bugs, it seems to decide to go for a recursive computation of the perfect matchings (which makes sense and i use similar techniques in python). Would this also be your choice, or would you generalize the two codes (that necessarily involves a funciton for enumerating the perfect matchings for arbitrary even graphs?) in a different way? Are there already useful functions to do so in mathlib?

[Moritz Firsching]

Mario Krenn said:

I do have now two codes (spending lots of time with GPT 5.2 Pro), one for N=4 (with 2 theorems using witnesses for d=2 and 3, and one conjeture for d=4) and one for N=6 (one theorem with a witness for d=2 and a conjecture for d=3).

I am able to validate by hand the two codes, i would still be very happy if someone could look at it and check whether i do something weird with them.

Now, for larger (even) N, it gets highly unconvinient to write the pmSumN function by hand, thus i try to generalize this approach to arbitrary even N.

I have 3 questions:
1) Do the two codes look reasonable?
2) For contributing to formal_conjectures, would you prefere the hardcoded codes (as above), or do you prefere one general expression and then deriving numerous special cases from there?
3) I am trying to generlize with GPT Pro such that i understand it. After long time of fixing bugs, it seems to decide to go for a recursive computation of the perfect matchings (which makes sense and i use similar techniques in python). Would this also be your choice, or would you generalize the two codes (that necessarily involves a funciton for enumerating the perfect matchings for arbitrary even graphs?) in a different way? Are there already useful functions to do so in mathlib?

1) Yes, I suppose
2) I think getting the first (easiest) open case is most interesting here, and for the general case a general expression would be preferred over large system of equations.
3) Seems like this is a difference between a more recursive approach and just defining the set of all perfect matching and filtering? Seems like the latter is more easy?

Perhaps you can draft a pull request and we can discuss there?

[Mario Krenn]

Thanks, i've done so: PR