FC100SolvedSet2

A curated subset of 100 hard-to-formalise solved research problems with verified formal statements (category research solved) and no existing formal proof.

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

The 100 statements the list names, numbered as it lists them, each linked to its problem's article.

Entries 1 to 20

• 1. PoincareConjecture.poincare_conjecture.variants.smooth_known_cases (research solved), in The Poincaré Conjecture
• 2. SatoTateConjecture.satoTate_conjecture (research solved), in Sato–Tate conjecture
• 3. HasseWeil.exists_hasAnalyticContinuation_rat (research solved), in The Hasse--Weil conjecture for elliptic curves
• 4. AlgebraicGeometry.resolution_of_singularities_of_topologicalKrullDim_le_three (research solved), in Resolution of singularities
• 5. RamanujanTau.ramanujan_petersson (research solved), in Ramanujan τ-function
• 6. FermatCatalanConjecture.fermat_catalan.variants.darmon_granville (research solved), in Fermat-Catalan conjecture
• 7. Hilbert5.hilbert_smith_conjecture.variants.dimension_three (research solved), in Hilbert's Fifth Problem and the Hilbert–Smith Conjecture
• 8. SmallCohenMacaulayModules.exists_isBalancedBigCohenMacaulay (research solved), in The small Cohen-Macaulay modules conjecture
• 9. EllipticCurveRank.RatEllipticCurve.goldfeld_conjecture.variants.two_le (research solved), in Some conjectures about ranks of elliptic curves over ℚ
• 10. SerreMultiplicityConjectures.intersectionMultiplicity_eq_zero_of_lt (research solved), in Serre's multiplicity conjectures
• 11. Erdos89.erdos_89.variants.n_dvd_log_n (research solved), in Erdős Problem 89
• 12. Bugeaud08.problem_10_8.variants.exceptional_set_dimH_zero (research solved), in Bugeaud Collection of Conjectures and Open Questions: \(p\)-adic Littlewood Conjecture
• 13. Bugeaud32.adamczewski_faverjon (research solved), in Bugeaud Collection of Conjectures and Open Questions: Automatic Expansions in Two Bases
• 14. ZagierMZV.zagier_upper_bound (research solved), in Zagier's Conjecture on Multiple Zeta Values
• 15. DeGiorgi.DeGiorgi_ge_nine (research solved), in De Giorgi's conjecture
• 16. Erdos325.erdos_325.variants.wooley (research solved), in Erdős Problem 325
• 17. Erdos507.erdos_507.variants.upper_cpz24 (research solved), in Erdős Problem 507
• 18. Erdos65.erdos_65.variants.liu_montgomery (research solved), in Erdős Problem 65
• 19. GromovPolynomialGrowth.GromovPolynomialGrowthTheorem (research solved), in Gromov's theorem on groups of polynomial growth
• 20. Erdos687.erdos_687.variants.fgkmt (research solved), in Erdős Problem 687

Entries 21 to 40

• 21. SymbolLengthMilnorKTheory.symbol_length_problem.variants.zero_mem_of_lt (research solved), in The symbol length of \(K^M_n(\mathbb{C}(x_1, \dots, x_m))/p\)
• 22. Erdos723.erdos_723.variants.leq_11 (research solved), in Erdős Problem 723: The prime power conjecture.
• 23. KaplanskyUInvariant.u_invariant_values.variants.two_pow_add_one (research solved), in Kaplansky's problem on the values of the \(u\)-invariant
• 24. Kourovka.«1.74».kourovka_1_74.variants.tarski_monster (research solved), in Conjecture 1.74 (Minimal topological groups)
• 25. LocalUniformization.local_uniformization_of_trdeg_le_three (research solved), in Local uniformization
• 26. TarskiExponentialFunctionProblem.isDecidable_completeTheory_realExp_of_realSchanuelConjecture (research solved), in Tarski's exponential function problem
• 27. Arxiv.«2208.14736».zariski_cancellation_problem.variants.dim_two (research solved), in Zariski Cancellation
• 28. Erdos1057.erdos_1057.variants.agp_lower_bound (research solved), in Erdős Problem 1057
• 29. Kakeya.kakeya_3d (research solved), in Kakeya problem
• 30. Erdos114.erdos_114.variants.large_n (research solved), in Erdős Problem 114
• 31. CongruentNumber.Tunnell_even (research solved), in Congruent Number
• 32. PerfectNumbers.odd_perfect_number.lower_bound (research solved), in Perfect numbers
• 33. ArtinPrimitiveRootsConjecture.conditional_artin_primitive_roots.variants.part_ii_power_squarefreePart_not_modeq_one (research solved), in Artin's conjecture on primitive roots
• 34. Erdos5.erdos_5.variants.merikoski_measure (research solved), in Erdős Problem 5
• 35. HopfAlgebraCohomology.cohomology_finite_of_isCocomm (research solved), in Finite generation of the cohomology of finite-dimensional Hopf algebras
• 36. Green9.green_9_i (research solved), in Green's Open Problem 9
• 37. Arxiv.«2001.02665».kotzig_conjecture_large (research solved), in Ringel's Conjecture and Kotzig's Conjecture for large \(n\)
• 38. Erdos940.erdos_940.variants.three_powerful (research solved), in Erdős Problem 940
• 39. ClassNumberProblem.class_number_problem.variants.imaginary (research solved), in Class number problem for real quadratic fields
• 40. ElliottHalberstamConjecture.elliott_halberstam.variants.friedlander_granville (research solved), in Elliott–Halberstam conjecture

