Number theory

Erdős 373 - suranyi

Surányi was the first to conjecture that the only non-trivial solution to a!b!=n! is 6!7!=10!.

References

erdosproblems.com/373

No one has attempted this yet.

Formal statement

Lean type

{(n, a, b) | n.factorial = a.factorial * b.factorial ∧ 1 < n ∧ 1 < a ∧ 1 < b ∧ b ≤ a ∧ a + 1 ≠ n} = {(10, 7, 6)}

What you must prove

import FormalConjectures.ErdosProblems.«373»
import TaskSupport

namespace Bounty

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

end Bounty

Pinned source: FormalConjectures/ErdosProblems/373.lean

Source type SHA-256: sha256:4391b6fe2419b3ff7ca82e28d5d5c31fcd5f570506ae383d34ca0b5ed80b1d46
Task id: fc-379fc029-variants-suranyi-78fbd07968-formalized-v1
Task commitment: sha256:58ce42373ae21e9b88ed491a417cc0d43535ed4f7484590e0a91d9cb5d8a6df1

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.