Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-01 17:37 ddaa325e

View on Github →

feat(archive/imo): formalize IMO 1969 problem 1 (#4261) This is a formalization of the problem and solution for the first problem on the 1969 IMO: Prove that there are infinitely many natural numbers $a$ with the following property: the number $z = n^4 + a$ is not prime for any natural number $n$

Estimated changes

added theorem factorization
added theorem imo1969_q1
added theorem int_large
added theorem int_not_prime
added theorem left_factor_large
added theorem polynomial_not_prime
added theorem right_factor_large