Entries 41 to 60

• 41. Erdos813.erdos_813.variants.bucic_sudakov (research solved), in Erdős Problem 813
• 42. Mills.exists_least (research solved), in Mills' Theorem
• 43. RamseyNumbers.ramsey_number_five_five_upper_bound (research solved), in Ramsey numbers
• 44. Transcendental.transcendental_gamma_one_div_three (research solved), in Open questions on transcendence of numbers
• 45. Erdos61.erdos_61.variants.bnss23 (research solved), in Erdős Problem 61 -- Erdős–Hajnal Conjecture
• 46. Erdos985.erdos_985.variants.two_three_five_primitive_root (research solved), in Erdős Problem 985
• 47. Green41.minCopies_set_nonempty (research solved), in Ben Green's Open Problem 41
• 48. RiemannZetaMoments.moment_isEquiv₂ (research solved), in Moments of the Riemann zeta function on the critical line
• 49. Erdos604.erdos_604.variants.katz_tardos (research solved), in Erdős Problem 604
• 50. Erdos408.erdos_408.variants.ford_konyagin_luca (research solved), in Erdős Problem 408
• 51. Green4.large_green_4 (research solved), in Ben Green's Open Problem 4
• 52. InverseGalois.inverse_galois_problem.variants.complex_rational_functions (research solved), in Inverse Galois problem
• 53. Margulis.huang_shi_theorem_1_2 (research solved), in A conjecture by Margulis on matrix groups
• 54. DiophantineTuple.noIntegralDiophantineFiveTuple (research solved), in Diophantine \(m\)-tuples
• 55. PierceBirkhoff.pierce_birkhoff_conjecture_dim_two (research solved), in Pierce–Birkhoff conjecture
• 56. ShelahSpencerZeroOneLaw.zeroOne_irrational (research solved), in Shelah-Spencer's Zero-One Law for Sparse Random Graphs
• 57. LonelyRunnerConjecture.lonely_runner_conjecture.variants.tao_2017 (research solved), in Lonely runner conjecture
• 58. RiemannHypothesis.weil_positivity_criterion (research solved), in Equivalents to the Riemann Hypothesis
• 59. Green14.green_14_polynomial_k_eq_3 (research solved), in Ben Green's Open Problem 14
• 60. Green22.green_22.variants.moreira_infinite (research solved), in Green's Open Problem 22

Entries 61 to 80

