Properly rename Erdos Problem theorems #2414
Description
Describe the misformalization
To standardize the naming conventions of theorems, I've proposed a solution in #2407 and discussion in #2327
Suggested fix
Here is a list of theorems that may be required to be renamed:
erdos_100_guth_katz
erdos_100_kanold
erdos_100_piepmeyer
erdos_100_strong
erdos_1038.inf
erdos_1038.inf_lowerBound
erdos_1038.inf_upperBound
erdos_1038.sup
erdos_1051.rapid_growth
erdos_1056_k2
erdos_1056_k3
erdos_1060.bound_one
erdos_1060.bound_two
erdos_1062.lebensold_bounds
erdos_1062.limit_density
erdos_1062.lower_bound
erdos_1063.better_upper
erdos_1065a
erdos_1065b
erdos_1071a
erdos_1071b
erdos_1072a
erdos_1072b
erdos_1074.part8_i_i
erdos_1074.part_i_ii
erdos_1074.part_ii_i
erdos_1074.parts_ii_ii
erdos_1082a
erdos_1082b
erdos_1101.polynomial
erdos_1101.subexponential
erdos_1102.density_zero_of_P
erdos_1102.exists_sequence_with_P
erdos_1102.lower_density_Q_exists
erdos_1102.upper_density_Q
erdos_1106_k2
erdos_1108.k_th_powers
erdos_1108.powerful_numbers
erdos_1142.test_105
erdos_1142.test_15
erdos_1142.test_21
erdos_1142.test_4
erdos_1142.test_45
erdos_1142.test_7
erdos_1142.test_75
erdos_1142.test_not_106
erdos_1145_implies_erdos_28
erdos_1148.lower_bound
erdos_1150.parseval_lower_bound
erdos_137.multiple_powerful_factors
erdos_13_general
erdos_14a
erdos_14b
erdos_152.square
erdos_158.B22
erdos_158.isSidon
erdos_160.better_lower
erdos_160.better_upper
erdos_160.known_lower
erdos_160.known_upper
erdos_188.estimate
erdos_188.nonempty
erdos_198.variant_concrete
erdos_208.i
erdos_208.ii
erdos_233.variant
erdos_238.variant
erdos_23_n1
erdos_23_n1_tight
erdos_242_schinzel_generalization
erdos_28_of_erdos_40
erdos_307_coprime
erdos_307_coprime_one_notMem
erdos_313_conjecture
erdos_313_solution_42_2_3_7
erdos_313_solution_6_2_3
erdos_318.contain_single_even
erdos_318.infinite_AP
erdos_318.odd
erdos_318.posDensity
erdos_318.square_excluding_one
erdos_318.squares
erdos_318.univ
erdos_32.varaints.log_squared
erdos_329.converse_implication
erdos_329.lower_bound
erdos_329.of_sub_perfectDifferenceSet
erdos_330_statement
erdos_346.example
erdos_346.f_isAddStronglyCompleteNatSeq
erdos_346.f_isLacunary
erdos_346.f_not_isAddComplete
erdos_346.gt_goldenRatio_not_IsAddComplete
erdos_361.bigO
erdos_361.bigTheta
erdos_361.smallO
erdos_375.bounded_gap
erdos_375.le_two
erdos_375.legendre
erdos_375.log
erdos_386.variants_forall
erdos_386.variants_two
erdos_387.easy
erdos_387.schinzel
erdos_387.variant
erdos_394_factorial_gap_10
erdos_394_factorial_gap_conjecture
erdos_394_hall_bound
erdos_394_hall_conjecture
erdos_394_lower_bound
erdos_394_part_a
erdos_394_part_b
erdos_409.termination
erdos_413_bigOmega
erdos_413_bigOmega_largest_barrier_lt_100k
erdos_413_epsilon
erdos_413_hasPosDensity_barrier_expProd
erdos_417.part.a
erdos_417.part.b
erdos_41_i
erdos_42.constructive
erdos_427.of_shiu
erdos_427.shiu
erdos_44.empty_start
erdos_454.two_le_limsup
erdos_455.liminf
erdos_470.part1
erdos_470.part2
erdos_477.S_sq
erdos_477.X_pow_three
erdos_477.degree_two_dvd_condition_b_ne_zero
erdos_477.monomial
erdos_507.equivalent
erdos_507.lower
erdos_507.upper
erdos_513.lower_bound
erdos_513.sup
erdos_513.upper_bound
erdos_516.limsup_ratio_eq_one
erdos_516.limsup_ratio_eq_one_of_hasFabryGaps_ofFiniteOrder
erdos_516.limsup_ratio_eq_one_of_hasFejerGaps
erdos_517.fabry
erdos_517.fejer
erdos_567_H5
erdos_567_K33
erdos_567_Q3
erdos_680.variant
erdos_69.specialisation_of_erdos_257
erdos_697.beta_lt
erdos_697.delta_lt
erdos_697.lt_beta
erdos_707.counterexample_hall
erdos_707.counterexample_mian_chowla
erdos_707.counterexample_prime
erdos_723.eq_12
erdos_723.leq_11
erdos_723.prime_pow_is_projplane_order
erdos_727_variants.k_1
erdos_727_variants.k_1_2
erdos_727_variants.k_2
erdos_741.basis
erdos_741.density
erdos_757.lowerBound
erdos_757.upperBound
erdos_770.density
erdos_770.liminf
erdos_770.prime
erdos_770.three
erdos_848_asymptotic
erdos_853_strong
erdos_886_variants_rosenfeld_bound
erdos_886_variants_rosenfeld_infinite
erdos_887.variant_i
erdos_887.variant_ii
erdos_887.variant_iii
erdos_888_S
erdos_888_primes
erdos_944.dirac_conjecture.k_eq_four
erdos_945.equivalence
erdos_951.isBeurlingPrimes
erdos_961.erdos_upper_bound
erdos_961.jutila_ramachandra_shorey_upper_bound
erdos_961.sylvester_schur
erdos_961.sylvester_schur_1_1
erdos_961.well_defined
erdos_965.generalization
erdos_978.squarefree
erdos_978.sub_one
erdos_978.sub_one_density
erdos_978.sub_two
erdos_979_k2
erdos_979_k3
erdos_996.log2
erdos_996.log3
Choose either option
- I plan on working on this issue
- This issue is up for grabs: I would like to see this misformalization fixed by somebody else