AI Proves in Half an Hour a Math Theorem Humans Couldn't Crack in a Year
A stuck L^p problem: AI delivers a five-page proof in half an hour, compresses a 60-page paper down to its core lemma, and casually pushes the threshold for continuous density from 588 to 9.
The argument · tap a timestamp to hear it
For the first time, AI had a good idea
The speaker says this is the first time he has encountered a model that "really had a good idea" on a problem he has worked on for a long time, and that this idea led to "very elegant efficient progress." Note his wording: it's not that AI did the computation for him, it's that AI produced a proof approach he hadn't thought of. He credits the result to Astra, and says it was done only last week.
— Constantin KoglerThe key theorem: absolute continuity automatically carries L^p
The core theorem is: if a self-similar measure μ is absolutely continuous, then its density automatically lies in some L^p with p greater than 1. What actually excites the speaker is not the fact itself, but that p is quantitative — p can be expressed explicitly in terms of the mass μ assigns to small balls. Precisely because p is quantitative, one can bring over the methods used to study explicit absolute continuity, construct explicit L^p examples, and from there get to continuous density.
— Constantin Koglerp can never be made uniform
The speaker specifically warns: p can never be made uniform. For any dimension d and any p greater than 1, there exists some self-similar measure that lies in L^1 but not in L^p. So this quantitative result must not be read as "all absolutely continuous self-similar measures have uniform L^p integrability" — it is a case-by-case bound that depends on the mass distribution.
— Constantin KoglerSplitting λ into odd and even parts
The trick for proving continuous density: split the random series of the Bernoulli convolution into odd and even terms; after factoring out one λ from the odd part, what remains is exactly the even part. So μ_λ equals the convolution of μ_{λ²} with itself. If λ² falls in the range where Solomyak proved L^2 holds almost surely, then the convolution of two L^2 functions is continuous, and μ_λ has continuous density. This is the bridge from an L^2 result to continuity.
— Constantin KoglerA 60-page paper compressed into 5 pages
The speaker says the core idea was in fact already his and his collaborator's, but that AI was "extremely elegant and efficient" in using it. Varju's paper is 60 pages, his own paper is also very long, and AI compressed the passage from one result to another into 5 pages; and after "maybe a bit of a weakening," another 5 pages suffice to get a stronger conclusion. He stresses this is not AI thinking up the core idea for him, it's AI combining known tools in a way he "could have never" done.
— Constantin KoglerHalf an hour to run, 50 hours to formalize
Asked about runtime, the speaker says "not long, maybe half an hour." The whole result was then formalized in Lean, which took about 50 hours. He also mentions tricks like a goal command that let the model "really try hard." The comparison: it might have taken him a year, and "if you sent me this paper to referee, I would like who is this person?"
— Constantin KoglerThe threshold for continuous density goes from 588 to 9
For the case λ = 1 - 1/n, AI proves μ_λ is continuous when n is greater than 588 — the speaker says this is not yet the result of him pushing the constant, "if I push the constant, I could easily push the constant more." Even more striking is another result: absolutely continuous when n is greater than 9, which the speaker says "I could not dare think I could prove"; he himself pushed for two and a half hours to get to 9, while the ideal target is 3.
— Constantin KoglerThe key lemma comes from an obscure paper
At the heart of the proof is a lemma from geometric measure theory: for a positive L^1 function f, if the mass of a set inside a small ball is small and the integral of f over that set is also small, then f lies in some explicit L^p, with p given explicitly by C, ε, A. The speaker says this lemma is "not too difficult to prove," about a page, but "extremely difficult to find because it's not a very well-known fact" — it was dug out of some random papers.
— Constantin KoglerIn their own words · checked verbatim
it was the first time for me where where the models really had a good idea. So they had a good idea on a problem I worked long about that le led to progress like very elegant efficient progress I was very happy with.
Constantin Kogler0:18
the AI was extremely elegant and efficient in using it so var's paper is 60 pages okay my paper is k does many things but it's also it's also a long paper the AI reduced to five pages
Constantin Kogler34:17
it just used these things that I knew. It used the tools I used too, but it just combined it in a way I could have never.
Constantin Kogler37:19
if you sent me this paper to referee, I would like who is this person? I mean, this is like it was it's a if this is the smartest person in the world, I would say fine. But uh but I've never seen anything like this.
Constantin Kogler37:19
That's me not trying hard. That's not me. This is not me trying to run the I can push the constant more, but it's just it's just the eye chilling and p pushing.
Constantin Kogler39:21
if you're an analytic number theorist if you want to calculate something these things are unbeliev like uncomparable to us in calculations.
Constantin Kogler41:22
it's extremely difficult to find because it's not a very well-known fact. It's some random fact from wherever.
Constantin Kogler44:23
Figures
| AI proof runtime | about half an hour | 36:18 |
| Lean formalization time | about 50 hours | 36:18 |
| Varju paper length | 60 pages | 34:17 |
| AI-compressed proof length | 5 pages | 34:17 |
| Continuous density threshold n | greater than 588 | 39:21 |
| Absolute continuity threshold n | greater than 9 | 41:22 |
| Ideal target threshold n | 3 | 41:22 |
| Time speaker spent pushing the constant | about two and a half hours | 41:22 |
Glossary
- self-similar measure
- A probability measure generated by finitely many contracting similarity maps and satisfying a self-similarity equation, usually a fractal object.
- Bernoulli convolution
- The distribution of the random series Σ ±λ^n, with λ between 0 and 1; a classical model for studying absolute continuity.
- absolutely continuous
- A measure that can be written as the integral of some L^1 function against Lebesgue measure, i.e. a density function exists.
- L^p density
- A density function lying in the L^p space; the larger p is, the more "spread out" the density is required to be.
- Lean
- An interactive theorem prover used to formalize mathematical proofs to the point of machine verification.
How to listen
Mathematicians and theoretical computer scientists interested in AI's real capabilities in pure math, and engineers who want to see what "AI doing proofs" actually looks like.
You can fast-forward the first section on the basic definitions of self-similar measures and Bernoulli convolutions, and jump straight to the AI part after the 33-minute mark.