• 61. Arxiv.«0805.3777».isGenericRank_cube (research solved), in Generic and maximal rank of 3-tensors
• 62. Arxiv.«2606.03696».bondy_conjecture.variants.large_explicit (research solved), in Bondy's conjecture on longest cycles in highly connected graphs
• 63. Green2.green_2_lower_bound_sanders (research solved), in Ben Green's Open Problem 2
• 64. RiemannZetaValues.infinite_irrational_at_odd (research solved), in Particular values of the Riemann zeta function
• 65. CarmichaelTotient.carchimaelTotient_bound (research solved), in Carmichael's totient function conjecture
• 66. HyperbolicGroupsResiduallyFinite.hyperbolic_residuallyFinite_iff_exists_finiteIndex_ne_top (research solved), in Residual finiteness of hyperbolic groups
• 67. Kourovka.«8.8».kourovka_8_8a (research solved), in Conjecture 8.8
• 68. EisenbudGreenHarris.eisenbud_green_harris.variants.caviglia_deStefani (research solved), in The Eisenbud-Green-Harris conjecture
• 69. Arxiv.«math.0608009».dixmier_conjecture.variants.poisson_implication (research solved), in The Dixmier Conjecture
• 70. AuslanderReiten.auslander_reiten.variants.normal (research solved), in The Auslander-Reiten conjecture
• 71. Green19.green_19 (research solved), in Ben Green's Open Problem 19
• 72. Green54.green_54 (research solved), in Ben Green's Open Problem 54
• 73. Green72.no_k_in_line_big (research solved), in Ben Green's Open Problem 72
• 74. InscribedSquare.exists_inscribed_square_of_C2 (research solved), in Inscribed square problem
• 75. OeisA109074.conjecture (research solved), in Numerator of \(\binom{6n-2}{2n} / \left(2 \binom{4n-1}{2n}\right)\)
• 76. DirichletDivisorProblem.divisor_error_hardy (research solved), in Dirichlet divisor problem
• 77. Green16.green_16_upper_bound (research solved), in Ben Green's Open Problem 16
• 78. PowerfulNumbersDensity.asymptotic_bateman_grosswald (research solved), in Asymptotic density of powerful numbers
• 79. NoetherProblem.noether_problem.variants.forty_seven (research solved), in Rational_variety
• 80. UnionClosed.union_closed.variants.yu (research solved), in Union-closed sets conjecture

Entries 81 to 100

• 81. GaussCircleProblem.error_not_isLittleO (research solved), in Gauss circle problem
• 82. Arxiv.«1609.08688».maximalLength_le_isBigO (research solved), in The length of an \(s\)-increasing sequence of \(r\)-tuples
• 83. Bloch.landauConstant_upper_bound (research solved), in Bloch and Landau constants
• 84. Green26.green_26.variants.yu25 (research solved), in Green's Open Problem 26
• 85. Green27.green_27.variants.lower_be23 (research solved), in Green's Open Problem 27
• 86. LamLitt.lam_litt.variants.eisenstein (research solved), in Lam--Litt conjecture
• 87. Mahler32.mahler_conjecture.variants.flatto_lagarias_pollington (research solved), in Mahler's 3/2 Problem
• 88. FiniteLocallyFreeGroupSchemeExponent.killed_by_rank.variants.reduced_base (research solved), in Is a finite locally free group scheme killed by its order?
• 89. Green18.green_18.bmz_corners (research solved), in Ben Green's Open Problem 18
• 90. Gourevitch.gourevitch_series_identity (research solved), in Gourevitch's series identity
• 91. ConjugacyClassSizes.conjClassSizes_iff_sym_three_solvable (research solved), in The \(S_3\)-conjecture (conjugacy classes of distinct sizes)
• 92. Green82.green_82_upper_bound (research solved), in Ben Green's Open Problem 82
• 93. Bugeaud06.boshernitzan (research solved), in Bugeaud Collection of Conjectures and Open Questions: Rapidly Increasing Sequences Dense Modulo One
• 94. Green29.green_29.variant (research solved), in Ben Green's Open Problem 29
• 95. Green31.green_31.variants.upper_cho25 (research solved), in Ben Green's Open Problem 31
• 96. WeaklyFirstCountable.CH.existsWeaklyFirstCountableCompactNotFirstCountable (research solved), in Conjectures about Weakly First Countable spaces
• 97. Green21.green_21.variants.fox_kleitman (research solved), in Ben Green's Open Problem 21
• 98. Green51.green_51.upper_ap (research solved), in Green's Open Problem 51
• 99. LehmerMahlerMeasureProblem.lehmer_mahler_measure_problem.variants.not_reciprocal (research solved), in Lehmer's Mahler measure problem
• 100. SixStandardDeviations.six_standard_deviations (research solved), in Six standard deviations suffice (Spencer's theorem)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.