Green's Open Problem 87 to Ben Green's Open Problem 97
TheoremGreen's Open Problem 87#
References: - [Gr24] Green, Ben. "100 open problems." (2024). - [BW15] Britnell, John R., and Mark Wildon. "Computing derangement probabilities of the symmetric group acting on k-sets." arXiv preprint arXiv:1511.04106 (2015). - [EFG16] Eberhard, Sean, Kevin Ford, and Ben Green. "Permutations fixing a k-set." International Mathematics Research Notices 2016.21 (2016): 6713-6731. arXiv:1507.04465. - [GS26] Green, Ben, and Mehtaab Sawhney. "The proportion of permutations fixing a k-set." arXiv preprint arXiv:2604.28116 (2026). - [Ve26] Veljjanoski, Daniel. "p(k) for permutations fixing a k-set: values and checks for k ≤ 121." https://github.com/veljjanoski/green87-fixing-k-set (2026).
Quoted from FormalConjectures/GreensOpenProblems/87.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 4 research or textbook statements: 2 open and 2 solved.
Green87.green_87.variants.exists_tendsto
Solved: stated here without proof.
For every \(k\), \(i(n, k)\) converges as \(n \to \infty\) [BW15, Section 2]; the limit is \(p(k)\) in Green's notation. It is the probability that the random multiset with \(\mathrm{Pois}(1/j)\) parts of size \(j\) (\(1 \le j \le k\), independent) has a sub-multiset of total size \(k\).
theorem green_87.variants.exists_tendsto (k : ℕ) :
∃ L : ℝ, Tendsto (fun n ↦ i n k) atTop (𝓝 L)
Category research solved; AMS 05 Combinatorics, 20 Group theory and generalizations, 60 Probability theory and stochastic processes. Declared in FormalConjectures/GreensOpenProblems/87.lean, line 56.
Green87.green_87.decreasing
Open: stated without proof.
Let \(p(k)\) be the limit, as \(n \to \infty\), of the probability that a random permutation of \([n]\) preserves some set of size \(k\). Is \(p(k)\) a decreasing function of \(k\)?
This is a conjecture of Peter Cameron (2010), see [BW15]. The statement is taken in the strict sense, as in [BW15]: they verified \(p(k) > p(k + 1)\) for \(k < 30\), and the values computed numerically in [Ve26] satisfy it for \(k < 121\). Note \(p(0) = 1\), since the empty set is always fixed, and \(p(1) = 1 - 1/e\). The limit \(p\) is quantified inside the statement; it exists and is unique by
green_87.variants.exists_tendsto.
theorem green_87.decreasing :
∀ p : ℕ → ℝ, (∀ k, Tendsto (fun n ↦ i n k) atTop (𝓝 (p k))) → StrictAnti p
Category research open; AMS 05 Combinatorics, 20 Group theory and generalizations, 60 Probability theory and stochastic processes. Declared in FormalConjectures/GreensOpenProblems/87.lean, line 73.
Green87.green_87.variants.order
Solved: stated here without proof.
\(p(k)\) is bounded above and below by constant multiples of \(k^{-\delta} (\log k)^{-3/2}\). [EFG16, Theorem 1.1] proves this for \(i(n, k)\) uniformly in \(1 \le k \le n/2\) (with \((1 + \log k)^{-3/2}\)); letting \(n \to \infty\) gives the statement for \(p\).
theorem green_87.variants.order :
∀ p : ℕ → ℝ, (∀ k, Tendsto (fun n ↦ i n k) atTop (𝓝 (p k))) →
p =Θ[atTop] fun k : ℕ ↦ (k : ℝ) ^ (-δ) * (Real.log k) ^ (-(3 / 2 : ℝ))
Category research solved; AMS 05 Combinatorics, 20 Group theory and generalizations, 60 Probability theory and stochastic processes. Declared in FormalConjectures/GreensOpenProblems/87.lean, line 81.
Green87.green_87.asymptotic
Open: stated without proof.
Is \(p(k) = (C + o(1)) k^{-\delta} (\log k)^{-3/2}\) for some absolute constant \(C\)?
Green and Sawhney [GS26] proved \(p(k) = (1 + o(1)) f(\{\log_2 k\}) k^{-\delta} (\log k)^{-3/2}\) for an explicit smooth, positive \(f\) on \(\mathbb{R} / \mathbb{Z}\) with \(\max f / \min f < 1 + 2 \cdot 10^{-7}\). The question is therefore equivalent to whether \(f\) is constant; they conjecture that it is not, so the expected answer is no, but this has not been proved.
theorem green_87.asymptotic :
∀ p : ℕ → ℝ, (∀ k, Tendsto (fun n ↦ i n k) atTop (𝓝 (p k))) →
∃ C : ℝ, 0 < C ∧
p ~[atTop] fun k : ℕ ↦ C * (k : ℝ) ^ (-δ) * (Real.log k) ^ (-(3 / 2 : ℝ))
Category research open; AMS 05 Combinatorics, 20 Group theory and generalizations, 60 Probability theory and stochastic processes. Declared in FormalConjectures/GreensOpenProblems/87.lean, line 94.
Sources
TheoremBen Green's Open Problem 88#
References: - [Gr24] Ben Green's Open Problem 88 - [GoLo21] The length of an \(s\)-increasing sequence of \(r\)-tuples by W. T. Gowers and J. Long
Quoted from FormalConjectures/GreensOpenProblems/88.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 1 research or textbook statement: 1 open.
Green88.green_88
Open: stated without proof.
[Gr24, Problem 88]: Is there an absolute constant \(\delta > 0\) such that every pairwise \(2\)-comparable set \(S \subseteq [N]^3\) satisfies \(|S| \leq N^{2 - \delta}\)?
theorem green_88 :
∃ δ > (0 : ℝ), ∀ (N : ℕ) (S : Finset (Fin 3 → Fin N)),
(S : Set (Fin 3 → Fin N)).Pairwise IsComparable₂ →
(S.card : ℝ) ≤ (N : ℝ) ^ (2 - δ)
Category research open; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/GreensOpenProblems/88.lean, line 44.
Sources
TheoremBen Green's Open Problem 93#
References: - [Gr24] Green, Ben. "100 open problems." (2024). - [BrVa19] Breuillard, E. and Varjú, P. P., Irreducibility of random polynomials of large degree. Acta Math. 223 (2019), 195--249. arXiv:1810.13360 - [BSKK23] Bary-Soroker, L., Koukoulopoulos, D. and Kozma, G., Irreducibility of random polynomials: general measures. Invent. Math. 233 (2023), 1041--1120. arXiv:2007.14567 - [Ko99] Konyagin, S. V., On the number of irreducible polynomials with 0,1 coefficients. Acta Arith. 88 (1999), 333--350.
Quoted from FormalConjectures/GreensOpenProblems/93.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 5 research or textbook statements: 1 open and 4 solved. It also has 2 API statements, counted here but not shown.
Green93.green_93
Open: stated without proof.
Is a random polynomial with coefficients in \(\{0,1\}\) and nonzero constant term almost surely irreducible?
More precisely, writing \(p_n\) for the probability that \(1 + a_1 x + \cdots + a_{n-1} x^{n-1} + x^n\) is irreducible, where the \(a_i\) are independent and take the values \(0\) and \(1\) with equal probability, does \(p_n \to 1\)?
The probability \(p_n\) is
irreducibleProb 1 n. The conjecture is due to Odlyzko and Poonen [BrVa19, Section 1].
theorem green_93 : Tendsto (fun n : ℕ ↦ irreducibleProb 1 n) atTop (𝓝 1)
Category research open; AMS 11 Number theory, 12 Field theory and polynomials, 60 Probability theory and stochastic processes. Declared in FormalConjectures/GreensOpenProblems/93.lean, line 99.
Green93.green_93.variants.konyagin
Solved: stated here without proof.
Konyagin [Ko99] proved that \(p_n \ge c / \log n\) for an absolute constant \(c > 0\), as stated in [BrVa19, Section 1]. We state it for all large \(n\). It is superseded by
green_93.variants.bskk_small.
theorem green_93.variants.konyagin :
∃ c : ℝ, 0 < c ∧ ∀ᶠ n : ℕ in atTop, c / Real.log (n : ℝ) ≤ irreducibleProb 1 n
Category research solved; AMS 11 Number theory, 12 Field theory and polynomials, 60 Probability theory and stochastic processes. Declared in FormalConjectures/GreensOpenProblems/93.lean, line 108.
Green93.green_93.variants.bskk_small
Solved: stated here without proof.
Bary-Soroker, Koukoulopoulos and Kozma [BSKK23, Theorem 1(b)] proved that a random monic polynomial of degree \(n\) whose coefficients are uniform on \(N\) consecutive integers in \([-H, H]\) with \(2 \le N \le 34\), and with nonzero constant term, is irreducible with probability at least \(\delta\). Here \(\delta > 0\) is an absolute constant, and \(n\) must be at least an absolute constant and at least \((\log H)^3\). We state it for the integers \(\{0, 1, \dots, M\}\) with \(1 \le M \le 33\), so \(N = M + 1\) and \(H = M\). The condition on \((\log H)^3\) is absorbed into \(n_0\), because \(M\) is bounded. The case \(M = 1\) gives \(p_n \ge \delta\) for large \(n\) for the polynomial of
green_93.
theorem green_93.variants.bskk_small :
∃ δ : ℝ, 0 < δ ∧ ∃ n₀ : ℕ, ∀ M n : ℕ, 1 ≤ M → M ≤ 33 → n₀ ≤ n →
δ ≤ irreducibleProb M n
Category research solved; AMS 11 Number theory, 12 Field theory and polynomials, 60 Probability theory and stochastic processes. Declared in FormalConjectures/GreensOpenProblems/93.lean, line 123.
Green93.green_93.variants.bskk_large
Solved: stated here without proof.
Bary-Soroker, Koukoulopoulos and Kozma [BSKK23, Theorem 1(a)] proved that a random monic polynomial of degree \(n\) whose coefficients are uniform on \(N \ge 35\) consecutive integers in \([-H, H]\), with nonzero constant term, is irreducible with probability at least \(1 - n^{-c}\). Here \(c > 0\) is an absolute constant, and \(n\) must be at least an absolute constant and at least \((\log H)^3\). We state it for the integers \(\{0, 1, \dots, M\}\) with \(M \ge 34\), so \(N = M + 1 \ge 35\) and \(H = M\). In particular
irreducibleProb M n\(\to 1\) for each such \(M\), which is the analogue ofgreen_93for coefficients in \(\{0, \dots, M\}\).
theorem green_93.variants.bskk_large :
∃ c : ℝ, 0 < c ∧ ∃ n₀ : ℕ, ∀ M n : ℕ, 34 ≤ M → n₀ ≤ n → (Real.log (M : ℝ)) ^ 3 ≤ n →
1 - (n : ℝ) ^ (-c) ≤ irreducibleProb M n
Category research solved; AMS 11 Number theory, 12 Field theory and polynomials, 60 Probability theory and stochastic processes. Declared in FormalConjectures/GreensOpenProblems/93.lean, line 139.
Green93.green_93.variants.breuillard_varju
Solved: stated here without proof.
Breuillard and Varjú. Assume the Riemann hypothesis for the Dedekind zeta functions of all number fields \(\mathbb{Q}(a)\) with \(a\) a root of a polynomial with coefficients in \(\{0, 1\}\) (
ZeroOneRootFieldsRH). Then \(p_n \to 1\) [BrVa19, Theorem 1].
theorem green_93.variants.breuillard_varju :
ZeroOneRootFieldsRH → Tendsto (fun n : ℕ ↦ irreducibleProb 1 n) atTop (𝓝 1)
Category research solved; AMS 11 Number theory, 12 Field theory and polynomials, 60 Probability theory and stochastic processes. Declared in FormalConjectures/GreensOpenProblems/93.lean, line 163.
Sources
TheoremBen Green's Open Problem 94#
Reference: - Ben Green's Open Problem 94 - erdosproblems.com/120 - [OAI26a] OpenAI, The dyadic case of the Erdős similarity conjecture. OpenAI Math Release preprint (2026). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-dyadic-case-of-the-Erdos-similarity-conjecture-September-25-2026/paper.pdf
Quoted from FormalConjectures/GreensOpenProblems/94.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 2 research or textbook statements: 2 solved.
Green94.green_94_outer_measure
Solved: stated here; a Lean proof is at https://github.com/google-deepmind/formal-conjectures/blob/153d79d6c82c76fe1bee860742af800840c974d9/FormalConjectures/GreensOpenProblems/94.lean#L174.
Let
A ⊂ Rbe a set of positive outer measure. Does \(A\) contain an affine copy of{1, 1/2, 1/4, . . . }?The answer is "no".
theorem green_94_outer_measure :
¬ ∀ A : Set ℝ,
volume A > 0 →
∃ a b : ℝ, a ≠ 0 ∧ ∀ n : ℕ, a * (1 / 2^n) + b ∈ A
Category research solved; AMS 28 Measure and integration. Declared in FormalConjectures/GreensOpenProblems/94.lean, line 44.
Green94.green_94
Solved: stated here; a Lean proof is at https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/MeasureTheory/DyadicAvoidance/Main.lean#L103.
Let
A ⊂ Rbe a set of positive measure. Does \(A\) contain an affine copy of{1, 1/2, 1/4, . . . }?The answer is "no": there are compact sets of measure arbitrarily close to \(1\) in \([0, 1]\) that contain no affine copy of \(\{2^{-n} : n \geq 1\}\). This was proved by an internal OpenAI model in September 2026 [OAI26a]; see the linked Lean proof.
theorem green_94 :
¬ ∀ A : Set ℝ,
MeasurableSet A ∧ volume A > 0 →
∃ a b : ℝ, a ≠ 0 ∧ ∀ n : ℕ, a * (1 / 2^n) + b ∈ A
Category research solved; AMS 28 Measure and integration. Declared in FormalConjectures/GreensOpenProblems/94.lean, line 60.
Sources
TheoremBen Green's Open Problem 97#
References: - [Gr24] Green, Ben. "100 open problems." (2024). - [Si23] Simkin, M., The number of \(n\)-queens configurations. Adv. Math. 427 (2023), Paper No. 109127. arXiv:2107.13460 - [BoKe21] Bowtell, C. and Keevash, P., The \(n\)-queens problem. arXiv:2109.08083 (2021). - [NAB23] Nobel, P., Agrawal, A. and Boyd, S., Computing tighter bounds on the \(n\)-queens constant via Newton's method. Optim. Lett. 17 (2023), 1229--1240. arXiv:2112.03336 - [EMM19] Eberhard, S., Manners, F. and Mrazović, R., Additive triples of bijections, or the toroidal semiqueens problem. J. Eur. Math. Soc. 21 (2019), 441--463. arXiv:1510.05987
Quoted from FormalConjectures/GreensOpenProblems/97.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 6 research or textbook statements: 3 open and 3 solved. It also has 3 test statements, counted here but not shown.
Green97.green_97
Open: stated without proof.
In how many ways (asymptotically) \(Q(n)\) may \(n\) non-attacking queens be placed on an \(n \times n\) chessboard?
This is the \(n\)-queens problem, see [Gr24, Problem 97]. We read "asymptotically" as: find an explicit function
green_97.answerwith \(Q(n) \sim\)green_97.answer n. The function \(n \mapsto Q(n)\) itself is not an explicit answer. [Gr24] notes that an asymptotic "rather than an asymptotic for the log" is open. What is known is \(Q(n) = ((1+o(1))\, n e^{-\alpha})^n\) for a constant \(1.94 < \alpha < 1.9449\) [Si23], seegreen_97.variants.simkin.
theorem green_97 :
(fun n : ℕ ↦ (numQueens n : ℝ)) ~[atTop] green_97.answer
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/GreensOpenProblems/97.lean, line 122.
Green97.green_97.variants.simkin
Solved: stated here without proof.
Simkin's theorem. There is a constant \(1.94 < \alpha < 1.9449\) such that
\[\lim_{n \to \infty} \frac{Q(n)^{1/n}}{n} = e^{-\alpha},\]that is, \(Q(n) = ((1+o(1))\, n e^{-\alpha})^n\) [Si23, Theorem 1.1]. The constant \(\alpha\) is defined in [Si23] as the solution of a convex optimisation problem over Borel probability measures on the square \([-1/2, 1/2]^2\). The limit determines \(\alpha\) uniquely. Nobel, Agrawal and Boyd [NAB23] combined Simkin's formulation with a sharper bound of Knuth, solved the resulting convex problems numerically, and report the tighter range \(\alpha \in [1.944000752, 1.944001082]\).
theorem green_97.variants.simkin :
∃ α : ℝ, 1.94 < α ∧ α < 1.9449 ∧
Tendsto (fun n : ℕ ↦ (numQueens n : ℝ) ^ ((1 : ℝ) / n) / n) atTop
(𝓝 (Real.exp (-α)))
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/GreensOpenProblems/97.lean, line 137.
Green97.green_97.variants.alpha
Open: stated without proof.
Find an explicit value for the constant \(\alpha\) of
green_97.variants.simkin, that is, the number with \(Q(n)^{1/n}/n \to e^{-\alpha}\).[Gr24] writes that "an explicit solution remains an open problem". The value \(\alpha\) is the solution of an entropy optimisation problem [Si23]. As for
green_97, an explicit closed form is intended.
theorem green_97.variants.alpha :
Tendsto (fun n : ℕ ↦ (numQueens n : ℝ) ^ ((1 : ℝ) / n) / n) atTop
(𝓝 (Real.exp (-green_97.variants.alpha.answer)))
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/GreensOpenProblems/97.lean, line 154.
Green97.green_97.variants.bowtell_keevash
Solved: stated here without proof.
Bowtell and Keevash. For \(n \equiv 1, 5 \pmod 6\) the number of toroidal \(n\)-queens configurations satisfies \(T(n) = ((1+o(1))\, n e^{-3})^n\) [BoKe21, Theorem 1.2]. The filter
toroidalDegreesrestricts to these \(n\), because \(T(n) = 0\) for all other \(n \ge 1\).
theorem green_97.variants.bowtell_keevash :
Tendsto (fun n : ℕ ↦ (numToroidalQueens n : ℝ) ^ ((1 : ℝ) / n) / n) toroidalDegrees
(𝓝 (Real.exp (-3)))
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/GreensOpenProblems/97.lean, line 165.
Green97.green_97.variants.toroidal
Open: stated without proof.
Find an asymptotic for the number \(T(n)\) of toroidal \(n\)-queens configurations, for \(n \equiv 1, 5 \pmod 6\).
[Gr24] writes, after the result of [BoKe21], that the problem of "obtaining an asymptotic (rather than an asymptotic for the log) remains open". [BoKe21] proved the asymptotic of the logarithm, see
green_97.variants.bowtell_keevash. We read "asymptotic" as forgreen_97: an explicit function is intended.
theorem green_97.variants.toroidal :
(fun n : ℕ ↦ (numToroidalQueens n : ℝ)) ~[toroidalDegrees]
green_97.variants.toroidal.answer
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/GreensOpenProblems/97.lean, line 182.
Green97.green_97.variants.eberhard_manners_mrazovic
Solved: stated here without proof.
Eberhard, Manners and Mrazović. For odd \(n\), the number \(s_n\) of pairs \((\pi_1, \pi_2)\) of bijections \(\{1, \dots, n\} \to \mathbb{Z}/n\mathbb{Z}\) with \(\pi_1 + \pi_2\) also a bijection is
\[s_n = (e^{-1/2} + o(1))\, \frac{(n!)^3}{n^{n-1}}\][EMM19, Theorem 1.2]. [Gr24] refers to this paper for the variant of the toroidal question where only \(\pi_1\), \(\pi_2\) and \(\pi_1 - \pi_2\) are required to be bijections. Replacing \(\pi_2\) by \(-\pi_2\) shows that this variant has the same count \(s_n\). For even \(n\), \(s_n = 0\) [EMM19, Section 1], so the theorem is stated for odd \(n\).
theorem green_97.variants.eberhard_manners_mrazovic :
(fun n : ℕ ↦ (numAdditiveTriples n : ℝ)) ~[atTop ⊓ Filter.principal {n : ℕ | Odd n}]
fun n : ℕ ↦ Real.exp (-(1 / 2)) * ((n ! : ℕ) : ℝ) ^ 3 / (n : ℝ) ^ (n - 1)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/GreensOpenProblems/97.lean, line 208.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.