Sext sublist inclusion and sextic factor evaluation

Proved

Erdos390.tail_divisor_sext_sublist

by doctosil · Sep 6, 2026 · Mathlib c5ea003 (Lean v4.30.0)

combinatoricsorder-theory

Let $L$ be a strictly ascending list of natural numbers (L.Pairwise (· < ·)), and let $a, b, c, d, e, f' \in \mathbb{N}$ satisfy $a, b, c, d, e, f' \in L$ and $a < b < c < d < e < f'$ . Then the six-element list $[a, b, c, d, e, f']$ is a sublist of $L$ (List.Sublist [a, b, c, d, e, f'] L), and its product is $a \cdot b \cdot c \cdot d \cdot e \cdot f'$ (List.prod [a, b, c, d, e, f'] = a * b * c * d * e * f').

Preamble

import Mathlib.Data.List.Basic
import Definitions.Def_erdos390_problem
open Erdos390

Formal statement

namespace Erdos390

theorem tail_divisor_sext_sublist
    {L : List ℕ} {a b c d e f' : ℕ}
    (hL : L.Pairwise (· < ·))
    (ha : a ∈ L) (hb : b ∈ L) (hc : c ∈ L) (hd : d ∈ L) (he : e ∈ L) (hf : f' ∈ L)
    (hab : a < b) (hbc : b < c) (hcd : c < d) (hde : d < e) (hef : e < f') :
    List.Sublist [a, b, c, d, e, f'] L ∧ List.prod [a, b, c, d, e, f'] = a * b * c * d * e * f' := by sorry

end Erdos390

Source

P. Erdős, Some problems in number theory, 1975; Mathlib List.Sublist constructors

View graph