FC100SolvedSet1

A random subset of 100 non-open problems, drawn uniformly at random from all problems without the category research open tag (solved, test, API, etc.).

Quoted from FormalConjectures/Subsets/FC100SolvedSet1.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0.

The 100 statements the list names, numbered as it lists them, 94 of them linked to their problem's article; the 6 others, without an article here, are listed at the end.

Entries 2 to 22

• 2. WrittenOnTheWallII.GraphConjecture13.conjecture13 (research solved), in Written on the Wall II - Conjecture 13
• 3. OpenQuantumProblem35.ame_3_exists (research solved), in Open Quantum Problem 35: existence of absolutely maximally entangled pure states
• 4. LychrelNumbers.eventually_palindrome_base10 (API), in Lychrel numbers in base 10
• 5. Erdos42.example_maximal_sidon (textbook), in Erdős Problem 42: Maximal Sidon Sets and Disjoint Difference Sets
• 6. Mathoverflow75792.Reachable.complexity (test), in Mathoverflow 75792
• 7. OeisA280831.a_0 (test), in The 1680-Conjecture
• 8. Erdos141.first_three_odd_primes (test), in Erdős Problem 141
• 9. WrittenOnTheWallII.GraphConjecture33.conjecture33 (research solved), in Written on the Wall II - Conjecture 33
• 10. MonochromaticQuantumGraph.eqSystem4_has_solution_d2 (test), in Monochromatic quantum graphs (inherited vertex colorings)
• 11. OeisA228828.a_2 (test), in Numbers \(n\) such that \(n^2 + \pi(n)\) is prime
• 12. Erdos399.erdos_399.variants.cambie (research solved), in Erdős Problem 399
• 13. Erdos349.exists_t_for_k_disjoint_segments (research solved), in Erdős Problem 349
• 14. Erdos686.erdos_686.variants.four_three (research solved), in Erdős Problem 686
• 15. OpenQuantumProblem23.hasConstantOverlapSq_singleton (test), in Open Quantum Problem 23: SIC-POVMs
• 17. Erdos678.lcmInterval_lt_example3 (test), in Erdős Problem 678
• 18. Gourevitch.gourevitch_series_identity (research solved), in Gourevitch's series identity
• 19. WrittenOnTheWallII.GraphConjecture16.conjecture16 (research solved), in Written on the Wall II - Conjecture 16
• 20. Erdos12.erdos_12.variants.erdos_sarkozy (research solved), in Erdős Problem 12
• 21. Mahler32.mahler_conjecture.variants.consequence (textbook), in Mahler's 3/2 Problem
• 22. DegreeSequencesTriangleFree.lemma2_d (API), in Degree sequences in triangle-free graphs

Entries 23 to 43

• 23. Kaplansky.UnitConjecture.counterexamples.ii (research solved), in Kaplansky's Conjectures
• 24. Erdos697.erdos_697.parts.i (research solved), in Erdős Problem 697
• 25. Erdos61.erdos_61.variants.bnss23 (research solved), in Erdős Problem 61 -- Erdős–Hajnal Conjecture
• 26. Erdos968.erdos_968.variants.sum_abs_diff_isTheta_log_sq (research solved), in Erdős Problem 968
• 27. RamanujanTau.ramanujan_petersson (research solved), in Ramanujan τ-function
• 28. Green14.green_14_quadratic (research solved), in Ben Green's Open Problem 14
• 29. Erdos1063.erdos_1063.variants.cambie_upper_bound (research solved), in Erdős Problem 1063
• 31. Erdos697.density_exists (research solved), in Erdős Problem 697
• 32. Green14.W_3_15 (research solved), in Ben Green's Open Problem 14
• 33. OpenQuantumProblem35.ame_2_exists (research solved), in Open Quantum Problem 35: existence of absolutely maximally entangled pure states
• 34. Erdos392.erdos_392.variants.implication (research solved), in Erdős Problem 392
• 35. Erdos886.erdos_886.variants.rosenfeld_infinite (research solved), in Erdős Problem 886
• 36. OpenQuantumProblem23.qubitSICFamily_pairwise (test), in Open Quantum Problem 23: SIC-POVMs
• 37. Erdos835.johnsonGraph_18_9_chromaticNumber (research solved), in Erdős Problem 835
• 38. OeisA56777.a_65 (test), in Divisibility of \(2^n + 1\) by \(n\)
• 39. Erdos41.erdos_41.variants.pairwise (research solved), in Erdős Problem 41
• 40. OeisA232174.a_2 (test), in Representations with prime conditions
• 41. Erdos350.distinctSubsetSums_1_2 (test), in Erdős Problem 350
• 42. Arxiv.«2602.05192».finiteAdditiveConvolution_monic' (test), in First Proof, Theorem 4
• 43. Erdos295.erdos_295.variants.erdos_straus (research solved), in Erdős Problem 295

Entries 44 to 63

