A Lean-checked construction disproves Vaught's conjecture for infinitary logic

← Back to the filtered Breakthrough Tracker

Stable ID

math-vaught-infinitary-counterexample-2026

Revision

math-vaught-infinitary-counterexample-2026.v3

Field

Mathematics · Model theory, descriptive set theory and formal verification

Evidence

Tier 1 · Peer reviewed: No

Record state

Provisional · Formally checked provisional counterexample

Last checked

2026-10-25

AI role

Freer worked with Claude Code, Codex and related models to formalize and repair Knight's construction. The authors report substantial human mathematical direction, AI-assisted exploration and three propositions requiring extensive guided AI work.

Record details

Problem or result

Vaught's conjecture for sentences of infinitary logic L-omega-one-omega

Authors

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

Institutions

Harvard University; Massachusetts Institute of Technology; University of Oxford

Result date

Preprint submitted October 10; Lean correspondence work extended through October 25, 2026

Why it matters

The infinitary statement is one of the oldest open problems connecting model theory and descriptive set theory. The public Lean theorem now proves the manuscript's Theorem 4.36 spectrum statement for the repository's template sentence on models coded by the natural numbers, adding unusually strong artifact evidence to the unrefereed paper.

Limits

The result concerns infinitary logic, not the still-open first-order Vaught conjecture. The repository proves exactly aleph-one isomorphism classes and no perfect set for its template sentence on models coded by the natural numbers, but explicitly does not identify that sentence with its density sentence or transfer the repository's main theorem. The prose paper remains unrefereed and the definitions still require semantic specialist review.

Sources

1. Primary: Ackerman, Freer and Knight counterexample preprint
2. Formal proof: Lean proof development
3. Independent mechanical check: Palomar Comparator registry entry

Correction and revision history

1. 2026-10-19 — Added after primary-source, scope, status, AI-role and limitation review.
2. 2026-10-22 — Recorded post-publication Lean work formalizing counterparts of Propositions 4.32, 4.34 and 4.35, while preserving the repository's explicit sentence-identification and spectrum-transfer caveats.
3. 2026-10-25 — Recorded the merged Lean proof of Theorem 4.36 for the repository's template sentence and the published-text audit, while retaining the explicit sentence-identification, spectrum-transfer and semantic-review caveats.

Machine-readable: JSON v1 · CSV v1 · Schema v1

This individual record remains noindex until a story-specific featured image passes Kingy’s rendered-pixel visual review. The source-linked tracker hub remains the public index.