Book IX · Proposition 36

IX.36

If as many numbers as we please beginning from an unit be set out continuously in double proportion, until the sum of all becomes prime, and if the sum multiplied into the last make some number, the product will be perfect.Heath, 1908

Euclid pairs perfect numbers with Mersenne primes. Euler later proved the converse for even numbers; whether an odd perfect number exists is still open, which makes this the oldest unsolved problem in mathematics.

Every step, checked

• the sum of the doubling series is primegiven
• the doubling series sums to the stated totalby IX.35
• the product of the sum and the last term is perfectby IX.36
• it equals the sum of its own proper partsby Def.VII.22

What it needs, and what needs it

Needs: IX.35

Rests on: Def.VII.20, Def.VII.22

Depth: 1 steps of argument above the first principles. Parallel postulate: not needed.

What it takes on trust

Nothing. It draws no intersections and reads nothing off the picture.

The proposition as code

@proposition(
    "IX.36",
    THEOREM,
    sample=_mersenne_exponent,
    note="Euclid pairs perfect numbers with Mersenne primes. Euler later proved the "
    "converse for even numbers; whether an odd perfect number exists is still open, "
    "which makes this the oldest unsolved problem in mathematics.",
)
def prop_IX_36(exponent: int) -> Out:
    total = 2**exponent - 1
    hypothesis("the sum of the doubling series is prime", is_prime(total))
    candidate = total * 2 ** (exponent - 1)

    because(prop_IX_35, 2, exponent) if exponent >= 3 else None

    claim("the doubling series sums to the stated total", "IX.35",
          sum(2**k for k in range(exponent)) == total)
    claim("the product of the sum and the last term is perfect", "IX.36",
          is_perfect(candidate))
    claim("it equals the sum of its own proper parts", "Def.VII.22",
          sum(proper_divisors(candidate)) == candidate)
    return Out(perfect=candidate, mersenne=total)