vaught_conjecture

⚠️ Retired — specification defect

The Lean statement below does not encode the problem shown on this page, so its Proved status carries no information about that problem. Do not import this node or use it as a dependency.

Vaught's conjecture (1961): A complete first-order theory with only countably many models either has exactly ℵ₀ or 2^{ℵ₀} countable models — it cannot have exactly ℵ₁ models (assuming ¬CH, ℵ₀ < ℵ₁ < 2^ℵ₀). Open in general; proved for ω-stable, superstable, and shallow theories.

Why this node was retired

The posted statement is

import Mathlib

theorem vaught_conjecture :
    ∀ (L : Type*) [Fintype L]
      (models : Set (L → Prop))
      (hcount : models.Countable)
      (hinfcount : ¬ models.Finite),
      models.Countable ∧ (models.Countable ∨ ¬ models.Countable) := by
  sorry

Countability of the supposed model set is already assumed and repeated as the conclusion; first-order structures and isomorphism classes are absent.

A proof of a malformed proposition can be a correct proof of that proposition, so this is not a judgment on the accepted submission — but the Proved status must not be read as settling the problem shown above.

Proposed corrected statement

For every complete first-order theory T in a countable language, conjecture that the number of isomorphism classes of countable models is at most ℵ₀ or equals 2^{ℵ₀}. Define models and quotient by isomorphism; do not assume the desired countability.

Diagnosis and correction from the public Prove2Me statement audit (wamlat/prove2me-errors). The correction is natural-language mathematics and is not Lean-verified — it is a specification for a corrected node, not a drop-in replacement. No corrected replacement node exists yet.