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/ arXiv: 2610.15217 / 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.

Formalizations

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. https://palomar-registry.org/entry?id=PALOMAR-2026-10-07-000001&version=1. Palomar Registry, PALOMAR-2026-10-07-000001, version 1link
  3. Nathanael Ackerman; Cameron Freer; Robin Knight. Vaught's Conjecture Counterexample: Lean 4 Proof Development. 2026. https://github.com/cameronfreer/vaught-conjecture-counterexample/. GitHub repositorylink
  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. https://github.com/oOo0oOo/lean-lsp-mcplink
  9. Cameron E. Freer. Lean 4 Skills: Theorem Proving Skill and Workflow Pack for AI Coding Agents. 2025. https://github.com/cameronfreer/lean4-skillslink
  10. Cameron E. Freer. Infinitary Logic in Lean 4. 2026. https://github.com/cameronfreer/infinitary-logiclink
Show all 30 referencesShow fewer references
  1. Hjorth, Greg. Vaught's conjecture on analytic sets. J. Amer. Math. Soc., vol. 14, no. 1, pp. 125–143. 2001DOI
  2. Hjorth, Greg. A note on counterexamples to the Vaught conjecture. Notre Dame J. Formal Logic, vol. 48, no. 1, pp. 49–51. 2007DOI
  3. 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
  4. Hart, Bradd; Starchenko, Sergei; Valeriote, Matthew. Vaught's conjecture for varieties. Trans. Amer. Math. Soc., vol. 342, no. 1, pp. 173–196. 1994DOI
  5. 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
  6. Jech, Thomas. Set theory. Springer-Verlag, Berlin, pp. xiv+769. 2003
  7. Knight, R. W. The Vaught Conjecture: A Counterexample. 2002. Unpublished manuscript
  8. Kurilić, Miloš S. Vaught's conjecture for almost chainable theories. J. Symbolic Logic, vol. 86, no. 3, pp. 991–1005. 2021DOI
  9. Lopez-Escobar, E. G. K. An interpolation theorem for denumerably long formulas. Fund. Math., vol. 57, pp. 253–272. 1965DOI
  10. Mayer, Laura L. Vaught's conjecture for o-minimal theories. J. Symbolic Logic, vol. 53, no. 1, pp. 146–159. 1988DOI
  11. Montalbán, Antonio. A computability theoretic equivalent to Vaught's conjecture. Adv. Math., vol. 235, pp. 56–73. 2013DOI
  12. Morley, Michael. The number of countable models. J. Symbolic Logic, vol. 35, pp. 14–18. 1970DOI
  13. Puninskaya, Vera. Vaught's conjecture for modules over a serial ring. J. Symbolic Logic, vol. 65, no. 1, pp. 155–163. 2000DOI
  14. Sacks, Gerald E. On the number of countable models. Southeast Asian conference on logic (Singapore, 1981), vol. 111, pp. 185–195. 1983DOI
  15. Sami, Ramez L. Polish group actions and the Vaught conjecture. Trans. Amer. Math. Soc., vol. 341, no. 1, pp. 335–353. 1994DOI
  16. 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
  17. Steel, John R. On Vaught's conjecture. Cabal Seminar 76–77 (Proc. Caltech-UCLA Logic Sem., 1976–77), vol. 689, pp. 193–208. 1978
  18. Steel, John R. On Vaught's conjecture. Large cardinals, determinacy and other topics. The Cabal Seminar. Vol. IV, vol. 49, pp. 179–195. 2021
  19. Tanović, Predrag. Vaught's conjecture for theories of discretely ordered structures. Notre Dame J. Formal Logic, vol. 65, no. 3, pp. 247–257. 2024DOI
  20. 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