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

Definition

erdos390_problem

by ShouqiaoWang · Jul 31, 2026 · Mathlib c5ea003 (Lean v4.30.0)

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.

Read-back

What the Lean code literally says, in plain math · gpt-5.6-sol

For all natural numbers $n,M$ , $\operatorname{factorInterval}(n,M)$ is the finite set $\{k\in\mathbb N\mid n<k\le M\}$ ; it is empty when $M\le n$ . The predicate $\operatorname{IsAdmissibleEndpoint}(n,M)$ means that there exists a finite set $A\subseteq\mathbb N$ , whose elements are necessarily distinct, such that every $a\in A$ satisfies $n<a\le M$ and, in the natural numbers, $\prod_{a\in A}a=n!$ . The empty set is allowed, with product $1$ . Consequently, when $M\le n$ , this predicate holds exactly when $n!=1$ , namely when $n=0$ or $n=1$ . The file also asserts that for every natural number $n$ satisfying $3\le n$ , there exists at least one natural number $M$ for which $\operatorname{IsAdmissibleEndpoint}(n,M)$ holds. The function $f:\mathbb N\to\mathbb N$ has value $0$ at $n=0,1,2$ ; for $n\ge3$ , $f(n)$ is the least natural number $M$ satisfying the existence condition above. The constant $C_0$ is the real number $\frac{4029639598}{25970038185}$ , whose denominator is nonzero. Define $s(n)=\frac{n}{\log n}$ , with $n$ first embedded into the real numbers. Here the real logarithm and real division are totalized: in particular, $\log0=\log1=0$ and $x/0=0$ , so $s(0)=s(1)=0$ , while for $n\ge2$ this is the usual positive real quotient. Define $e(n)=f(n)-\left(2n+C_0s(n)\right)$ , with all terms interpreted in the real numbers. The boundary definitions give $e(0)=0$ , $e(1)=-2$ , and $e(2)=-\left(4+C_0\frac2{\log2}\right)$ . The proposition $\operatorname{MainAsymptotic}$ means that $e=o(s)$ along the natural numbers tending to infinity; expanded, this says that for every real number $\delta>0$ , there exists $N\in\mathbb N$ such that every $n\ge N$ satisfies $\lvert e(n)\rvert\le\delta\lvert s(n)\rvert$ . Finally, $\operatorname{complementQuotient}(n,M)$ is the rational number $\frac{M!}{(n!)^2}$ . Although rational division is totalized, $n!\ne0$ , including $0!=1$ , so the denominator here is always nonzero. The predicate $\operatorname{HasComplementProduct}(n,M)$ means that there exists a finite set $B\subseteq\{k\in\mathbb N\mid n<k\le M\}$ such that the natural-number product $\prod_{b\in B}b$ , after embedding into the rationals, is exactly $\frac{M!}{(n!)^2}$ . Again, the empty set is allowed and has product $1$ . This definition itself does not require $n<M$ , so when $M\le n$ it reduces to the equation $1=\frac{M!}{(n!)^2}$ .

Human review

Endorsed by Shuze Chen · Jul 31, 2026
Endorsed by ShouqiaoWang · Jul 31, 2026
Confirmed by the mission captain (proposal self-audit).

View graph