• 44. Erdos36.M_four (test), in Erdős Problem 36
• 45. Erdos590.erdos_590 (research solved), in Erdős Problem 590
• 46. Arxiv.«1308.0994».KTExtendsK (API), in Boxdot Conjecture
• 47. Erdos198.erdos_198.variants.concrete (research solved), in Erdős Problem 198
• 48. Erdos513.erdos_513.variants.lower_bound (research solved), in Erdős Problem 513
• 49. Erdos198.baumgartner_strong (research solved), in Erdős Problem 198
• 50. Erdos617.erdos_617.variants.r_eq_4 (research solved), in Erdős Problem 617
• 51. Erdos1038.erdos_1038.parts.ii (research solved), in Erdős Problem 1038
• 52. OeisA231201.a_8 (test), in Sum of two numbers with prime conditions
• 53. Erdos56.maxWeaklyDivisible_one (test), in Erdős Problem 56
• 54. Erdos17.isClusterPrime_97_isLeast_non_cluster (test), in Erdős Problem 17
• 55. BealConjecture.flt_of_beal_conjecture (textbook), in Beal conjecture
• 56. Arxiv.«1609.08688».maximalLength_ge_of_isSquare (research solved), in The length of an \(s\)-increasing sequence of \(r\)-tuples
• 57. RiemannZetaValues.infinite_irrational_at_odd (research solved), in Particular values of the Riemann zeta function
• 58. AgohGiuga.isWeakGiuga_iff_sum_primeFactors (research solved), in Agoh-Giuga conjecture
• 59. OeisA6697.count_false_morphism (API), in Subword complexity of the morphism a → aab, b → b
• 60. Mathoverflow10799.μ_half_eq_uniform (test), in Optimal monotone families for the discrete isoperimetric inequality
• 61. OeisA67720.a_6 (test), in Conjectures associated with A067720
• 62. OpenQuantumProblem13.Qubit.star_smul_mul_smul (API), in Open Quantum Problem 13: Mutually unbiased bases
• 63. Erdos920.erdos_920.variants.k_eq_3 (research solved), in Erdős Problem 920

Entries 64 to 84

• 64. Erdos26.erdos_26.variants.rusza (research solved), in Erdős Problem 26
• 65. InverseGalois.inverse_galois_problem.variants.symmetric_group (research solved), in Inverse Galois problem
• 66. Erdos1067.erdos_1067.variants.infinite_edge_connectivity (research solved), in Erdős Problem 1067
• 67. Erdos1074.erdos_1074.variants.EHSNumbers_init (test), in Erdős Problem 1074
• 68. Erdos26.not_isThick_of_finite (test), in Erdős Problem 26
• 69. Erdos50.erdos_50_schoenberg (research solved), in Erdős Problem 50
• 70. Erdos951.erdos_951.variants.isBeurlingPrimes (API), in Erdős Problem 951
• 71. Erdos965.erdos_965.variants.generalization (research solved), in Erdős Problem 965
• 72. Erdos985.erdos_985.variants.two_three_five_primitive_root (research solved), in Erdős Problem 985
• 73. PellNumbers.pellNumber_two (test), in Infinitude of Pell number primes
• 75. BusyBeaver.sanity_check (API), in Busy Beaver
• 76. OpenQuantumProblem13.Qubit.firstCol_normSq (API), in Open Quantum Problem 13: Mutually unbiased bases
• 77. Erdos263.erdos_263.variants.sub_doubly_exponential (research solved), in Erdős Problem 263
• 78. Arxiv.«1609.08688».tripleProduct_const (API), in The length of an \(s\)-increasing sequence of \(r\)-tuples
• 79. Erdos317.erdos_317.variants.counterexample (textbook), in Erdős Problem 317
• 80. OpenQuantumProblem23.sicOverlapSq_three (test), in Open Quantum Problem 23: SIC-POVMs
• 81. Erdos442.erdos_442.variants.tao (research solved), in Erdős Problem 442
• 82. AgohGiuga.korselts_criterion (textbook), in Agoh-Giuga conjecture
• 83. Erdos1054.f_undefined_at_2 (textbook), in Erdős Problem 1054
• 84. Erdos503.erdos_503.variants.R3 (research solved), in Erdős Problem 503

Entries 85 to 100

• 85. OeisA63880.a_of_primitive_mul_squarefree (textbook), in Conjectures associated with A063880
• 86. Erdos1142.erdos_1142.variants.mientka_weitzenkamp (research solved), in Erdős Problem 1142
• 87. CongruentNumber.congruentNumber_7 (test), in Congruent Number
• 90. Erdos590.erdos_590.variants.ge_three_false (research solved), in Erdős Problem 590
• 91. Erdos494.erdos_494.variants.product (research solved), in Erdős Problem 494
• 92. Green29.green_29.variant (research solved), in Ben Green's Open Problem 29
• 93. Erdos865.erdos_865.variants.k2 (research solved), in Erdős Problem 865
• 94. Hadamard.HadamardConjecture.variants.first_cases (research solved), in Hadamard's conjecture
• 95. Mathoverflow10799.boundaryCount_univ (test), in Optimal monotone families for the discrete isoperimetric inequality
• 96. Erdos457.erdos_457 (research solved), in Erdős Problem 457
• 97. OpenQuantumProblem23.bb84Family_not_isSICFamily (test), in Open Quantum Problem 23: SIC-POVMs
• 98. Green32.hasGap_empty (test), in Green's Open Problem 32
• 99. Erdos1052.isUnitaryPerfect_60 (test), in Erdős Problem 1052
• 100. OeisA67720.a_1 (test), in Conjectures associated with A067720

Without an article here: 1. WrittenOnTheWallII.Test.petersen_size (test, in FormalConjectures/WrittenOnTheWallII/Test.lean), 16. WrittenOnTheWallII.Test.house_radius (test, in FormalConjectures/WrittenOnTheWallII/Test.lean), 30. WrittenOnTheWallII.Test.petersen_residue (test, in FormalConjectures/WrittenOnTheWallII/Test.lean), 74. WrittenOnTheWallII.Test.C6_size (test, in FormalConjectures/WrittenOnTheWallII/Test.lean), 88. WrittenOnTheWallII.Test.petersen_szeged (test, in FormalConjectures/WrittenOnTheWallII/Test.lean), 89. WrittenOnTheWallII.Test.petersen_radius (test, in FormalConjectures/WrittenOnTheWallII/Test.lean).

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.