Erdős Problem 390 — exact finite model and asymptotic target

Definition

erdos390_problem

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

asymptoticscombinatoricserdos-problemsfactorialsnumber-theory

For natural numbers $n$ and $M$ , let

I(n,M)=\{a\in\mathbb N:n<a\le M\}.

Call $M$ an admissible endpoint for $n$ if there is a finite set $A\subseteq I(n,M)$ whose product is $n!$ . Because $A$ is a set, its factors are automatically distinct. For $n\ge3$ , define $f(n)$ to be the least admissible endpoint; set $f(n)=0$ for $n<3$ only to make $f$ a total function.

Define

C_0=\frac{4029639598}{25970038185},\qquad s(n)=\frac{n}{\log n},\qquad E(n)=f(n)-\bigl(2n+C_0s(n)\bigr).

The main asymptotic proposition is $E=o(s)$ along the natural numbers tending to infinity. For the complementary formulation, also define

Q(n,M)=\frac{M!}{(n!)^2}

as a rational number, and say that $(n,M)$ has a complement product if some finite subset of $I(n,M)$ has product $Q(n,M)$ .

These definitions provide the exact finite model and asymptotic target used by the mission.

Formalization Note Real logarithm and division are total operations. Thus the displayed functions also have formal values at small $n$ , but every asymptotic assertion is taken at $n\to\infty$ . The quotient $Q(n,M)$ is rational rather than truncated natural-number division.

Definition code

import Mathlib.Analysis.Asymptotics.Defs
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Data.Finset.Interval
import Mathlib.Data.Nat.Factorial.Basic

open Filter
open scoped BigOperators

namespace Erdos390

noncomputable section

/-- The integer interval `(n, M]`. -/
def factorInterval (n M : ℕ) : Finset ℕ :=
  Finset.Ioc n M

/-- There is a factorization of `n!` into distinct integers in `(n, M]`. -/
def IsAdmissibleEndpoint (n M : ℕ) : Prop :=
  ∃ factors : Finset ℕ,
    factors ⊆ factorInterval n M ∧ factors.prod id = n.factorial

/-- For `n ≥ 3`, the singleton factorization `{n!}` supplies an endpoint. -/
theorem exists_admissibleEndpoint {n : ℕ} (hn : 3 ≤ n) :
    ∃ M, IsAdmissibleEndpoint n M := by
  refine ⟨n.factorial, {n.factorial}, ?_, by simp⟩
  intro a ha
  have ha' : a = n.factorial := by simpa using ha
  subst a
  simp [factorInterval, Nat.lt_factorial_self hn]

/-- The least possible largest factor. Outside the paper's domain `n ≥ 3`,
the value is set to zero solely to make the function total. -/
def f (n : ℕ) : ℕ :=
  by
    classical
    exact if hn : 3 ≤ n then Nat.find (exists_admissibleEndpoint hn) else 0

/-- The exact second-order constant in the proposed solution. -/
def C0 : ℝ :=
  (4029639598 : ℝ) / 25970038185

/-- The second-order scale `n / log n`. -/
def secondOrderScale (n : ℕ) : ℝ :=
  (n : ℝ) / Real.log (n : ℝ)

/-- The error after subtracting the asserted two leading terms. -/
def mainError (n : ℕ) : ℝ :=
  (f n : ℝ) -
    (2 * (n : ℝ) + C0 * secondOrderScale n)

/-- The literal small-`o` formulation of the paper's main asymptotic. -/
def MainAsymptotic : Prop :=
  mainError =o[atTop] secondOrderScale

/-- The exact rational complement quotient `M! / (n!)²`. -/
def complementQuotient (n M : ℕ) : ℚ :=
  (M.factorial : ℚ) / (n.factorial : ℚ) ^ 2

/-- A subset of `(n,M]` whose product is the complement quotient. -/
def HasComplementProduct (n M : ℕ) : Prop :=
  ∃ selected : Finset ℕ,
    selected ⊆ factorInterval n M ∧
      ((selected.prod id : ℕ) : ℚ) = complementQuotient n M

end

end Erdos390

Source

Shouqiao Wang, A Proposed Solution to Erdős Problem 390, p. 3, Section 1, Theorem 1.1: https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/390/paper.pdf. Exact formal finite model and target: https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/390/lean/Erdos390/WholePaper/Definitions.lean#L14-L81. Pinned repository snapshot: https://github.com/ShouqiaoW/erdos/tree/61325b10bbdc29f4fb5e0618b414b9f2189333ad/390.

View graph