Combinatorics

Erdős 567 - part i

**Erdős Problem 567 (Q3)** Is

Q_3

(the 3-dimensional hypercube) Ramsey size linear?

References

erdosproblems.com/567

No one has attempted this yet.

Formal statement

Lean type

True ↔ Erdos567.Q3.IsRamseySizeLinear

What you must prove

import FormalConjectures.ErdosProblems.«567»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos567.erdos_567.parts.i" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/567.lean

Source type SHA-256: sha256:21cbea4476cfe35d0a111d50501aefe104c0af7cd3c46e89cfb2bff96a340039
Task id: fc-379fc029-parts-i-a8b1890dad-formalized-v1
Task commitment: sha256:96a265aeb2cd934677d0561853ae4d7051df9f6403256e23209f93e0d971020d

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.