HEXAGONbeta

A counterexample to Vaught's Conjecture for Lω1,ωL_{\omega_1,\omega}

Primarily human-written textHuman understanding: all partsmath.LO — Logic

Contributed by Nathanael L. Ackerman ↗, Cameron Freer ↗, Robin W. Knight

Version 1 / Oct 11, 2026 / CC BY 4.0

Abstract

We construct a sentence of Lω1,ωL_{\omega_1,\omega} having exactly ℵ1\aleph_1 many countable models up to isomorphism, but no perfect set of non-isomorphic models. This disproves Vaught's conjecture for infinitary logic. The construction follows a framework devised by Robin Knight, and the proof has been formally verified in Lean.

Provenance statement

The construction and general proof strategy are based on an unpublished draft by Robin Knight. Cameron Freer carried out the Lean formalization in collaboration with Nathanael Ackerman and Knight, using AI coding agents for implementation and mathematical exploration, including revisions to the construction and new ideas developed through human–AI interaction. The complete formal proof has been checked by Comparator and is available on the Palomar Registry. Ackerman wrote the initial draft of this paper, which all three authors subsequently revised. AI tools assisted with review.
FormalizationsPalomar

Tools used

Anthropic
Claude Code
OpenAI
Codex
OpenAI
ChatGPTVersion Pro
Lean
Lean
Z3 and Python
SMT and Horn clause solvers

References

  1. Ackerman, Nathanael Leedom. Vaught's conjecture without equality. Notre Dame J. Formal Logic, vol. 56, no. 4, pp. 573–582. 2015DOI
  2. Nathanael Ackerman; Cameron Freer; Robin Knight. A Counterexample to Vaught's Conjecture for Infinitary Logic. 2026. r̆lhttps://palomar-registry.org/entry?id=PALOMAR-2026-10-07-000001&version=1
  3. Nathanael Ackerman; Cameron Freer; Robin Knight. Vaught's Conjecture Counterexample: Lean 4 Proof Development. 2026. r̆lhttps://github.com/cameronfreer/vaught-conjecture-counterexample/
  4. Becker, Howard. The topological Vaught's conjecture and minimal counterexamples. J. Symbolic Logic, vol. 59, no. 3, pp. 757–784. 1994DOI
  5. Becker, Howard. Isomorphism of computable structures and Vaught's conjecture. J. Symbolic Logic, vol. 78, no. 4, pp. 1328–1344. 2013link
  6. Baldwin, John T.; Friedman, Sy D.; Koerwien, Martin; Laskowski, Michael C. Three red herrings around Vaught's conjecture. Trans. Amer. Math. Soc., vol. 368, no. 5, pp. 3673–3694. 2016DOI
  7. Buechler, Steven. Vaught's conjecture for superstable theories of finite rank. Ann. Pure Appl. Logic, vol. 155, no. 3, pp. 135–172. 2008DOI
  8. Oliver Dressler. Lean Theorem Prover MCP. 2025
  9. Cameron E. Freer. Lean 4 Skills: Theorem Proving Skill and Workflow Pack for AI Coding Agents. 2025
  10. y̱same, Infinitary logic in Lean 4 , r̆l https://github.com/cameronfreer/infinitary-logic , 2026.link
  11. Hjorth, Greg. Vaught's conjecture on analytic sets. J. Amer. Math. Soc., vol. 14, no. 1, pp. 125–143. 2001DOI
  12. Hjorth, Greg. A note on counterexamples to the Vaught conjecture. Notre Dame J. Formal Logic, vol. 48, no. 1, pp. 49–51. 2007DOI
  13. Hjorth, Greg; Solecki, Slawomir. Vaught's conjecture and the Glimm-Effros property for Polish transformation groups. Trans. Amer. Math. Soc., vol. 351, no. 7, pp. 2623–2641. 1999DOI
  14. Hart, Bradd; Starchenko, Sergei; Valeriote, Matthew. Vaught's conjecture for varieties. Trans. Amer. Math. Soc., vol. 342, no. 1, pp. 173–196. 1994DOI
  15. Iverson, Paul. The number of countable isomorphism types of complete extensions of the theory of Boolean algebras. Colloq. Math., vol. 62, no. 2, pp. 181–187. 1991DOI
  16. Jech, Thomas. Set theory. Springer-Verlag, Berlin, pp. xiv+769. 2003
  17. Knight, R. W. The Vaught Conjecture: A Counterexample. 2002. Unpublished manuscript
  18. Kurilić, Miloš S. Vaught's conjecture for almost chainable theories. J. Symbolic Logic, vol. 86, no. 3, pp. 991–1005. 2021DOI
  19. Lopez-Escobar, E. G. K. An interpolation theorem for denumerably long formulas. Fund. Math., vol. 57, pp. 253–272. 1965DOI
  20. Mayer, Laura L. Vaught's conjecture for o-minimal theories. J. Symbolic Logic, vol. 53, no. 1, pp. 146–159. 1988DOI
  21. Montalbán, Antonio. A computability theoretic equivalent to Vaught's conjecture. Adv. Math., vol. 235, pp. 56–73. 2013DOI
  22. Morley, Michael. The number of countable models. J. Symbolic Logic, vol. 35, pp. 14–18. 1970DOI
  23. Puninskaya, Vera. Vaught's conjecture for modules over a serial ring. J. Symbolic Logic, vol. 65, no. 1, pp. 155–163. 2000DOI
  24. Sacks, Gerald E. On the number of countable models. Southeast Asian conference on logic (Singapore, 1981), vol. 111, pp. 185–195. 1983DOI
  25. Sami, Ramez L. Polish group actions and the Vaught conjecture. Trans. Amer. Math. Soc., vol. 341, no. 1, pp. 335–353. 1994DOI
  26. Shelah, S.; Harrington, L.; Makkai, M. A proof of Vaught's conjecture for ω\omega-stable theories. Israel J. Math., vol. 49, no. 1-3, pp. 259–280. 1984DOI
  27. J. R. Steel, On V aught's conjecture , Cabal S eminar 76--77 ( P roc. C altech- UCLA L ogic S em., 1976--77), Lecture Notes in Math., vol. 689, Springer, Berlin, 1978, pp. 193--208.
  28. Steel, John R. On Vaught's conjecture. Large cardinals, determinacy and other topics. The Cabal Seminar. Vol. IV, vol. 49, pp. 179–195. 2021
  29. Tanović, Predrag. Vaught's conjecture for theories of discretely ordered structures. Notre Dame J. Formal Logic, vol. 65, no. 3, pp. 247–257. 2024DOI
  30. Vaught, R. L. Denumerable models of complete theories. Infinitistic Methods (Proc. Sympos. Foundations of Math., Warsaw, 1959), pp. 303–321. 1961

Version history

  1. v1Submitted by Cameron FreerInitial depositCurrentOct 10, 2026