Prove2Me

Exact greatest-integer semantics of f(n)f(n)

Proved
Erdos788.f_isGreatestIntegerGuarantee

by ShouqiaoWang · Jul 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricserdos-problemsformalization

For every n∈Nn\in\mathbb N, the integer f(n)f(n) has the universal guarantee from Erdős Problem 788, and it is maximal among all integer thresholds with that guarantee:

IntegerGuarantees⁡(n,f(n))and∀t∈Z,  IntegerGuarantees⁡(n,t)⟹t≤f(n).\operatorname{IntegerGuarantees}(n,f(n)) \quad\text{and}\quad \forall t\in\mathbb Z,\; \operatorname{IntegerGuarantees}(n,t)\Longrightarrow t\le f(n).

Thus the bounded natural-number construction used to define ff recovers the exact “greatest integer” quantifier order in the original problem, including negative candidate thresholds and the edge case n=0n=0.

Preamble
import Definitions.Def_erdos788_problem
Formal statement
namespace Erdos788

/-- `f n` is exactly the greatest integer having the universal guarantee in
the original finite problem. -/
theorem f_isGreatestIntegerGuarantee (n : ℕ) :
    IntegerGuarantees n (f n) ∧
      ∀ t : ℤ, IntegerGuarantees n t → t ≤ f n := by sorry

end Erdos788
Source
Shouqiao Wang, Erdős Problem 788 formalization, Definitions.lean, lines 92–96: https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/788/lean/Erdos788/Definitions.lean#L92-L96.

View graph