Harmonic Analysis

6 missions · 4 completed

Missions

Captain: Lucas

Formal Conjectures Portfolio: Bateman-Horn and CompanionsOpen Problem

## 1. Motivation Wikipedia's pages on open problems are, for many mathematicians, the first contact with a conjecture: a one-paragraph statement, a short history, a list of partial results. The [Formal Conjectures](https://github.com/google-deepmind/formal-conjectures) library (Google DeepMind, Apache-2.0) turned a large part of that material into Lean 4 statements, so that the conjectures can be attacked — and, just as importantly, *stated unambiguously* — by machine. This mission ports a coherent slice of that material to Prove2Me. It is deliberately a **portfolio mission**: the goal theorem is the Bateman–Horn conjecture, the strongest single statement in the collection, and the milestone list gathers the other conjectures and the landmark theorems that surround them. Some milestones are genuine steps toward the goal (the Bunyakovsky conjecture is literally the one-polynomial case); most are independent open problems from other fields, grouped here because they share a source, a level of difficulty, and a need for faithful formal statements. **A reader should not assume that proving a milestone advances the goal theorem.** The mission's value is that every statement in it has been written against the same Mathlib revision, checked to compile, and documented well enough to be attacked. A rough timeline of the collection's landmarks: - 1947 — Mills: a real $A>1$ with $\lfloor A^{3^n}\rfloor$ always prime. - 1962 — Radó: the busy beaver function outgrows every computable function. - 1971 — Davies: planar Kakeya sets have Hausdorff dimension $2$. - 1978 — Apéry: $\zeta(3)$ is irrational. - 1985 — Read (after Enflo, 1981): an operator on $\ell^1$ with no nontrivial closed invariant subspace. - 2001 — Zudilin: one of $\zeta(5),\zeta(7),\zeta(9),\zeta(11)$ is irrational. - 2002 — Mihăilescu: $8$ and $9$ are the only consecutive perfect powers (Catalan's conjecture). - 2009 / 2021 — Dvir; Bukh–Chao: the finite-field Kakeya bound and its sharp density constant. - 2021 — Gardam: Kaplansky's *unit* conjecture is false (its zero-divisor and idempotent companions remain open). - 2024 — Saito: Mills' constant is irrational; bbchallenge: $\mathrm{BB}(5)=47\,176\,870$. - 2025 — Wang–Zahl: the Kakeya set conjecture in $\mathbb{R}^3$. ## 2. Setting The goal theorem concerns prime values of polynomials. Fix a finite set $S=\{f_1,\dots,f_k\}\subseteq\mathbb{Z}[X]$ of distinct polynomials. Say that $f$ satisfies the **Bunyakovsky condition** if its leading coefficient is positive, $\deg f\ge 1$, and $f$ is irreducible over $\mathbb{Z}$; say that $S$ satisfies the **Schinzel condition** if for every prime $p$ there is an integer $n$ with $p\nmid f_1(n)\cdots f_k(n)$ — i.e. no fixed prime divides the product at every argument. For a prime $p$ let $\omega_p(S)$ be the number of residue classes $n \bmod p$ at which some $f_i$ vanishes, let $D=\prod_i \deg f_i$, and let $$\pi_S(x)=\#\{\,n\le x : |f_i(n)| \text{ is prime for every } i\,\}.$$ The **Bateman–Horn constant** is the (conditionally convergent) Euler product $$C=\lim_{N\to\infty}\ \prod_{p<N}\Big(1-\tfrac1p\Big)^{-k}\Big(1-\tfrac{\omega_p(S)}{p}\Big).$$ The other groups use their own vocabulary, each fixed in a definition item of this mission: Kakeya sets in $\mathbb{R}^n$ and over $\mathbb{F}_q$; Mills' property $\lfloor A^{3^n}\rfloor \in \mathbb{P}$; Wagstaff primes and Catalan–Mersenne numbers; polynomial self-maps and their Jacobian matrix; nontrivial closed invariant subspaces; linear extensions of a finite poset; Catalan's constant; and an explicit two-symbol Turing machine model with its maximum-shifts function $\mathrm{BB}$. ## 3. Target The goal theorem is the Bateman–Horn asymptotic: under the Bunyakovsky and Schinzel hypotheses, $C$ exists and is positive and $$\pi_S(x)\ \sim\ \frac{C}{D}\,\frac{x}{(\log x)^{k}}\qquad (x\to\infty).$$ Weaker statements in the same direction appear as milestones, first of all Bunyakovsky's conjecture: under the same hypotheses with $k=1$, $f$ takes prime values infinitely often. The remaining milestones are listed in the milestone panel and are grouped by subject: Diophantine equations (Brocard, Pillai, Lebesgue–Nagell, Catalan/Mihăilescu), Mersenne-type primality (New Mersenne, infinitude of Mersenne primes, Catalan–Mersenne), prime-representing constants (Mills), geometric measure theory (Kakeya in $\mathbb{R}^n$, Kakeya over $\mathbb{F}_q$, Falconer), operator theory (invariant subspace problem and Read's $\ell^1$ counterexample), group algebras (Kaplansky's zero-divisor and idempotent conjectures), affine algebraic geometry (the two-variable Jacobian conjecture), irrationality and transcendence ($\zeta(5)$, all odd zeta values, Zudilin's theorem, $e+\pi$, $e\pi$, $\gamma$, Catalan's constant), order theory (the $1/3$–$2/3$ conjecture), and computability (Radó's theorem). ## 4. Significance *The results themselves.* Bateman–Horn is the quantitative form of Schinzel's hypothesis H: it contains the twin prime conjecture, the infinitude of primes of the form $n^2+1$, and Bunyakovsky as special cases, and it is the standard heuristic behind prime-counting predictions. The other targets are each the headline question of their area: whether every bounded Hilbert-space operator has an invariant subspace; whether group algebras of torsion-free groups are domains; whether Kakeya sets must have full dimension. The solved milestones (Mihăilescu, Davies, Dvir, Zudilin, Read, Saito, Radó) are landmarks whose formal proofs would be significant library contributions in their own right. *Formalizing them.* None of the open statements is expected to fall here; the concrete deliverable is a set of faithful, compiling, reusable statements plus formal proofs of the solved milestones, most of which are not in Mathlib today. Several are realistically in reach: the finite-field Kakeya bound (Dvir's polynomial method is short), the elementary fact that $\pi+e$ and $\pi e$ cannot both be algebraic, and Radó's diagonal argument. ## 5. Difficulty For Bateman–Horn, the obstruction is visible already for $k=1$, $\deg f = 2$: sieve methods bound $\pi_S(x)$ from above by a constant times the conjectured main term and produce almost-primes, but the parity problem blocks every known sieve from producing a single prime value of an irreducible quadratic. The conditional convergence of the Euler product is a second, smaller trap: the product over $p<N$ must be taken in order, so any reformulation as an unordered infinite product changes the statement. Each other group has its own obstruction, and they do not transfer: the parity problem says nothing about Kakeya, where the difficulty is that dimension is not stable under the natural compactness arguments, nor about the invariant subspace problem, where the known counterexamples on $\ell^1$ show that no soft argument can work. ## 6. Formalization scope Conventions this mission commits to, all fixed in the definition items: - Polynomials are elements of `ℤ[X]`; primality of a polynomial value is primality of its absolute value, and the counting function ranges over natural numbers $n \le \lfloor x\rfloor$. - The Bateman–Horn constant is the limit of the *ordered* partial products over $p<N$, not an unordered infinite product. - Kakeya sets carry no compactness or measurability hypothesis, matching the source; the conjecture is stated as an equality of Hausdorff dimensions in $[0,\infty]$. - Falconer's hypothesis is written $d < 2\dim_H E$ to avoid division in $[0,\infty]$. - Torsion-freeness of a group is spelled out as "every element of finite order is the identity", which is the hypothesis the source intends (it is weaker than Mathlib's `IsMulTorsionFree`). - Linear extensions are order-preserving bijections onto $\{0,\dots,|P|-1\}$, and probabilities are quotients of set cardinalities in $\mathbb{Q}$. - The busy beaver model is an explicit $n$-state, $2$-symbol machine with a bi-infinite Boolean tape; $\mathrm{BB}$ counts transitions performed (maximum shifts), the halting transition included, and $\mathrm{BB}(0)=0$. - Several source statements are phrased as "is $X$ true?" with an unknown answer. Prove2Me statements must be definite, so each such question is recorded in its **affirmative** form (e.g. "$e+\pi$ is irrational"); a solver who can refute one should submit a disproof. The one question with no statable answer, "what is $\mathrm{BB}(6)$?", is replaced by Radó's growth theorem rather than guessed at. - Nothing here is vacuous: each hypothesis set is satisfiable (e.g. closed unit balls are Kakeya sets, and $X^2+1$ satisfies the Bunyakovsky and Schinzel conditions). Contributions welcome: proofs of the solved milestones; sharper variants; and additional faithful statements from the same source library, which contains far more than fits in one mission. ## 7. Selected references - P. T. Bateman and R. A. Horn, *A heuristic asymptotic formula concerning the distribution of prime numbers*, Math. Comp. 16 (1962), 363–367. [DOI](https://doi.org/10.1090/S0025-5718-1962-0148632-7) - T. Radó, *On non-computable functions*, Bell System Tech. J. 41 (1962), 877–884. [DOI](https://doi.org/10.1002/j.1538-7305.1962.tb00480.x) - R. O. Davies, *Some remarks on the Kakeya problem*, Math. Proc. Cambridge Philos. Soc. 69 (1971), 417–421. [DOI](https://doi.org/10.1017/S0305004100046867) - C. J. Read, *A solution to the invariant subspace problem on the space $\ell_1$*, Bull. London Math. Soc. 17 (1985), 305–317. [DOI](https://doi.org/10.1112/blms/17.4.305) - K. Falconer, *On the Hausdorff dimensions of distance sets*, Mathematika 32 (1985), 206–212. [DOI](https://doi.org/10.1112/S0025579300010998) - W. Zudilin, *One of the numbers $\zeta(5),\zeta(7),\zeta(9),\zeta(11)$ is irrational*, Russian Math. Surveys 56 (2001), 774–776. [DOI](https://doi.org/10.1070/RM2001v056n04ABEH000427) - P. Mihăilescu, *Primary cyclotomic units and a proof of Catalan's conjecture*, J. reine angew. Math. 572 (2004), 167–195. [DOI](https://doi.org/10.1515/crll.2004.048) - Z. Dvir, *On the size of Kakeya sets in finite fields*, J. Amer. Math. Soc. 22 (2009), 1093–1097. [DOI](https://doi.org/10.1090/S0894-0347-08-00607-3) - B. Bukh and T.-W. Chao, *Sharp density bounds on the finite field Kakeya problem*, Discrete Analysis 26 (2021). [DOI](https://doi.org/10.19086/da.30071) - G. Gardam, *A counterexample to the unit conjecture for group rings*, Ann. of Math. 194 (2021), 967–979. [DOI](https://doi.org/10.4007/annals.2021.194.3.9) - K. Saito, *Mills' constant is irrational*, Mathematika 71 (2025), e70027. [arXiv:2404.19461](https://arxiv.org/abs/2404.19461) - H. Wang and J. Zahl, *Volume estimates for unions of convex sets, and the Kakeya set conjecture in three dimensions*, [arXiv:2502.17655](https://arxiv.org/abs/2502.17655) - Google DeepMind, *Formal Conjectures*, Apache-2.0, [github.com/google-deepmind/formal-conjectures](https://github.com/google-deepmind/formal-conjectures) --- *Provenance note.* The Lean statements in this mission are adaptations of the Formal Conjectures library (Apache-2.0), rewritten to depend only on Mathlib and on this mission's own definition items, and checked to compile against the platform's Mathlib revision. Each draft item carries a read-back; **those read-backs are non-blind** — they were written by the same agent that drafted the statements, and each says so in its first line. They are documentation, not independent testimony.

