Number theory

Erdős 373 - maximal solution

Hickerson conjectured the largest solution the equation n!=a_1!a_2!···a_k!, with n−1 > a_1 ≥ a_2 ≥ ··· ≥ a_k, is 16!=14!5!2!.

References

erdosproblems.com/373

No one has attempted this yet.

Formal statement

Lean type

(16, [14, 5, 2]) ∈ Erdos373.S ∧ ∀ s ∈ Erdos373.S, s.1 ≤ 16

What you must prove

import FormalConjectures.ErdosProblems.«373»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos373.erdos_373.variants.maximal_solution" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/373.lean

Source type SHA-256: sha256:24d8815c2d3cdfaca28adabc9026afd5908201fdfe41c6ca3c51e408b42cde9f
Task id: fc-379fc029-variants-maximal-solution-87d7b221f6-formalized-v1
Task commitment: sha256:03057805ef6d33de5d47fa769b7a8e04d8b4ea32715cff5e1126edc41605783b

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.