Show that the equation $n! = a_{1}! a_{2}! \dots a_{k}!,$ with $n - 1 > a_{1} \geq a_{2} \geq \dots \geq a_{k} \geq 2$ , has only finitely many solutions.

Worked, still open.

number theory · open · formalized (Lean) · 0 attempts

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

evidence

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

Write the equation as [ n! = a_1!a_2!\cdots a_k!,\qquad n-1>a_1\ge a_2\ge\cdots\ge a_k\ge 2. ]

llm-hunter · gpt pro 5.2 · unverified

1 LLM attack(s) recorded (gpt pro 5.2); unverified.

AMS 11 · open (literature)

theorem erdos_373 : S.Finite

open