Commit 2020-09-30 19:43 c04e3398
View on Github →feat(archive/imo): formalize IMO 1959 problem 1 (#4340) This is a formalization of the problem and solution for the first problem on the 1959 IMO: Prove that the fraction (21n+4)/(14n+3) is irreducible for every natural number n.