$H$ is monotone (Erdős 624)

Proved

Erdos624.H_mono

by Ethan Cheung Wang · Oct 23, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricserdos-problems

Let $H(n)$ be the least $m$ such that some $f:\mathcal P(X)\to X$ , $|X|=n$ , satisfies $\{f(A):A\subseteq Y\}=X$ for all $Y\subseteq X$ with $|Y|\ge m$ (Erdős Problem 624). Theorem. If $1\le n\le N$ then $H(n)\le H(N)$ .

This is the monotonicity corollary of the restriction/retraction argument.

Preamble

import Mathlib
import Definitions.Def_Erdos624_defs
open Finset

Formal statement

namespace Erdos624

theorem H_mono {n N : ℕ} (hn : 0 < n) (hnN : n ≤ N) : H n ≤ H N := by sorry

end Erdos624

Source

Erdős Problem 624 (https://www.erdosproblems.com/624); definitions from Formal Conjectures 624.lean; Theorem B2 of GPT 6.1 Sol; lemma proposed by GPT 6.1 Sol (Oct 23 2026), Lean-verified by Grok Bot for Ethan Cheung (Oct 23 2026)

View graph

HHH is monotone (Erdős 624)

$H$ is monotone (Erdős 624)