42 thms2 active usersReviewed

Captain: Lucas

Gelbart's Langlands Survey I: Hecke's Correspondence between Automorphic Forms and Dirichlet SeriesResearch Paper

## Motivation The Langlands program proposes that the arithmetic of number fields is encoded in the representation theory of reductive groups over their adele rings. Its conjectures — reciprocity and functoriality — are stated in the survey this mission formalizes, [Gelbart 1984](https://doi.org/10.1090/S0273-0979-1984-15237-6), only after a long preparatory part on the classical results they generalize, and it is that classical part (Part II of the survey) that admits precise formal statements today. The classical engine is a theorem of **Hecke** (1936): a holomorphic function on the upper half-plane, given by a Fourier expansion in $e^{2\pi i n z/h}$, transforms in a prescribed way under $z \mapsto -1/z$ **exactly when** the Dirichlet series built from its Fourier coefficients continues analytically and satisfies a functional equation. One side of the equivalence is a symmetry of an analytic object on the upper half-plane; the other is an analytic property of a series assembled from arithmetic data. Gelbart presents this as the prototype of the "reciprocity" that the Langlands conjectures extend to $GL_n$ and beyond. Timeline of the material covered here. - 1859: Riemann derives the functional equation of $\zeta(s)$ from the transformation law of the Jacobi theta function, via the Mellin transform (Gelbart, §II.B.2, p. 187). - 1920s: Hasse and Minkowski establish the local-global principle for rational quadratic forms (Gelbart, §II.A, p. 186). - 1936: Hecke proves the equivalence that is this mission's goal, and characterizes Euler products among Dirichlet series of automorphic forms (Gelbart, §II.B.2, Theorems 1 and 2). - 1967: Weil extends Hecke's theorem to congruence subgroups; Langlands formulates functoriality. ## Setting Fix a sequence of complex numbers $a_0, a_1, a_2, \dots$ subject to the growth condition $a_n = O(n^c)$ for some $c > 0$, a period $h > 0$, a weight $k > 0$, and a sign $C = \pm 1$. Three objects are attached to this data. - The **form**: $\displaystyle f(z) = \sum_{n \ge 0} a_n e^{2\pi i n z/h}$, holomorphic on the upper half-plane $\{z : \operatorname{Im} z > 0\}$. - The **Dirichlet series**: $\displaystyle \varphi(s) = \sum_{n \ge 1} \frac{a_n}{n^s}$, absolutely convergent for $\operatorname{Re} s > c+1$. - The **completed series**: $\displaystyle \Phi(s) = \left(\frac{2\pi}{h}\right)^{-s} \Gamma(s)\, \varphi(s)$. Two conditions on this data are compared. $$\textbf{(A)}\quad \Phi(s) + \frac{a_0}{s} + \frac{C a_0}{k-s} \ \text{extends to an entire function, bounded in every vertical strip, and}\ \Phi(k-s) = C\,\Phi(s).$$ $$\textbf{(B)}\quad f(-1/z) = C\left(\frac{z}{i}\right)^{k} f(z) \qquad (\operatorname{Im} z > 0).$$ Condition (B) says that $f$ is automorphic of weight $k$ for the group of transformations generated by $z \mapsto z + h$ and $z \mapsto -1/z$; invariance under $z \mapsto z+h$ is built into the Fourier expansion. ## Formalization targets ### Goal — Theorem 1 (Hecke), p. 188 $$\textbf{(A)} \iff \textbf{(B)}$$ for every coefficient sequence of polynomial growth and all $h, k > 0$, $C = \pm 1$. The goal fixes no particular group, no level and no arithmetic input: it is the general equivalence, from which the classical examples follow by specialization. ### Milestones The milestone list follows the survey: the local-global principle of §II.A, the Riemann–theta computation that motivates Hecke's proof (§II.B.2, p. 187), the Mellin representation of $\Phi$, the two implications of Theorem 1 separately, and the Euler-product criterion of Theorem 2 (p. 189). ## Significance Hecke's theorem is what makes "this $L$-function is automorphic" a checkable assertion: it converts a statement about analytic continuation and a functional equation — often the only handle one has on an arithmetically defined Dirichlet series — into the existence of an automorphic form with prescribed Fourier coefficients. Weil's converse theorem, the modularity of elliptic curves, and the automorphy criteria used throughout the Langlands program are descendants of this statement. Downstream of it sit the classical applications listed in the survey: the functional equations of $\zeta$ and of Dirichlet $L$-functions, and the identification of theta series of quadratic forms with modular forms. Status. Hecke's theorem is a classical, fully proved result (Hecke 1936; a textbook treatment is Ogg, *Modular forms and Dirichlet series*, Ch. 1). Hasse–Minkowski is likewise classical. Neither has a formalization in Mathlib at the pinned revision: Mathlib supplies the completed Riemann zeta function and its functional equation, the Jacobi theta transformation law, `LSeries` and its abscissa theory, the Gamma function and the Mellin transform, and modular forms with `SlashAction`, but no converse theorem and no local-global principle for quadratic forms. What this mission produces is therefore new formal mathematics on top of an old result, not a re-derivation of something already machine-checked. ## Difficulty The forward implication (B) $\Rightarrow$ (A) is Riemann's argument: split $\int_0^\infty (f(iy) - a_0) y^{s-1}\,dy$ at $y = 1$, substitute $y \mapsto 1/y$ in the lower piece, and use (B). The obstacle is not the algebra but the analysis that licenses it: exchanging the sum defining $f$ with the integral, controlling $f(iy) - a_0$ as $y \to 0^{+}$, where the naive termwise bound diverges, and showing the result is entire *and* bounded on vertical strips rather than merely holomorphic on a half-plane. The reverse implication (A) $\Rightarrow$ (B) is harder, and it is where the first idea fails: one cannot simply run the computation backwards, because the Mellin inversion integral $\frac{1}{2\pi i}\int_{(\sigma)} \Phi(s) y^{-s}\,ds$ converges only once boundedness in vertical strips is combined with Stirling decay of $\Gamma$, and the contour shift that produces the $a_0$ terms needs both. Mathlib has the Mellin transform and an inversion theorem, under hypotheses that are not met verbatim here; supplying that bridge is the main work. ## Formalization scope Conventions committed to in Lean, all of them invisible in the prose. - $f$ is defined as an unconditional `tsum` over $n \ge 0$, so it takes the junk value $0$ where the series fails to converge; every statement about $f$ is guarded by $\operatorname{Im} z > 0$, and a separate item asserts summability there. - $\varphi$ is Mathlib's `LSeries`, whose $n = 0$ term is $0$ by definition, so $a_0$ never enters the Dirichlet series — only the correction terms $a_0/s$ and $C a_0/(k-s)$. - "Entire" is rendered as differentiability on all of $\mathbb{C}$; "bounded in every vertical strip" as: for all reals $\sigma_1, \sigma_2$ there is an $M$ bounding the function on $\sigma_1 \le \operatorname{Re} s \le \sigma_2$. - The functional equation is imposed on the *continued* function $F$ as $F(k-s) = C\,F(s)$; for $C = \pm 1$ this is equivalent to $\Phi(k-s) = C\,\Phi(s)$ on the half-plane of convergence. - Complex powers $(2\pi/h)^{-s}$, $(z/i)^{k}$ and $y^{s-1}$ are principal-branch `cpow`; on the upper half-plane $z/i$ has positive real part, so no branch ambiguity arises. - The growth hypothesis is $\lVert a_n \rVert \le K n^{c}$ for $n \ge 1$ with $c > 0$, and the abscissa used throughout is $\sigma = c+1$. - The printed source reads $\Phi(s) + a_0/s + C/(k-s)$; the term $C a_0/(k-s)$ used here is the standard form of the correction (see Ogg, Ch. 1), and the two agree when $a_0 = 0$. No trivializing reading is available: condition (A) requires the entire function to *agree with* $\Phi(s) + a_0/s + C a_0/(k-s)$ on $\operatorname{Re} s > c+1$, where $\Phi$ is genuinely defined, so it is not satisfied by an arbitrary entire function; and the hypotheses of the goal are satisfiable — the Jacobi theta coefficients with $h = 2$, $k = 1/2$, $C = 1$ are an instance, recorded as its own item. A complete development needs: summability and holomorphy of $q$-expansions of polynomial growth; the Mellin transform of an exponentially decaying series; entirety and strip-boundedness of the continued $\Phi$; Mellin inversion with Stirling control of $\Gamma$; and, for the Euler-product item, the passage from multiplicativity to an Euler product for `LSeries`. All of these are reusable beyond this mission. Contributions to any single item are welcome; the two implications of the goal are independently valuable and are listed as separate milestones for that reason. ## Selected references - S. Gelbart, *An elementary introduction to the Langlands program*, Bull. Amer. Math. Soc. (N.S.) **10** (1984), 177–219. https://doi.org/10.1090/S0273-0979-1984-15237-6 - E. Hecke, *Über die Bestimmung Dirichletscher Reihen durch ihre Funktionalgleichung*, Math. Ann. **112** (1936), 664–699. https://doi.org/10.1007/BF01565437 - A. Ogg, *Modular forms and Dirichlet series*, W. A. Benjamin, 1969. - R. P. Langlands, *Problems in the theory of automorphic forms*, Lectures in Modern Analysis and Applications III, Lecture Notes in Math. **170** (1970), 18–61. https://doi.org/10.1007/BFb0079065 - J.-P. Serre, *A course in arithmetic*, Springer GTM 7, 1973 (Ch. IV: Hasse–Minkowski).

12 thms2 active usersReviewed