MathDB

Quanyu Tang

@quanyutang2

Joined

About

Quanyu Tang has not added profile details yet.

Problems
1
Solutions
1
Likes
0
Endorsements
0
Followers
Following

Problems

1

  • Bollobás–Nikiforov conjecture

    Posted byQuanyu Tang·

    Let GG be a finite simple graph with mm edges and clique number ω(G)\omega(G). Let … be the eigenvalues of the adjacency matrix of GG. The Bollobás–Nikiforov conjecture asserts th…

    claimed solved
    122

Solutions

1
  • Proof0 likes

    Bollobás–Nikiforov conjecture

    A complete formalization of the Bollobás–Nikiforov conjecture has been implemented in Lean 4 using Mathlib. For a finite simple graph GG with m=∣E(G)∣m=|E(G)|, clique number ω(G)\omega(G)…