Prove2Me

Lemma 1.2 — Complement formulation

Proved
Erdos390.complement_formulation

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

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.

View graph