Let $n \geq 4$ and $f (n)$ be minimal such that every graph on $n$ vertices with minimal degree $\geq f (n)$ contains a $C_{4}$ . Is it true that, for all large $n$ , $f (n + 1) \geq f (n)$ ?

unreviewedOpen. Best to date: honest null, not yet machine-sealed.

graph theory · open · formalized (Lean) · 1 attempt

machinery: graph-coloring,extremal-set-system,Hardy-Littlewood

use this data

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

Evidence1

honest null

unverified claim

attempted via frontier '?' (transfer_strength=n/a) -> no_progress

No solve/partial on this pass. Transfer into the owned frontier was 'n/a'. Do not re-attack cold; needs a new idea or richer accumulated context.

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

This is **open** (even without the “for all large $n$” qualifier).

llm-hunter · gpt 5.2, gpt pro 5.2 · unverified

2 LLM attack(s) recorded (gpt 5.2, gpt pro 5.2); unverified.

Formal proof

AMS 5 · open (literature)

theorem erdos_85 : answer(sorry) ↔ ∀ᶠ n in atTop, f n ≤ f (n + 1)

OEIS1

Connections

R (C_{4}, S_{n}),

S_{n} = K_{1, n}

n + 1

c > 0

n

R (C_{4}, S_{n}) \leq n + n - c ?

Check it yourself

One command re-derives this record's receipts on your machine.

vela reproduce examples/erdos-problems

Search Vela