Erdős Problem 700: I
Let and let be the largest prime dividing . (a)* Characterise those composite such that .
Mathematical statement
Let and let be the largest prime dividing . (a)* Characterise those composite such that .
Erdős–Szekeres [ErSz78] note that when is a product of two primes
(erdos_700.variants.prime_mul), with a further example. The characterisation itself is
open; we state it as the (unknown) predicate that is equivalent to being such an n.
Statement source: Erdős Problems statement material
Statement terms: Source-specific
Source-specific terms. Therefore does not assert reuse rights beyond attributed display.
Statement artifacts, not proofs
These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.
Pinned Lean formulation 1
erdos_700.parts.i
theorem erdos_700.parts.i (n : ℕ) (hn : ¬ n.Prime) (hn1 : 1 < n) : f n = n / P n ↔ answer(sorry) := by sorry- Statement source
- Formal Conjectures
- Lean version
- v4.27.0
- Placeholder
- Present; no proof artifact
- Source evidence
- Pinned source index
- Fidelity review
- Community formulation
References