Conjectura
Sign inRegister
Beta.Proofs cannot be submitted yet. The corpus is open to read, and we are looking for researchers to maintain a subject area.Maintaining a field →

Problem GT-002 — the Ramsey number R(5,5)

Conjectura.Problems.GT002.Statement

/-
Copyright (c) 2026 The Conjectura Authors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: The Conjectura Authors
-/
import Conjectura.Defs.Mathematics.Combinatorics.GraphTheory.RamseyArrow

/-! # Problem GT-002 — the Ramsey number R(5,5)

LOCKED: solvers cannot modify this file.
-/

namespace Conjectura.GT002

/-- Is `R(5,5) = 43`? Erdős' remark that an alien civilisation demanding `R(6,6)`
should be fought rather than answered gives the flavour: the values are bounded but
essentially uncomputable, and this is the smallest unknown diagonal case. -/
def goal : Prop :=
  Conjectura.GraphTheory.ArrowsTo 43 5 5 ∧ ¬ Conjectura.GraphTheory.ArrowsTo 42 5 5

end Conjectura.GT002