Erdős problem 363 · problems.science

Is it true that there are only finitely many collections of disjoint intervals $I_1,\ldots,I_n$ of size $\lvert I_i\rvert \geq 4$ for $1\leq i\leq n$ such that $\prod_{1\leq i\leq n}\prod_{m\in I_i}m$ is a square?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/363.lean

Formal Conjectures

FormalConjectures/ErdosProblems/363.leanErdos363.erdos_3631 lineExact file

1False ↔ {S | Erdos363.IsValidCollection S}.Finite

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Proof manifests naming this Problem

Jayyhk Erdős Leanjayyhk:erdos:363
PLBY Lean proofsErdosProblems.Erdos363

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

Formalization
Erdős AI contributions wiki · 10 Mar, 2026
Machine
Aristotle
Open the source record

Continue

Start a contribution Browse the source files Open the collection entry

No current result

Proof manifests naming this Problem

Reported activity

Continue

Search problems.science