Easy formalization targets

The "solved" ones may be more appropriate for direct PR to Mathlib, if they are not related to an unsolved conjecture.

Feel free to suggest additional targets.

#### Number Theory
- [x] [existence of an odd perfect number](https://en.wikipedia.org/wiki/Perfect_number#Odd_perfect_numbers) (WIP: #122)
- [ ] [existence of infinitely many Mersenne primes](https://en.wikipedia.org/wiki/Mersenne_conjectures#Lenstra%E2%80%93Pomerance%E2%80%93Wagstaff_conjecture): #134
- [x] conjectures on Fermat primes from Wikipedia: #135
- [ ] [infinitude of primes of the form $x^2+1$](https://mathoverflow.net/questions/151159/status-of-the-x2-1-problem)
- [x] [Schinzel's hypothesis H](https://en.wikipedia.org/wiki/Schinzel's_hypothesis_H) (a generalization of the [twin prime conjecture](https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/LandauProblems/TwinPrimes.lean) and the first [Hardy–Littlewood conjecture](https://github.com/google-deepmind/formal-conjectures/blob/3091da8029c4b2bbe585ffb37f109d67a8913187/FormalConjectures/Wikipedia/HardyLittlewood.lean)): #136
- [ ] [Catalan's conjecture](https://en.wikipedia.org/wiki/Catalan%27s_conjecture) (solved)
- [ ] [Fermat–Catalan conjecture](https://en.wikipedia.org/wiki/Fermat%E2%80%93Catalan_conjecture) (generalization of Catalan's and FLT)
- [ ] [Euler's sum of powers conjecture](https://en.wikipedia.org/wiki/Euler%27s_sum_of_powers_conjecture) (unknown for k ≥ 6, disproved for k = 4, 5)
- [x] [Beal conjecture](https://github.com/google-deepmind/formal-conjectures/blob/cd787dbe6edd33b8eb1045c20bf2bd38bc1d0416/FormalConjectures/Wikipedia/BealConjecture.lean)
- [x] [abc conjecture](https://github.com/google-deepmind/formal-conjectures/blob/491083e7b95a7c61d16d56144d5f5579f9c2d68b/FormalConjectures/Wikipedia/ABC.lean)
- [x] [Ramanujan–Petersson conjecture](https://en.wikipedia.org/wiki/Ramanujan%E2%80%93Petersson_conjecture) (solved): #119
- [ ] [Kummer–Vandiver conjecture](https://en.wikipedia.org/wiki/Kummer%E2%80%93Vandiver_conjecture): #137, #297
- [x] [Congruent number problem](https://en.wikipedia.org/wiki/Congruent_number#Congruent_number_problem) ([solved](https://en.wikipedia.org/wiki/Tunnell%27s_theorem) conditional on BSD): #316, #317
- [ ] [Lander, Parkin, and Selfridge conjecture](https://en.wikipedia.org/wiki/Lander,_Parkin,_and_Selfridge_conjecture#Conjecture)
- [ ] [smallest Salem number](https://en.wikipedia.org/wiki/Salem_number#Relation_with_Pisot%E2%80%93Vijayaraghavan_numbers) (could be added to the same file as #97), [Pisot–Vijayaraghavan problem](https://en.wikipedia.org/wiki/Pisot%E2%80%93Vijayaraghavan_number#Diophantine_properties) and that [the union of Salem and Pisot numbers is closed](https://en.wikipedia.org/wiki/Pisot%E2%80%93Vijayaraghavan_number#Topological_properties), [Schinzel-Zassenhaus conjecture](https://link.springer.com/chapter/10.1007/978-3-030-80031-4_4) (solved)
- [ ] [existence of infinitely many real quadratic fields of class number one](https://en.wikipedia.org/wiki/Class_number_problem#Real_quadratic_fields): #243, #244
- [ ] [Artin's conjecture on primitive roots](https://en.wikipedia.org/wiki/Artin%27s_conjecture_on_primitive_roots)

#### Analytic number theory
- [ ] [Lindelöf hypothesis](https://en.wikipedia.org/wiki/Lindel%C3%B6f_hypothesis) (weaker than RH)
- [ ] equivalent forms of RH: [growth of arithmetic functions](https://en.wikipedia.org/wiki/Riemann_hypothesis#Growth_of_arithmetic_functions), [analytic criteria](https://en.wikipedia.org/wiki/Riemann_hypothesis#Analytic_criteria_equivalent_to_the_Riemann_hypothesis), [Jensen-Pólya Program](https://arxiv.org/abs/1910.01227), [Li's criterion](https://en.wikipedia.org/wiki/Li%27s_criterion)
- [ ] [generalized Riemann hypothesis](https://en.wikipedia.org/wiki/Generalized_Riemann_hypothesis) ([DirichletCharacter.LFunction](https://leanprover-community.github.io/mathlib4_docs/Mathlib/NumberTheory/LSeries/DirichletContinuation.html#DirichletCharacter.LFunction)), [extended Riemann hypothesis](https://en.wikipedia.org/wiki/Extended_Riemann_hypothesis) ([NumberField.dedekindZeta](https://leanprover-community.github.io/mathlib4_docs/Mathlib/NumberTheory/NumberField/DedekindZeta.html#NumberField.dedekindZeta)) (follow [RiemannHypothesis](https://leanprover-community.github.io/mathlib4_docs/Mathlib/NumberTheory/LSeries/RiemannZeta.html#RiemannHypothesis)), see also (not easy) [Selberg's 1/4 conjecture](https://mathoverflow.net/a/247020)
- [ ] [Dedekind's conjecture](https://en.wikipedia.org/wiki/Artin_L-function#The_Dedekind_conjecture) (Artin's is not easy, need analytic continuation)
- [ ] [non-existence of a Siegel zero](https://en.wikipedia.org/wiki/Siegel_zero#Defining_%22Siegel_zeros%22)
- [ ] [Montgomery's pair correlation conjecture](https://en.wikipedia.org/wiki/Montgomery%27s_pair_correlation_conjecture)
- [ ] [moment bounds for Riemann zeta](https://arxiv.org/abs/math/0612106)
- [ ] [Elliott–Halberstam conjecture](https://en.wikipedia.org/wiki/Elliott%E2%80%93Halberstam_conjecture)
- [ ] [Chowla conjecture and Sarnak conjecture](https://terrytao.wordpress.com/2012/10/14/the-chowla-conjecture-and-the-sarnak-conjecture/)
- [ ] [Siegel's conjecture](https://en.wikipedia.org/wiki/Regular_prime#Siegel's_conjecture) (infinitude/density of regular/irregular primes): #246, #248
- [ ] there are infinitely many irregular pairs (p, p − n) for every natural number n ≥ 2
- [ ] [Vinogradov's mean-value theorem](https://en.wikipedia.org/wiki/Vinogradov%27s_mean-value_theorem) (solved)
- [ ] [Cramer's conjecture](https://en.wikipedia.org/wiki/Cram%C3%A9r%27s_conjecture) (stronger than Legendre's and Andrica's; Oppermann's also in the PRs) ([related conjectures](https://en.wikipedia.org/wiki/Cram%C3%A9r%27s_conjecture#Related_conjectures_and_heuristics))
- [x] [Firoozbakht's conjecture](https://en.wikipedia.org/wiki/Firoozbakht%27s_conjecture): #170, #234 ("implies a strong form of Cramér's conjecture and is hence inconsistent with the heuristics of Granville and Pintz and of Maier")

#### Diophantine approximation
- [ ] [Duffin-Schaeffer conjecture / Koukoulopoulos–Maynard theorem](https://en.wikipedia.org/wiki/Duffin%E2%80%93Schaeffer_theorem) (solved)
- [ ] [Oppenheim conjecture](https://en.wikipedia.org/wiki/Oppenheim_conjecture) (solved)
- [ ] [Serge Lang's strengthening of Roth's theorem](https://en.wikipedia.org/wiki/Roth%27s_theorem#Discussion)

#### Transcendence theory
- [ ] [Gelfond–Schneider theorem](https://en.wikipedia.org/wiki/Gelfond%E2%80%93Schneider_theorem) (solved)
- [ ] [Baker's theorem](https://en.wikipedia.org/wiki/Baker%27s_theorem) (solved)
- [x] [Schanuel's conjecture](https://github.com/google-deepmind/formal-conjectures/blob/cd787dbe6edd33b8eb1045c20bf2bd38bc1d0416/FormalConjectures/Wikipedia/SchanuelsConjecture.lean) (TODO: switch to [Algebra.trdeg](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/AlgebraicIndependent/Basic.html#Algebra.trdeg))

#### Arithmetic geometry
- [ ] [Mordell conjecture](https://en.wikipedia.org/wiki/Faltings%27s_theorem) (solved, awaiting definition of genus, see [Zulip](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/.28Nice.29.20algebraic.20curves/near/521186454))

#### Algebra
- [x] [Casas-Alvero conjecture](https://mathoverflow.net/questions/27851/polynomials-having-a-common-root-with-their-derivatives): #149
- [x] [Jacobian conjecture](https://github.com/google-deepmind/formal-conjectures/blob/cd787dbe6edd33b8eb1045c20bf2bd38bc1d0416/FormalConjectures/Wikipedia/JacobianConjecture.lean)
- [x] [Kaplansky's conjectures](https://en.wikipedia.org/wiki/Kaplansky%27s_conjectures) (unit conjecture solved): #116, #117
- [ ] [Herzog–Schönheim conjecture](https://en.wikipedia.org/wiki/Herzog%E2%80%93Sch%C3%B6nheim_conjecture)

#### Graph theory
- [ ] [Ringel–Kotzig conjecture](https://en.wikipedia.org/wiki/Graceful_labeling) (all trees admit graceful labellings)
- [ ] [Kotzig's conjecture](https://en.wikipedia.org/wiki/Kotzig%27s_conjecture)
- [ ] [Lovász conjecture](https://en.wikipedia.org/wiki/Lov%C3%A1sz_conjecture)
- [ ] [existence of a Moore graph with girth 5 and degree 57](https://en.wikipedia.org/wiki/Moore_graph#Examples)
- [x] [Conway's 99-graph problem](https://github.com/google-deepmind/formal-conjectures/blob/c32e689d7d7ed23abba50c90bc91bea13d5450b5/FormalConjectures/Wikipedia/Conway99Graph.lean#L4)
- [ ] [Oberwolfach problem](https://en.wikipedia.org/wiki/Oberwolfach_problem), [Alspach's conjecture](https://en.wikipedia.org/wiki/Alspach%27s_conjecture)

#### Combinatorics
- [ ] [Erdős conjecture on arithmetic progressions](https://en.wikipedia.org/wiki/Erd%C5%91s_conjecture_on_arithmetic_progressions) (Erdős#3)
- [ ] [Erdős–Turán conjecture on additive bases](https://en.wikipedia.org/wiki/Erd%C5%91s%E2%80%93Tur%C3%A1n_conjecture_on_additive_bases)
- [ ] [Sunflower conjecture](https://en.wikipedia.org/wiki/Sunflower_(mathematics)#Sunflower_lemma_and_conjecture) (Erdős#20)
- [x] [1/3-2/3 conjecture](https://github.com/google-deepmind/formal-conjectures/blob/c32e689d7d7ed23abba50c90bc91bea13d5450b5/FormalConjectures/Wikipedia/conjecture_1_3_to_2_3.lean)
- [ ] [non-existence of finite projective planes of order other than prime powers, e.g. 10 or 12](https://en.wikipedia.org/wiki/Bruck%E2%80%93Ryser%E2%80%93Chowla_theorem#Projective_planes), see also [complete MOLS](https://en.wikipedia.org/wiki/Mutually_orthogonal_Latin_squares#Projective_planes)
- [ ] [No-three-in-line problem](https://en.wikipedia.org/wiki/No-three-in-line_problem)

#### Complex analysis
- [ ] [Bieberbach conjecture](https://en.wikipedia.org/wiki/De_Branges%27s_theorem) (solved)
- [ ] [unbounded denominators conjecture](https://arxiv.org/pdf/2109.09040) (solved)

#### Functional analysis
- [ ] [Invariant subspace problem](https://en.wikipedia.org/wiki/Invariant_subspace_problem) (open for separable Hilbert space, many recent claims): #530, #531

#### Geometry
- [ ] [Inscribed square problem](https://en.wikipedia.org/wiki/Inscribed_square_problem): #239, #451
- [ ] [Erdős–Ulam problem](https://en.wikipedia.org/wiki/Erd%C5%91s%E2%80%93Ulam_problem)
- [ ] [Harborth's conjecture](https://en.wikipedia.org/wiki/Harborth%27s_conjecture)
- [ ] [Hadwiger–Nelson problem](https://en.wikipedia.org/wiki/Hadwiger%E2%80%93Nelson_problem): #314, #315
- [ ] [Fuglede's conjecture](https://en.wikipedia.org/wiki/Fuglede%27s_conjecture) (also analysis)
- [ ] [period tiling conjecture](https://terrytao.wordpress.com/2022/09/19/a-counterexample-to-the-periodic-tiling-conjecture/) (disproved)
- [ ] [Conway's "dead fly problem"](https://oeis.org/A248380/a248380.pdf) (minimal spacing of [Danzer set](https://en.wikipedia.org/wiki/Danzer_set#Separation))