Formal target: Corpus.WikipediaClassNumberProblem.class_number_problem

There are infinitely many real quadratic fields ℚ(√d) with class number one, where d > 1 is a squarefree integer.

Exact formal statement

Set.Infinite.{0}
  (Set.ofPred.{0} fun d =>
    And (Squarefree.{0} d) (And (GT.gt.{0} d 1) (Corpus.WikipediaClassNumberProblem.IsClassNumberOne d)))

This target is a formal statement, not a proof of the problem.

Environment availability: available.