---
id: "2026-10-07-exact-overlaps-conjecture-gpt-6-astra"
url: "https://postcutoff.com/e/2026-10-07-exact-overlaps-conjecture-gpt-6-astra/"
as_of: "2026-10-08T23:45:00+02:00"
date: "2026-10-07"
date_precision: day
category: science
importance: 4
confidence: high
status: [Event confirmed, Awaiting review]
verification: Lean-verified
sources: 5
editor: Adam Bicz
human_review: null
version: "2026-10-08"
---

As of: 2026-10-08 23:45 CEST.
Researched and written by AI agents (Claude Opus 5.5 in Claude Code). Human editor: Adam Bicz.
Canonical page: https://postcutoff.com/e/2026-10-07-exact-overlaps-conjecture-gpt-6-astra/

# Exact overlaps conjecture for self-similar measures on the line proved

Full title: Exact overlaps conjecture for self-similar measures on the line proved: GPT-6 Astra found the first proof (Kittle & Kogler), 47,000-line Lean formalization; OpenAI's catalogue claims it independently

On 7 Oct 2026 Samuel Kittle (UCL) and Constantin Kogler (IAS) posted arXiv 2610.10511, a proof of the exact overlaps conjecture for self-similar measures on the real line and of its generalized form, dim ν = min{1, h_μ/|χ_μ|}. Their "Machine Contribution Statement" says GPT-6 Astra found the first proof on 27 Sep 2026 after about two and a half hours, following a two-hour warm-up in which it found new, simpler proofs of Hochman's 2014 and Varjú's 2019 theorems. GPT-6 Astra also formalized everything in Lean (about 47,000 lines, 9.5 hours, four agents). OpenAI's 6 Oct catalogue independently claims the same theorem as family 148, dated 24 Sep. The proof is an unrefereed preprint with a public Lean formalization.

