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$?

_Note: This problem does not yet have a formalized solution on [Compfiles](https://dwrensha.github.io/compfiles/). If you solve it, consider contributing your solution there._

Replace sorry in the template below with your solution. See Answer Bank for acceptible answer declarations. Mathlib version used by the checker is v4.34.0.

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