Strichartz's Question on Fourier Frames for the Cantor Measure
Statement
Does the middle-third Cantor measure admit a Fourier frame, that is, a countable set of exponentials giving two-sided frame bounds on its space? No. The Cantor measure with base admits no Fourier frame for any odd integer , which answers Strichartz's question for the middle-third case.
Record
Comments
No person has examined this. Everything below was judged by machines. say whether it holds →
proof attempt · #1
Jaume de Dios Pont, Lukas Liehr and Mitchell A. Taylor, using GPT-5.5, GPT-5.5 in CodexThat credit came with the record as it was imported. No ProbXiv account is credited for this work, and nobody has answered for it here.
The paper devotes a section to it. The authors were trying to build a frame, not to rule one out. With GPT-5.5 they analyzed why their translated ternary digit set candidates fail to give scale-uniform frame bounds, and it is that failed construction which suggested the obstruction the final proof turns on. The model also simplified the key normalized polynomial into a more concise equivalent form. GPT-5.5 in Codex then wrote the Lean formalization, and the authors state that the proof files were generated by language models while they curated and checked the statement.
Machine-checked by Lean on #1 · not a person
lean: correctLeanscope Lean formalization of the result
Lean 4 formalization of the main theorem at the linked repository. Showcase.lean carries a self-contained statement the authors curated and reviewed for human readability; the proof files themselves were LLM-generated, and the trust rests on Mathlib's definitions. We have not recompiled it. arXiv preprint, not yet peer-reviewed.
Lean checked the formalisation, not that it says the same thing as the statement above.
Sign in with an institutional address to take part in the discussion. Reading every thread stays open to everyone.
Sign inSolve with an agent
Open the statement in a chat, with the problem and the ground rules already written into the prompt.