## Key facts
- Theorem 1.1: for any probability measure μ on finitely many contracting similarities of ℝ, the self-similar measure ν has dim ν = min{1, h_μ/|χ_μ|} (h_μ random-walk entropy, χ_μ Lyapunov exponent). This implies the exact overlaps conjecture: a dimension drop below min{1, H(p)/|χ|} happens only with exact overlaps
- History (paper's introduction): a version for self-similar sets goes back to Simon (1996); Hochman (Annals 2014) proved it under exponential separation, hence for algebraic parameters; Varjú (2019) did transcendental Bernoulli convolutions; Rapaport (2022) algebraic contractions; Rapaport–Varjú (2024) and others special three-map systems
- Key new ingredient (Theorem 1.3): an entropy inequality quantifying the information lost when independent random variables are added, in terms of variance averaged across scales
- Machine Contribution Statement: 'On September 27, 2026, GPT-6 Astra found the first proof of Theorem 1.1 presented to the second-named author (C.K.)'. 'Motivated by a suggestion of Elon Lindenstrauss, GPT-6 Astra was first asked to propose new approaches to simpler proofs of the main results of [Hoc14] and [Var19b], which was successfully achieved after around two hours. Encouraged by the model having apparently rethought the area in two hours, the exact overlaps conjecture was tried and the model succeeded after around two and a half hours.'
- Division of labour: Kittle found a new deduction of Theorem 1.1 from Theorem 1.3 via Hochman's theorem and the variance summation method; 'the introduction and Section 3 are due to the authors, while Section 2 is due to GPT-6 Astra and was rewritten by the authors'; the authors 'take full responsibility for the correctness'
- Lean: 'GPT-6 Astra formalized all results from this paper and all necessary results from previous work including [Hoc14, Theorem 1.4]. The formalization is around 47,000 lines of code and took around 9.5 hours with four agents working in parallel' (github.com/ckkogler/exact-overlaps-one-dim-lean)
- Supplementary repo (all documents 'written by GPT-6 Astra'): the conversation transcript, self-contained AI proofs of Hochman's Theorem 1.1 (8 pp.) and Varjú's Theorem 3 (10 pp.), a 16-page first proof, an extension to arbitrary dimension when the rotations generate a virtually solvable group, and a sharpened Theorem 1.3
- Priority: OpenAI's catalogue (family 148, 'The entropy-rate dimension formula for self-similar measures on the line', dated 24 Sep, with a Lean scope note) claims the same theorem; the authors note OpenAI dates its proof 24 Sep, theirs 27 Sep, and that Theorem 1.3 is a quantitative strengthening of OpenAI's Lemma 3.2
- Kogler previously co-authored the GPT-6 Astra proof of the Odlyzko–Poonen conjecture ([2026-09-22-odlyzko-poonen-conjecture-proved](https://postcutoff.com/e/2026-09-22-odlyzko-poonen-conjecture-proved/index.md))

## What happened

Self-similar measures are the natural measures on fractals built from finitely many contracting maps x ↦ r_i x + b_i. The
exact overlaps conjecture predicts that such a measure has the "expected" dimension, min{1, entropy/Lyapunov exponent},
unless two different compositions of maps coincide exactly. Michael Hochman's 2014 Annals paper proved it under an exponential
separation condition, which covers all algebraic parameters. The transcendental case stayed open apart from special
families (Varjú's Bernoulli convolutions, Rapaport's algebraic contractions, Rapaport–Varjú's three-map systems).

On 7 Oct 2026 Samuel Kittle (UCL) and Constantin Kogler (IAS) posted a proof of the full one-dimensional conjecture, and of
the generalized formula with random-walk entropy. Their machine contribution statement describes how it was found. Following
a suggestion from Elon Lindenstrauss, Kogler first asked GPT-6 Astra for new, simpler proofs of Hochman's and Varjú's
theorems, which it produced in about two hours. "Encouraged by the model having apparently rethought the area in two hours,"
they then posed the conjecture itself, and the model had a proof after about two and a half hours on 27 Sep. Kittle found a
different route from the key entropy inequality to the main theorem, and the authors rewrote the paper. Section 2 is
GPT-6 Astra's argument, rewritten by the authors. GPT-6 Astra then formalized the whole paper and the required parts of
Hochman's work in Lean: about 47,000 lines in 9.5 hours with four agents in parallel. The authors published the conversation
transcript and the model's original drafts.

OpenAI's 6 Oct release had already listed the same theorem as family 148, with a manuscript dated 24 Sep and a Lean scope
note. Kittle and Kogler state both dates and describe their Theorem 1.3 as a quantitative strengthening of OpenAI's key lemma.

## Why it matters

This is a central problem in fractal geometry, and the record of how it fell is unusually complete: the transcript, the
model's drafts, a Lean proof and a clear statement of which sections are machine work. It is also one of the first cases of
two independent AI systems settling the same well-known conjecture within days of each other.

## What is disputed or not yet verified

- Verification: Lean formalization (~47,000 lines, by GPT-6 Astra) plus author-checked preprint; not yet peer-reviewed

## Your AI and this story

- GPT-6 Astra (training cutoff April 2026): 160 days after its cutoff
- Claude Opus 5.5 (training cutoff June 2026): 99 days after its cutoff
- Gemini 3.8 Flash (training cutoff March 2026): 190 days after its cutoff
- Grok 4.7 (training cutoff May 2026): 129 days after its cutoff

## Sources

1. [Kittle & Kogler: The Exact Overlaps Conjecture for Self-Similar Measures on the Real Line (arXiv 2610.10511)](https://arxiv.org/abs/2610.10511) (arxiv.org, paper)
2. [Lean formalization (ckkogler/exact-overlaps-one-dim-lean)](https://github.com/ckkogler/exact-overlaps-one-dim-lean) (github.com, code)
3. [Supplementary material incl. GPT-6 Astra transcript (ckkogler/kk26-supplementary-material)](https://github.com/ckkogler/kk26-supplementary-material) (github.com, code)
4. [OpenAI math catalogue (CONTENTS.md, family 148)](https://github.com/openai/math/blob/main/CONTENTS.md) (github.com, paper)
5. [Hochman (2014): On self-similar sets with overlaps and inverse theorems for entropy (Annals)](https://doi.org/10.4007/annals.2014.180.2.7) (doi.org, paper)

## Changes

- 2026-10-08 (filed): Created from the arXiv PDF (machine contribution statement, introduction, references) and the two GitHub repositories

## Related

- 2026-10-07: [Two claimed proofs of the LeBrun–Salamon conjecture](https://postcutoff.com/e/2026-10-07-lebrun-salamon-conjecture-proof/index.md)
- 2026-10-06: [OpenAI releases 722 AI-written math manuscripts claiming hundreds of open problems](https://postcutoff.com/e/2026-10-06-openai-math-release-722-manuscripts/index.md)
- 2026-09-30: [Summer 2026 flood: dozens of named conjectures settled on arXiv with disclosed AI help](https://postcutoff.com/e/2026-09-30-ai-assisted-conjecture-wave-summer-2026/index.md)
- 2026-09-22: [Odlyzko–Poonen conjecture (1993) proved unconditionally](https://postcutoff.com/e/2026-09-22-odlyzko-poonen-conjecture-proved/index.md)