Hoffman-Singleton Theorem

Stream: graph theory

[Rida Hamadani]

Hello,
I would like to formalize the Hoffman-Singleton Theorem, statement and proof. I don't have any experience writing proofs through lean other than very simple statements, and have no idea what are the best practices, so I was wondering if there is any problem or room for improvement with my current statement of the theorem, before I jump into writing a proof for it.

Here is the statement so far:

theorem hoffman_singleton [Fintype V] [DecidableEq V] {r : ℕ} {G : SimpleGraph V} [DecidableRel G.Adj]
    (h1 : G.IsRegularOfDegree r) (h2 : G.girth = 5) (h3 : Fintype.card V = r * r + 1) :
    r ∈ ({2, 3, 7, 57} : Finset ℕ) := by
  sorry

[Notification Bot]

Junyan Xu has marked this topic as resolved.

[Notification Bot]

Junyan Xu has marked this topic as unresolved.

[Alena Gusakov]

Is this related to strongly regular graphs? There's some strongly regular graph stuff but it's very minimal

[Kevin Buzzard]

That looks like the statement of a theorem (although I can't comment on whether it's the Hoffmann-Singleton theorem until you give me a maths statement of that theorem) -- of course you shouldn't just leap straight into a proof of it, there's an art to all this :-) It's far better to have twenty lemmas with five line proofs than one lemma with a 100 line proof which gets very tedious to write. So your next step is to break the proof up into small chunks. This is a mathematical exercise, not a lean one.

[Rida Hamadani]

Alena Gusakov said:

Is this related to strongly regular graphs? There's some strongly regular graph stuff but it's very minimal

Yes, the first step of the proof is to show that G is strongly regular, I'll make use of mathlib's strongly regular graphs, thank you.

[Rida Hamadani]

Kevin Buzzard said:

I can't comment on whether it's the Hoffmann-Singleton theorem until you give me a maths statement of that theorem

The theorem states that if a regular graph of degree r and girth 5 has r²+1 vertices, then r ∈ {2, 3, 7, 57}.

Kevin Buzzard said:

So your next step is to break the proof up into small chunks. This is a mathematical exercise, not a lean one.

Thank you, I will do that. In fact, we show the graph to be strongly regular first, it is convenient that the definition is already implemented in mathlib!

[Rida Hamadani]

As a lemma to the Hoffman-Singleton theorem, I'm trying to state and proof the fact that

$$I_n + \text{Adj}\left(G\right) + \text{Adj}\left(G^c\right) = J_n$$

(which sounds like something mathlib should have), this mwe represents how I stated it:

import Mathlib.Combinatorics.SimpleGraph.AdjMatrix

open SimpleGraph Matrix

universe u

variable {V : Type u} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj]

instance allOnes : (Matrix V V ℕ) :=
  λ _ _ => 1

instance unit : (Matrix V V ℕ) :=
  λ i j => if i = j then 1 else 0

theorem adjMatrix_plus_adjMatrix_compl_eq : unit + G.adjMatrix ℕ + compl (G.adjMatrix ℕ) = allOnes := by
  sorry

But the problem here is that:

• I had to define the all-ones and the unit matrices myself. Ideally, I would like to use such definitions from mathlib.
• I don't like the fact that the theorem is defined as addition between Matrix V V ℕ's instead of Matrix n n ℕ's where n = Fintype.card V, it doesn't feel "natural".

What is the best way to address these problems?

[Johan Commelin]

The unit matrix is simply written 1. I'm not sure if we have the all-ones matrix...

[Mario Carneiro]

the all ones matrix is fun _ _ => 1, I didn't see a definition for this in a quick skim

[Johan Commelin]

To address your other point: if you use n, then you need to explain which vertex corresponds to row/column 1,2,3,...

[Johan Commelin]

People tend to gloss over this on paper. You can choose an ordering of the vertices, but that quickly becomes annoying

[Rida Hamadani]

I see, that makes sense. Thank you!

[Kevin Buzzard]

Note that instance allOnes... is wrong because Matrix isn't a class. Use abbrev instead

[Rida Hamadani]

I skimmed quickly through the "Theorem Proving in Lean4" Manual and couldn't find anything about abbrev. So to ask for a fishing rod instead of a fish, is there a documentation that explains things such as abbrev, class, notation, etc.

[Kevin Buzzard]

#tpil certainly has stuff about classes and notation. abbrev is a reducible inline definition

[Rida Hamadani]

I proved that

$$I_n + \text{Adj}\left(G\right) + \text{Adj}\left(G^c\right) = J_n$$

Is this statement in scope of mathlib? I feel like it belongs to the Compl section of this file:
https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean

If yes, I would like to request write access to non-master branches, and I'll send my proof here in order to get feedback on it before doing any PRs.

[Alex J. Best]

@maintainers :up:

[Anatole Dedecker]

What is your GitHub username? Don't hesitate to open a (draft ?) PR right away, it's much easier to review code on GitHub than on Zulip.

[Anatole Dedecker]

Ah, it's in your profile. Give me a second

[Anatole Dedecker]

Invitation sent!

[Rida Hamadani]

Thank you!