Quad sublist inclusion and quartic factor evaluation

Proved

Erdos390.tail_divisor_quad_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 \in \mathbb{N}$ satisfy $a, b, c, d \in L$ and $a < b < c < d$ . Then the four-element list $[a, b, c, d]$ is a sublist of $L$ (List.Sublist [a, b, c, d] L), and its product is $a \cdot b \cdot c \cdot d$ (List.prod [a, b, c, d] = a * b * c * d).

Preamble

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

Formal statement

namespace Erdos390

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

end Erdos390

Source

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

View graph