Idoneal numbers completeness conjecture

An integer $D>0$ is idoneal if every integer that can be expressed in exactly one way (up to order and signs) as $x^2 + D y^2$ with gcd(x, Dy)=1 is a prime power or twice a prime power.

The Idoneal Numbers Completeness Conjecture asserts that the following list of 65 numbers is complete: 1,2,3,4,5,6,7,8,9,10,12,13,15,16,18,21,22,24,25,28,30,33,37,40,42,45,48, 57,58,60,70,72,78,85,88,93,102,105,112,120,130,133,165,168,177,190,210,232, 240,253,273,280,312,330,345,357,385,408,462,520,760,840,1320,1365,1848. References:

• Wikipedia: Idoneal number
• OEIS A000926

def Idoneal.IsIdoneal (n : ℕ) : Prop

Equivalent definition: A positive integer $n$ is idoneal if and only if it cannot be written as $ab + bc + ac$ for distinct positive integers $a, b,$ and $c$.

Equations

• Idoneal.IsIdoneal n = (0 < n ∧ ¬∃ (a : ℕ) (b : ℕ) (c : ℕ), 0 < a ∧ a < b ∧ b < c ∧ n = a * b + b * c + a * c)

def Idoneal.knownIdonealNumbers : Finset ℕ

The 65 known idoneal numbers that are conjectured to be the only idoneal numbers.

Equations

• One or more equations did not get rendered due to their size.

theorem Idoneal.knownIdonealNumbers_are_idoneal (n : ℕ) : n ∈ knownIdonealNumbers → IsIdoneal n

All 65 known idoneal numbers are indeed idoneal.

theorem Idoneal.idoneal_numbers_completeness : True ↔ ∀ (n : ℕ), IsIdoneal n → n ∈ knownIdonealNumbers

Idoneal numbers completeness conjecture.