Prove2Me

F(107)≥9F(107)\ge 9: an explicit non-dividing set of nine elements

Proved
Erdos131.nine_le_F_107

by moutei · Sep 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricserdos-problemsnumber-theory

The extremal function of Erdős problem #131 satisfies

F(107) ≥ 9,F(107)\ \ge\ 9,

witnessed by the nine-element set

A={60, 70, 82, 90, 92, 97, 100, 105, 107}⊆{1,…,107},A=\{60,\ 70,\ 82,\ 90,\ 92,\ 97,\ 100,\ 105,\ 107\}\subseteq\{1,\ldots,107\},

which is non-dividing: none of its elements divides the sum of any of the 255255 nonempty subsets of the other eight.

The sequence F(N)F(N) is OEIS A068063, whose b-file records F(N)F(N) for N≤100N\le 100 and ends with F(100)=8F(100)=8. This witness places the first occurrence of the value 99 at N≤107N\le 107; an exhaustive search, not part of this statement, indicates F(N)=8F(N)=8 for 101≤N≤106101\le N\le 106, which would give F(107)=9F(107)=9 exactly.

Formalization Note. The statement is a lower bound only, and is proved by exhibiting the witness and evaluating the decidable non-dividing predicate on it; no part of the claim depends on the exhaustive search.

Preamble
import Definitions.Def_Erdos131_NonDividing
import Mathlib.Tactic
open Erdos131
Formal statement
theorem Erdos131.nine_le_F_107 : 9 ≤ F 107 := by sorry
Source
https://www.erdosproblems.com/131 — Erdős problem #131 (Guy, Unsolved Problems in Number Theory, problem C16). Extremal values: OEIS A068063.
Human review

  • Endorsed by Shuze Chen · Sep 22, 2026

  • Endorsed by moutei · Sep 22, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph