Conjectures.io

Number theory

Erdős 375

Is Erdos375Prop true?

References

  • [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).
  • [RST75] Ramachandra, K. and Shorey, T. N. and Tijdeman, R., On Grimm's problem relating to factorisation of a block of consecutive integers. J. Reine Angew. Math. (1975), 109-124. -

No one has attempted this yet.

Formal statement

Lean type

True ↔ Erdos375.Erdos375Prop

What you must prove

import FormalConjectures.ErdosProblems.«375»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos375.erdos_375" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/375.lean

Source type SHA-256
sha256:c68070ef89ab41b0cf1db676d028ce79f2e37a1a7caeaa31ee75d2908a161610
Task id
fc-379fc029-erdos375-erdos-375-3a3273c85d-formalized-v1
Task commitment
sha256:6be5612381b7d1de04296ce7f8a1efc985741199a6e74ac1ee7f3e422e5af39f

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.