google-deepmind / google-deepmind/formal-conjectures
tracking problem list: Unsolved problems in number theory
- Dominant language
- Lean
- Stars
- 1.3k
- Forks
- 485
- Avg merge
- 1d 20h
- Merged PRs (30d)
- 328
Description
I manually checked all the links from [unsolved problems list](https://en.wikipedia.org/wiki/Category:Unsolved_problems_in_number_theory). Below are only those that are not in the repository yet.
- [ ] [Pollock's conjectures](https://en.wikipedia.org/wiki/Pollock's_conjectures)
- [ ] [Woodall primes](https://en.wikipedia.org/wiki/Woodall_primes)
- [ ] [Riesel primes](https://en.wikipedia.org/wiki/Riesel_primes)
- [ ] [Sierpiński problem](https://en.wikipedia.org/wiki/Sierpiński_problem)
- [ ] [Balanced prime](https://en.wikipedia.org/wiki/Balanced_prime)
- [ ] [Birch and Swinnerton-Dyer conjecture](https://en.wikipedia.org/wiki/Birch_and_Swinnerton-Dyer_conjecture)
- [ ] [Brumer–Stark conjecture](https://en.wikipedia.org/wiki/Brumer–Stark_conjecture)
- [ ] [Carmichael's totient function conjecture](https://en.wikipedia.org/wiki/Carmichael's_totient_function_conjecture)
- [ ] [Class number problem](https://en.wikipedia.org/wiki/Class_number_problem)
- [ ] [https://en.wikipedia.org/wiki/Covering_system#Boundedness_of_the_smallest_modulus_[solved]](https://en.wikipedia.org/wiki/Covering_system)
- [ ] [https://en.wikipedia.org/wiki/Covering_system#Systems_of_odd_moduli](https://en.wikipedia.org/wiki/Covering_system)
- [ ] [Cuboid conjectures](https://en.wikipedia.org/wiki/Cuboid_conjectures)
- [ ] [Cullen number (Proth prime)](https://en.wikipedia.org/wiki/Cullen_number_(Proth_prime))
- [ ] [Divisor summatory function](https://en.wikipedia.org/wiki/Divisor_summatory_function)
- [ ] [https://en.wikipedia.org/wiki/Double_Mersenne_number#Double_Mersenne_primes](https://en.wikipedia.org/wiki/Double_Mersenne_number)
- [ ] [https://en.wikipedia.org/wiki/Double_Mersenne_number#Catalan–Mersenne_number_conjecture](https://en.wikipedia.org/wiki/Double_Mersenne_number)
- [ ] [Elliott–Halberstam conjecture](https://en.wikipedia.org/wiki/Elliott–Halberstam_conjecture)
- [ ] [Erdős–Moser equation](https://en.wikipedia.org/wiki/Erdős–Moser_equation)
- [ ] [Erdős–Straus conjecture](https://en.wikipedia.org/wiki/Erdős–Straus_conjecture)
- [ ] [Erdős–Turán conjecture on additive bases](https://en.wikipedia.org/wiki/Erdős–Turán_conjecture_on_additive_bases) ?hard
- [ ] [Erdős–Ulam problem](https://en.wikipedia.org/wiki/Erdős–Ulam_problem)
- [x] [Euclid number](https://en.wikipedia.org/wiki/Euclid_number) #1122
- [ ] [Euclid–Mullin sequence](https://en.wikipedia.org/wiki/Euclid–Mullin_sequence)
- [ ] [Feit–Thompson conjecture](https://en.wikipedia.org/wiki/Feit–Thompson_conjecture) #625, and the same in The Kourovka Notebook
- [ ] [Friendly number](https://en.wikipedia.org/wiki/Friendly_number)
- [ ] [Square-difference-free set](https://en.wikipedia.org/wiki/Square-difference-free_set)
- [ ] [Gillies' conjecture](https://en.wikipedia.org/wiki/Gillies'_conjecture)
- [x] [Giuga number](https://en.wikipedia.org/wiki/Giuga_number)
- [ ] [Goormaghtigh conjecture](https://en.wikipedia.org/wiki/Goormaghtigh_conjecture)
- [ ] [Greenberg's conjectures](https://en.wikipedia.org/wiki/Greenberg's_conjectures)
- [ ] [Grothendieck–Katz p-curvature conjecture](https://en.wikipedia.org/wiki/Grothendieck–Katz_p-curvature_conjecture) ?hard
- [ ] [Hermite's problem](https://en.wikipedia.org/wiki/Hermite's_problem)
- [ ] [Hilbert's ninth problem](https://en.wikipedia.org/wiki/Hilbert's_ninth_problem) too vague
- [ ] [Idoneal number](https://en.wikipedia.org/wiki/Idoneal_number)
- [x] [Kummer–Vandiver conjecture](https://en.wikipedia.org/wiki/Kummer–Vandiver_conjecture) #297
- [ ] [Lander, Parkin, and Selfridge conjecture](https://en.wikipedia.org/wiki/Lander,_Parkin,_and_Selfridge_conjecture)
- [ ] [Legendre's conjecture](https://en.wikipedia.org/wiki/Legendre's_conjecture)
- [ ] [Leopoldt's conjecture](https://en.wikipedia.org/wiki/Leopoldt's_conjecture) #247
- [ ] [Lindelöf hypothesis](https://en.wikipedia.org/wiki/Lindelöf_hypothesis)
- [ ] [Lychrel number](https://en.wikipedia.org/wiki/Lychrel_number)
- [ ] [Magic square of squares](https://en.wikipedia.org/wiki/Magic_square_of_squares)
- [ ] [Manin conjecture](https://en.wikipedia.org/wiki/Manin_conjecture) ?hard
- [x] [Minimum overlap problem](https://en.wikipedia.org/wiki/Minimum_overlap_problem) #215
- [ ] [Montgomery's pair correlation conjecture](https://en.wikipedia.org/wiki/Montgomery's_pair_correlation_conjecture)
- [ ] [n conjecture](https://en.wikipedia.org/wiki/n_conjecture)
- [ ] [Newman–Shanks–Williams prime](https://en.wikipedia.org/wiki/Newman–Shanks–Williams_prime)
- [ ] [Newman's conjecture](https://en.wikipedia.org/wiki/Newman's_conjecture)
- [ ] [Odd greedy expansion](https://en.wikipedia.org/wiki/Odd_greedy_expansion) too vague
- [ ] [Palindromic prime](https://en.wikipedia.org/wiki/Palindromic_prime)
- [x] [Pell number](https://en.wikipedia.org/wiki/Pell_number)
- [ ] [Perfect number](https://en.wikipedia.org/wiki/Perfect_number)
- [ ] [Prime quadruplet](https://en.wikipedia.org/wiki/Prime_quadruplet)
- [ ] [Quasiperfect number](https://en.wikipedia.org/wiki/Quasiperfect_number)
- [ ] [Amicable numbers](https://en.wikipedia.org/wiki/Amicable_numbers) A generalisation of Quasiperfect number
- [ ] [Rank of an elliptic curve](https://en.wikipedia.org/wiki/Rank_of_an_elliptic_curve#Conjectures_on_the_boundedness_of_ranks) ?hard
- [ ] [Riesel number](https://en.wikipedia.org/wiki/Riesel_number)
- [ ] [Scholz conjecture](https://en.wikipedia.org/wiki/Scholz_conjecture)
- [ ] [Serre's conjecture II](https://en.wikipedia.org/wiki/Serre's_conjecture_II) ?hard
- [ ] [Sierpiński number](https://en.wikipedia.org/wiki/Sierpiński_number)
- [ ] [Stark conjectures](https://en.wikipedia.org/wiki/Stark_conjectures) ?hard
- [ ] [Sum of four cubes problem](https://en.wikipedia.org/wiki/Sum_of_four_cubes_problem)
- [ ] [Superperfect number](https://en.wikipedia.org/wiki/Superperfect_number) More on Arxiv
- [ ] [Supersingular prime](https://en.wikipedia.org/wiki/Supersingular_prime) hard
- [ ] [Szpiro's conjecture](https://en.wikipedia.org/wiki/Szpiro's_conjecture)
- [ ] [Tate conjecture](https://en.wikipedia.org/wiki/Tate_conjecture) hard
- [ ] [Vojta's conjecture](https://en.wikipedia.org/wiki/Vojta's_conjecture) hard
- [ ] [Waring–Goldbach problem](https://en.wikipedia.org/wiki/Waring–Goldbach_problem) More on Arxiv
- [ ] [Waring's problem](https://en.wikipedia.org/wiki/Waring's_problem)
- [ ] [Wieferich prime](https://en.wikipedia.org/wiki/Wieferich_prime)
- [ ] [Wilson prime](https://en.wikipedia.org/wiki/Wilson_prime)
- [ ] [Wolstenholme prime](https://en.wikipedia.org/wiki/Wolstenholme_prime)
- [x] [Riemann hypothesis](https://en.wikipedia.org/wiki/Riemann_hypothesis) It's already in `mathlib4`!
I marked some of them as hard. I probably won't be able to formalize them, but I'll try to finish the rest by the end of October!
Contributor guide
Assessment
This issue has not been assessed yet.