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

Your AI and this story

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