I. IMO 2000 Problem 5

Does there exist a positive integer $n$ such that $n$ has exactly $2000$ distinct prime divisors and $n$ divides $2 ^ n + 1$?

This problem does not have a formalized solution on Compfiles yet. If you solve it, consider contributing your solution to Compfiles.

import Mathlib.Data.Nat.PrimeFin

def answer : Prop := sorry

theorem solution : (∃ n, 0 < n ∧ n.primeFactors.card = 2000 ∧ n ∣ 2 ^ n + 1) ↔ answer := sorry

Submit Solution

Login to submit a solution.

Recent Submissions