Prove2Me

Lemma 1.2 — Complement formulation

Proved
Erdos390.complement_formulation

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

combinatoricserdos-problemsfactorialsnumber-theory

Let n,M∈Nn,M\in\mathbb N with n<Mn<M, and let I(n,M)={a∈N:n<a≤M}I(n,M)=\{a\in\mathbb N:n<a\le M\}. Then the following are equivalent:

  1. Some finite set of distinct integers from I(n,M)I(n,M) has product n!n!.
  2. Some finite set of distinct integers from I(n,M)I(n,M) has product
Q(n,M)=M!(n!)2.Q(n,M)=\frac{M!}{(n!)^2}.

This is the exact complement formulation connecting the original distinct-factor problem to the complementary product used in the paper.

Formalization Note The quotient is interpreted in Q\mathbb Q, so the statement does not use truncated natural-number division.

Preamble
import Definitions.Def_erdos390_problem
Formal statement
namespace Erdos390

/-- The complement formulation immediately following the main theorem. -/
theorem complement_formulation {n M : ℕ} (hnM : n < M) :
    IsAdmissibleEndpoint n M ↔ HasComplementProduct n M := by sorry

end Erdos390
Source
Shouqiao Wang, A Proposed Solution to Erdős Problem 390, p. 3, Section 1, Lemma 1.2 (Complement formulation), https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/390/paper.tex#L203-L237. Formal theorem: https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/390/lean/Erdos390/WholePaper/Complement.lean#L18-L108.
Read-back

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

For all natural numbers n,Mn,M, if n<Mn<M, then the following two existence statements are equivalent: first, there exists a finite set A⊆{k∈N∣n<k≤M}A\subseteq\{k\in\mathbb N\mid n<k\le M\}, with distinct elements, whose natural-number product satisfies ∏a∈Aa=n!\prod_{a\in A}a=n!; second, there exists a finite set B⊆{k∈N∣n<k≤M}B\subseteq\{k\in\mathbb N\mid n<k\le M\}, with distinct elements, whose natural-number product, after embedding into the rationals, satisfies (∏b∈Bb:Q)=M!(n!)2\left(\prod_{b\in B}b:\mathbb Q\right)=\frac{M!}{(n!)^2}. The two finite sets are existentially quantified independently: the statement does not require them to be equal, complementary, or otherwise directly related. Either set may be empty, and an empty product is 11. The hypothesis requires only n<Mn<M, not n≥3n\ge3, so it includes the boundary case n=0n=0 and the convention 0!=10!=1. Rational division is totalized, but (n!)2≠0(n!)^2\ne0, so this quotient has a nonzero denominator.

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