Papers With

← All papers
First page of A counterexample to Vaught's Conjecture for $L_{ω_1,ω}$

A counterexample to Vaught's Conjecture for $L_{ω_1,ω}$

Nathanael L. Ackerman, Cameron E. Freer, Robin W. Knight

math.LO Oct 10, 2026 · v1
formalization ai-agents logic
Read PDF arXiv abstract Code
TL;DR
The full counterexample to Vaught's conjecture for L_{ω1,ω} is formally verified in Lean 4, built with AI coding agents and an infinitary-logic Lean library.
Abstract
We construct a sentence of $L_{ω_1,ω}$ having exactly $\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.
Problem

Vaught's conjecture for the infinitary logic L_{ω1,ω} asserts that any sentence with uncountably many countable models has a perfect set of non-isomorphic models. The authors seek a counterexample: a sentence with exactly aleph_1 countable models up to isomorphism but no perfect set of non-isomorphic models.

Approach

The construction follows Robin Knight's framework. It introduces geometry languages and 'Knight systems', and shows that any class forming the base of a Knight system has aleph_1 models and no perfect set. A toy example using labeled geometric trees motivates the method. The actual counterexample is built from plans, templates, and a legal template system. Coding agents, using the lean4-skills workflow and a Lean LSP MCP server, helped formalize the proof in Lean 4 with Freer's infinitary-logic library. SMT and Horn clause solvers were used to explore finite configurations, but the final proof does not trust them.

Results

A sentence of L_{ω1,ω} with exactly aleph_1 countable models and no perfect set of non-isomorphic models is constructed. This disproves Vaught's conjecture for infinitary logic, and the entire argument is certified in Lean.