Source labels openChecked July 26, 2026

Unique Crystal Components

If $n = ab$ is a crystal, then there are no other pairs of positive integers $c, d > 1$ , different from the couple $a, b$ , such that $n = cd$ and $B(c, d) ∈ ℕ$ , i.e., the components of the crystals are unique.

Number theory AMS 11 AMS 26

Mathematical statement

Statement source: arXiv 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

crystals_components_unique

Canonical source

Complete statement target, proof intentionally absentLean 4

theorem crystals_components_unique (n a b c d : ℕ)    (hab : IsCrystalWithComponents n a b) (hcd : IsCrystalWithComponents n c d) :    ({a, b} : Finset ℕ) = {c, d} := 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

Pinned Formal Conjectures sourceformalization arxiv/1601.03081background