MathOverflow

The 14 problem files in FormalConjectures/Mathoverflow that state a research or textbook statement, at commit 2055e5ad, one article each.

Their docstrings and Lean statements are quoted from Formal Conjectures (Google DeepMind) at that commit, under its Apache-2.0 license.

TheoremMathoverflow 1973#

Does the 6-sphere \(S^6\) admit the structure of a complex manifold?

References: - mathoverflow/1973, asked by user Fetchinson0234. - [Al26] L. Alpöge, A compact complex threefold fibred by tori over the projective line, and the six-sphere (2026), originally shared on X.

Quoted from FormalConjectures/Mathoverflow/1973.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 solved.

Mathoverflow1973.mathoverflow_1973

Solved: stated here; a Lean proof is at https://github.com/plby/HopfProblem/blob/9ac8a456b526527837d7082ff775213ca8bc9809/Solution.lean.

Does the 6-sphere admit a complex structure, i.e. an atlas of holomorphically compatible charts relating it to EuclideanSpace ℂ (Fin 3)? This is known as the Hopf Problem.

The answer is yes, see [Al26]. Formalisation of the proof by Boris Alexeev.

theorem mathoverflow_1973 :
    ∃ atlas : ChartedSpace (EuclideanSpace ℂ (Fin 3)) (unitSphere 6),
      IsManifold 𝓘(ℂ, EuclideanSpace ℂ (Fin 3)) 1 (unitSphere 6)

Category research solved; AMS 32 Several complex variables and analytic spaces. Declared in FormalConjectures/Mathoverflow/1973.lean, line 50.

Sources
LeanMathoverflow1973.mathoverflow_1973

TheoremOptimal monotone families for the discrete isoperimetric inequality#

References: - mathoverflow/10799 asked by user Gil Kalai - Optimal Monotone Families for the Discrete Isoperimetric Inequality by Gil Kalai (2026), a Polymath project with AI agents - An Isoperimetric Inequality for the Hamming Cube and Integrality Gaps in Bounded-Degree Graphs by Jeff Kahn and Gil Kalai (2006) - A Proof of the Kahn–Kalai Conjecture by Jinyoung Park and Huy Tuan Pham (2022)

Quoted from FormalConjectures/Mathoverflow/10799.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: 3 solved and 1 textbook result. It also has 9 test statements, counted here but not shown.

Mathoverflow10799.mathoverflow_10799

Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/408f53dc0856c0882a5e77acd24fc83b978f0bc9/FormalConjectures/Mathoverflow/10799.lean#L252.

Problem: For every monotone increasing family \(F\), given an interval \([s,t]\) of real numbers so that \(t/s > 1000 \log n\) we have some \(p\) in the interval \([s,t]\) so that \(F\) is optimal with respect to \(\mu_p\).

This was a "missing lemma" in the work of Kahn and Kalai on threshold behavior of monotone properties. The related Kahn–Kalai conjecture was settled by Park and Pham.

This conjecture is false without the additional assumption \(\mu_t(F) = 1/2\). A counterexample was found by Shlomo Perles (April 7, 2026).

theorem mathoverflow_10799 :
    ¬ ∀ (n : ℕ) (_ : 2 ≤ n)
    (F : Finset (Finset (Fin n))) (_ : IsMonotoneIncreasing F)
    (s t : ℝ) (_ : 0 < s) (_ : s ≤ t) (_ : t < 1)
    (_ : t / s > 1000 * Real.log n),
    ∃ p, s ≤ p ∧ p ≤ t ∧ IsOptimal p F

Category research solved; AMS 05 Combinatorics, 60 Probability theory and stochastic processes. Declared in FormalConjectures/Mathoverflow/10799.lean, line 178.

Mathoverflow10799.mathoverflow_10799.variants.kahn_kalai_conjecture_7

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/kahn-kalai-conjecture-7-counterexample/blob/5446d2f/lean/MO10799CounterexampleFC.lean#L2597-L2604.

Conjecture 7 from Kahn–Kalai 2006: a fixed-1000 variant of the original conjecture, with the additional assumption that \(t\) is the critical probability for \(F\), namely \(\mu_t(F) = 1/2\).

This variant is false by a counterexample due to Sahar Diskin and Uri Kreitner; see the MathOverflow discussion and the counterexample note. Their construction was adapted to this exact Formal Conjectures statement and formalized in Lean by Kenta Kitamura (KitaKen1).

theorem mathoverflow_10799.variants.kahn_kalai_conjecture_7 :
    ¬ ∀ (n : ℕ) (_ : 2 ≤ n)
    (F : Finset (Finset (Fin n))) (_ : IsMonotoneIncreasing F)
    (s t : ℝ) (_ : 0 < s) (_ : s ≤ t) (_ : t < 1)
    (_ : μFamily t F = 1 / 2)
    (_ : t / s > 1000 * Real.log n),
    ∃ p, s ≤ p ∧ p ≤ t ∧ IsOptimal p F

Category research solved; AMS 05 Combinatorics, 60 Probability theory and stochastic processes. Declared in FormalConjectures/Mathoverflow/10799.lean, line 202.

Mathoverflow10799.mathoverflow_10799.variants.weak_kahn_kalai

Solved: stated here without proof.

Weaker version proven by Kahn–Kalai (2006): for every fixed \(\varepsilon > 0\) there is a constant \(C = C_\varepsilon\) such that for every monotone increasing family \(F\) with critical probability \(t\), i.e. \(\mu_t(F) = 1/2\), there is some \(p \in [n^{-\varepsilon} t, t]\) for which \(F\) is \((C \log(1/p), p)\)-optimal.

theorem mathoverflow_10799.variants.weak_kahn_kalai :
    ∀ ε > (0 : ℝ), ∃ C > (0 : ℝ), ∀ (n : ℕ) (_ : 2 ≤ n)
    (F : Finset (Finset (Fin n))) (_ : IsMonotoneIncreasing F)
    (t : ℝ) (_ : 0 < t) (_ : t < 1) (_ : μFamily t F = 1 / 2),
    ∃ p, (n : ℝ) ^ (-ε) * t ≤ p ∧ p ≤ t ∧ IsOptimalWith C p F

Category research solved; AMS 05 Combinatorics, 60 Probability theory and stochastic processes. Declared in FormalConjectures/Mathoverflow/10799.lean, line 218.

Mathoverflow10799.discrete_isoperimetric_inequality

Textbook result, stated without proof.

Now a famous isoperimetric relation asserts that (IR) \(I^p(F) \ge \frac{1}{p} \mu_p(F) \log_p \mu_p(F)\) This relation holds for monotone increasing families \(F\) and \(0 < p < 1\). It is especially famous and simple when \(p=1/2\) and \(\mu_p(F)=1/2\). In this case, it says that given a set of half the vertices of the discrete cube \(2^X\), the number of edges between \(F\) and its complement is at least \(2^{n-1}\).

Note on translation: We use Real.logb p m to represent the logarithm base \(p\) directly. The factor of \(p\) in the denominator (equivalent to \(1/p\) in front) is consistent with the definition of IsOptimal used in the counterexample proof.

theorem discrete_isoperimetric_inequality (n : ℕ) (p : ℝ) (hp : 0 < p) (hp' : p < 1)
    (F : Finset (Finset (Fin n))) (hF : IsMonotoneIncreasing F) :
    let m := μFamily p F
    edgeBoundary n p F ≥ m * Real.logb p m / p

Category textbook; AMS 05 Combinatorics, 60 Probability theory and stochastic processes. Declared in FormalConjectures/Mathoverflow/10799.lean, line 238.

Sources
LeanMathoverflow10799.mathoverflow_10799 · Mathoverflow10799.mathoverflow_10799.variants.kahn_kalai_conjecture_7 · Mathoverflow10799.mathoverflow_10799.variants.weak_kahn_kalai · Mathoverflow10799.discrete_isoperimetric_inequality

TheoremMathoverflow 17560#

Reference: mathoverflow/17560 asked by user Alon-Amit

Quoted from FormalConjectures/Mathoverflow/17560.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 3 research or textbook statements: 1 open and 2 textbook results.

Mathoverflow17560.mathoverflow_17560

Open: stated without proof.

If \(2^x\) and \(3^x\) are integers, then \(x\) must be an integer.

theorem mathoverflow_17560 {x : ℝ} (hx : ∃ m : ℕ, (2 : ℝ) ^ x = m) (hx' : ∃ m : ℕ, (3 : ℝ) ^ x = m) :
    ∃ m : ℕ, x = m

Category research open; AMS 11 Number theory, 13 Commutative algebra. Declared in FormalConjectures/Mathoverflow/17560.lean, line 35.

Mathoverflow17560.mathoverflow_17560.variants.all_nats

Textbook result, stated without proof.

If for each natural number \(n\) the number \(n^x\) is an integer then \(x\) must also be an integer.

theorem mathoverflow_17560.variants.all_nats {x : ℝ} (hx : ∀ n : ℕ, ∃ m : ℕ, (n : ℝ) ^ x = m) :
    ∃ m : ℕ, x = m

Category textbook; AMS 11 Number theory, 13 Commutative algebra. Declared in FormalConjectures/Mathoverflow/17560.lean, line 43.

Mathoverflow17560.mathoverflow_17560.variants.with_5

Textbook result, stated without proof.

If \(2^x\), \(3^x\) and \(5^x\) are integers, then \(x\) must be an integer.

theorem mathoverflow_17560.variants.with_5 {x : ℝ} (hx : ∃ m : ℕ, (2 : ℝ) ^ x = m)
    (hx' : ∃ m : ℕ, (3 : ℝ) ^ x = m) (hx'' : ∃ m : ℕ, (5 : ℝ) ^ x = m) : ∃ m : ℕ, x = m

Category textbook; AMS 11 Number theory, 13 Commutative algebra. Declared in FormalConjectures/Mathoverflow/17560.lean, line 51.

Sources
LeanMathoverflow17560.mathoverflow_17560 · Mathoverflow17560.mathoverflow_17560.variants.all_nats · Mathoverflow17560.mathoverflow_17560.variants.with_5

TheoremMathoverflow 21003#

Is there any polynomial \(f(x, y) \in \mathbb{Q}[x, y]\) such that \(f : \mathbb{Q} \times \mathbb{Q} \rightarrow \mathbb{Q}\) is a bijection?

Reference: mathoverflow/21003 asked by user Z.H.

Quoted from FormalConjectures/Mathoverflow/21003.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.

Mathoverflow21003.mathoverflow_21003

Open: stated without proof.

Is there any polynomial \(f(x, y) \in \mathbb{Q}[x, y]\) such that \(f : \mathbb{Q} \times \mathbb{Q} \rightarrow \mathbb{Q}\) is a bijection?

theorem mathoverflow_21003 :
    ∃ f : MvPolynomial (Fin 2) ℚ, Function.Bijective fun x ↦ f.eval x

Category research open; AMS 12 Field theory and polynomials. Declared in FormalConjectures/Mathoverflow/21003.lean, line 42.

Sources
LeanMathoverflow21003.mathoverflow_21003

TheoremMathoverflow 31809#

Source: Mathoverflow/31809

References: - [CLLZ26] X.-W. Chen, J. Liu, X.-S. Lu and C. Zhang, "A pre-triangulated category which is not triangulated", arXiv:2608.09777

Quoted from FormalConjectures/Mathoverflow/31809.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 solved.

Mathoverflow31809.mathoverflow_31809

Solved: stated here without proof.

Does there exist a category that is pretriangulated but not triangulated?

Yes. Theorem 1.2 of [CLLZ26] twists the triangulated structure on the category of finitely generated projective modules over the preprojective algebra of type \(A_5\) over \(\mathbb{F}_2\). The result is pretriangulated but does not satisfy the octahedral axiom.

theorem mathoverflow_31809 : ¬ (∀ (C : Type*) [Category C] [Preadditive C]
    [HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive]
    [Pretriangulated C], IsTriangulated C)

Category research solved; AMS 18 Category theory; homological algebra. Declared in FormalConjectures/Mathoverflow/31809.lean, line 44.

Sources
LeanMathoverflow31809.mathoverflow_31809

TheoremMathoverflow 34145#

Can the unit square be covered by \(1/k\)-by-\(1/(k+1)\) rectangles (across \(1 \le k\) natural)?

I am deliberately not requiring that the rotations can only be \(0^\circ, 90^\circ, 180^\circ, \text{ or } 270^\circ\).

Because of indexing, since n : ℕ starts at 0, we change the side lengths to \(1 / (n + 1)\) and \(1 / (n + 2)\), so that the first rectangle is \(1/1\) by \(1/2\), the second is \(1/2\) by \(1/3\), etc.

Reference: mathoverflow/34145 asked by user Kaveh

Quoted from FormalConjectures/Mathoverflow/34145.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. It also has 6 test statements, counted here but not shown.

Mathoverflow34145.rectangles_cover_unit_square

Open: stated without proof.

Can a unit square be covered by rectangles of width 1 / (n + 1) and height 1 / (n + 2)?

theorem rectangles_cover_unit_square :
    ∃ c : Configuration, ∀ p ∈ unitSquare, ∃ n, p ∈ (c.rect n).toSet

Category research open; AMS 51 Geometry. Declared in FormalConjectures/Mathoverflow/34145.lean, line 146.

Mathoverflow34145.rectangles_pack_unit_square

Open: stated without proof.

Equivalently, can a unit square be packed with rectangles of width 1 / (n + 1) and height 1 / (n + 2)?

theorem rectangles_pack_unit_square :
    ∃ c : Configuration, (∀ n, (c.rect n).toSet ⊆ unitSquare) ∧ c.IsPacking

Category research open; AMS 51 Geometry. Declared in FormalConjectures/Mathoverflow/34145.lean, line 153.

Mathoverflow34145.rectangles_pack_square_133_div_132

Solved: stated here without proof.

It is known that packing the rectangles into a square of side length 133/132 is possible.

Reference: https://www.sciencedirect.com/science/article/pii/0097316594901163

theorem rectangles_pack_square_133_div_132 :
    (∃ c : Configuration,
      (∀ n, (c.rect n).toSet ⊆ Rectangle.toSet ⟨133/132, 133/132, (0, 0), 0⟩) ∧
      c.IsPacking)

Category research solved; AMS 51 Geometry. Declared in FormalConjectures/Mathoverflow/34145.lean, line 162.

Mathoverflow34145.rectangles_pack_square_501_div_500

Solved: stated here without proof.

It is known that packing the rectangles into a square of side length 501/500 is possible.

Reference: https://www.sciencedirect.com/science/article/pii/S0167506008706009

theorem rectangles_pack_square_501_div_500 :
    (∃ c : Configuration,
      (∀ n, (c.rect n).toSet ⊆ Rectangle.toSet ⟨501/500, 501/500, (0, 0), 0⟩) ∧
      c.IsPacking)

Category research solved; AMS 51 Geometry. Declared in FormalConjectures/Mathoverflow/34145.lean, line 173.

Sources
LeanMathoverflow34145.rectangles_cover_unit_square · Mathoverflow34145.rectangles_pack_unit_square · Mathoverflow34145.rectangles_pack_square_133_div_132 · Mathoverflow34145.rectangles_pack_square_501_div_500

TheoremMathoverflow 75792#

Various questions about integer complexity, which is the minimum number of 1s needed to express a natural number using addition, multiplication, and parentheses.

Let ‖n‖ denote the integer complexity of n > 0. * It is known that ‖3^n‖ = 3n for n > 0. * Is it true that ‖2^n‖ = 2n for n > 0? * The corresponding conjecture for 5 is false, because 5^6 = 15625 = 1 + 2^3 * 3^2 * (1 + 2^3 * 3^3)!

We have chosen to formalise this using an inductive type.

References: - mathoverflow/75792 by user Harry Altman - http://arxiv.org/abs/1203.6462 by Jānis Iraids, Kaspars Balodis, Juris Čerņenoks, Mārtiņš Opmanis, Rihards Opmanis, Kārlis Podnieks - http://arxiv.org/abs/1207.4841 by Harry Altman, Joshua Zelinsky - https://oeis.org/A5245 : Mahler-Popken complexity.

Quoted from FormalConjectures/Mathoverflow/75792.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 3 research or textbook statements: 1 open and 2 solved. It also has 15 test statements, counted here but not shown.

Mathoverflow75792.complexity_five_pow

Proved here.

Is 5n the complexity of 5^n for 0 < n? Answer: No.

theorem complexity_five_pow : ¬ ∀ n : ℕ, 0 < n → complexity (5 ^ n) = 5 * n

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Mathoverflow/75792.lean, line 204.

Mathoverflow75792.complexity_three_pow

Solved: stated here without proof.

Is 3n the complexity of 3^n for 0 < n? Answer: Yes, by John Selfridge.

Reference: https://arxiv.org/abs/1207.4841

theorem complexity_three_pow : ∀ n : ℕ, 0 < n → complexity (3 ^ n) = 3 * n

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Mathoverflow/75792.lean, line 213.

Mathoverflow75792.complexity_two_pow

Open: stated without proof.

Is 2n the complexity of 2^n for 0 < n?

theorem complexity_two_pow : ∀ n : ℕ, 0 < n → complexity (2 ^ n) = 2 * n

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Mathoverflow/75792.lean, line 218.

Sources
LeanMathoverflow75792.complexity_five_pow · Mathoverflow75792.complexity_three_pow · Mathoverflow75792.complexity_two_pow

TheoremMathoverflow 235893#

Reference: mathoverflow/235893 asked by user Willie Wong

Quoted from FormalConjectures/Mathoverflow/235893.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: 1 open and 1 solved. It also has 6 test statements, counted here but not shown.

Mathoverflow235893.mathoverflow_235893

Open: stated without proof.

Assume for \(n>1\), \(f:\mathbb{R}^n\to\mathbb{R}^n\) is a bijection, where \(\mathbb{R}^n\) is equipped with the standard topology. Does the connectedness of (the induced power set map) \(f\) imply that of \(f^{-1}\)?

theorem mathoverflow_235893 :
    ∀ n > 1, ∀ (f : ℝ^n ≃ ℝ^n), IsConnectedMap f → IsConnectedMap f.symm

Category research open; AMS 26 Real functions, 54 General topology. Declared in FormalConjectures/Mathoverflow/235893.lean, line 207.

Mathoverflow235893.mathoverflow_260589

Solved: stated here without proof.

There exists a connected bijection ℝ → ℝ^2 where the inverse is not connected, proven in mathoverflow/260589 by user Gro-Tsen.

theorem mathoverflow_260589 :
    ∃ f : ℝ ≃ ℝ^2, IsConnectedMap f ∧ ¬ IsConnectedMap f.symm

Category research solved; AMS 26 Real functions, 54 General topology. Declared in FormalConjectures/Mathoverflow/235893.lean, line 217.

Sources
LeanMathoverflow235893.mathoverflow_235893 · Mathoverflow235893.mathoverflow_260589

TheoremMathoverflow 339137#

Why do polynomials with coefficients 0,1 like to have only factors with 0,1 coefficients?

Reference: mathoverflow/339137 asked by user Sil

Quoted from FormalConjectures/Mathoverflow/339137.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: 1 open and 1 textbook result.

Mathoverflow339137.mathoverflow_339137

Open: stated without proof.

Let \(P(x), Q(x) ∈ ℝ[x]\) be two monic polynomials with non-negative coefficients. If \(R(x) = P(x)Q(x)\) is a \(0,1\) polynomial (coefficients only from \(\{0,1\}\)), then \(P(x)\) and \(Q(x)\) are also \(0, 1\) polynomials.

theorem mathoverflow_339137 (P Q R : ℝ[X]) (hP: P.Monic) (hQ : Q.Monic)
    (hp : ∀ c ∈ P.coeffs, 0 ≤ c) (hq : ∀ c ∈ Q.coeffs, 0 ≤ c)
    (h : R = P * Q) (hR : IsZeroOne R) :
    IsZeroOne P ∧ IsZeroOne Q

Category research open; AMS 12 Field theory and polynomials. Declared in FormalConjectures/Mathoverflow/339137.lean, line 53.

Mathoverflow339137.mathoverflow_339137_probabilistic

Textbook result, stated without proof.

Green's Open Problem 28 is the probabilistic reformulation of Mathoverflow 339137.

Suppose that \(X, Y\) are two finitely-supported independent random variables taking integer values, and such that \(X + Y\) is uniformly distributed on its range. Are \(X\) and \(Y\) themselves uniformly distributed on their ranges?

Mathematically, this equivalence is established via Probability Generating Functions (PGFs), shifting the support to \(\mathbb{N}\), and appropriately scaling the coefficients.

theorem mathoverflow_339137_probabilistic :
    type_of% Mathoverflow339137.mathoverflow_339137 ↔ type_of% Green28.green_28

Category textbook; AMS 60 Probability theory and stochastic processes. Declared in FormalConjectures/Mathoverflow/339137.lean, line 70.

Sources
LeanMathoverflow339137.mathoverflow_339137 · Mathoverflow339137.mathoverflow_339137_probabilistic

TheoremMathoverflow 347178#

Reference: mathoverflow/347178 asked by user Biagio Ricceri

Quoted from FormalConjectures/Mathoverflow/347178.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 3 research or textbook statements: 3 solved.

Mathoverflow347178.mathoverflow_347178

Solved: stated here; a Lean proof is at https://github.com/google-deepmind/formal-conjectures/blob/fc20c0b55eab6fc26e2bb5b24fb3005303a0910b/FormalConjectures/Mathoverflow/347178.lean#L670.

Let \(f : \mathbb R^n \to \mathbb R, n \geq 2\) be a \(C^1\) function. Is it true that

\[\sup_{x \in \mathbb R^n}f(x) = \sup_{x\in \mathbb R^n} f(x+\nabla f(x))\]

?

Answer: No. A counterexample in \(\mathbb R^2\) is recorded in the linked formal proof.

theorem mathoverflow_347178 :
    ¬ ∀ᵉ (n ≥ 2) (f : ℝ^n → ℝ) (_ : ContDiff ℝ 1 f),
        (BddAbove (range f) ↔ BddAbove (range (fun x ↦ f (x + gradient f x)))) ∧
        (⨆ x, (f x : EReal)) = ⨆ x, (f (x + gradient f x) : EReal)

Category research solved; AMS 26 Real functions. Declared in FormalConjectures/Mathoverflow/347178.lean, line 44.

Mathoverflow347178.mathoverflow_347178.variants.bounded_iff

Solved: stated here; a Lean proof is at https://github.com/google-deepmind/formal-conjectures/blob/fc20c0b55eab6fc26e2bb5b24fb3005303a0910b/FormalConjectures/Mathoverflow/347178.lean#L690.

Let \(f : \mathbb R^n \to \mathbb R, n \geq 2\) be a \(C^1\) function. Is the boundedness of \(\sup_{x \in \mathbb R^n}f(x)\) and \(\sup_{x\in \mathbb R^n} f(x+\nabla f(x))\) equivalent?

Answer: No. The same counterexample is recorded in the linked formal proof.

theorem mathoverflow_347178.variants.bounded_iff :
    ¬ ∀ᵉ (n ≥ 2) (f : ℝ^n → ℝ) (_ : ContDiff ℝ 1 f),
        BddAbove (range f) ↔ BddAbove (range fun x ↦ f (x + gradient f x))

Category research solved; AMS 26 Real functions. Declared in FormalConjectures/Mathoverflow/347178.lean, line 60.

Mathoverflow347178.mathoverflow_347178.variants.bounded_only

Solved: stated here; a Lean proof is at https://github.com/inozemtsev/gradient-supremum/blob/56743ea06dd2953e02274841c16e0f56927b5a44/GradientSupremum/Mathoverflow347178.lean#L30.

Let \(f : \mathbb R^n \to \mathbb R, n \geq 2\) be a \(C^1\) function. Does the equality

\[\sup_{x \in \mathbb R^n}f(x) = \sup_{x\in \mathbb R^n} f(x+\nabla f(x))\]

hold when both suprema are finite?

Answer: Yes. Upper boundedness of \(f\) alone suffices.

theorem mathoverflow_347178.variants.bounded_only :
    ∀ᵉ (n ≥ 2) (f : ℝ^n → ℝ) (hf : ContDiff ℝ 1 f)
        (h : BddAbove (range f)) (h' : BddAbove (range (fun x ↦ f (x + gradient f x)))),
        (⨆ x, f x) = ⨆ x, f (x + gradient f x)

Category research solved; AMS 26 Real functions. Declared in FormalConjectures/Mathoverflow/347178.lean, line 76.

Sources
LeanMathoverflow347178.mathoverflow_347178 · Mathoverflow347178.mathoverflow_347178.variants.bounded_iff · Mathoverflow347178.mathoverflow_347178.variants.bounded_only

TheoremAre prime numbers among sums of prime numbers distributed as \(\frac n{2\ln(n)}\)?#

Reference:

mathoverflow.net/questions/434111

[Me18] Meštrović, R., Curious Conjectures on the Distribution of Primes Among the Sums of the First 2n Primes, arXiv:1804.04198 (2018), Conjecture 3.3.

Quoted from FormalConjectures/Mathoverflow/434111.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 open.

MathOverflow434111.restricted_prime_number_theorem

Open: stated without proof.

The conjecture claims that \(\pi_n\sim\frac n{2\ln(n)}\).

In other words, primes are distributed among the much sparser sequence \((S_n)_n\) with essentially the same density as in the positive integers, up to a factor of \(2\).

MathOverflow 434111.

[Me18] Meštrović, R., Curious Conjectures on the Distribution of Primes Among the Sums of the First 2n Primes, arXiv:1804.04198 (2018).

theorem restricted_prime_number_theorem :
    ((fun n : ℕ => (piRestricted n : ℝ)) ~[atTop] (fun n : ℕ => (n : ℝ) / (2 * Real.log n)))

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Mathoverflow/434111.lean, line 60.

MathOverflow434111.restricted_prime_number_theorem.variants.even_subsequence

Open: stated without proof.

Meštrović's original formulation [Me18, Conjecture 3.3]: the sequence of sums of the first \(2m\) primes satisfies the Restricted Prime Number Theorem, \(\pi(m, (S_{2m})) \sim \frac{m}{\ln m}\).

theorem restricted_prime_number_theorem.variants.even_subsequence :
    ((fun m : ℕ => (((Finset.Icc 1 m).filter (fun k => Nat.Prime (S (2 * k)))).card : ℝ)) ~[atTop]
      (fun m : ℕ => (m : ℝ) / Real.log m))

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Mathoverflow/434111.lean, line 69.

Sources
LeanMathOverflow434111.restricted_prime_number_theorem · MathOverflow434111.restricted_prime_number_theorem.variants.even_subsequence

TheoremMathoverflow 486451#

Reference: mathoverflow/486451 asked by user Junyan Xu

Quoted from FormalConjectures/Mathoverflow/486451.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.

Mathoverflow486451.exists_semiring_unique_left_maximal_not_unique_right_maximal

Solved: stated here without proof.

There exists a semiring with a unique left maximal ideal but more than one right maximal ideals.

theorem exists_semiring_unique_left_maximal_not_unique_right_maximal :
    ∃ (R : Type) (_ : Semiring R), (∃! I : Ideal R, I.IsMaximal) ∧
      ∃ I J : Ideal Rᵐᵒᵖ, I.IsMaximal ∧ J.IsMaximal ∧ I ≠ J

Category research solved; AMS 16 Associative rings and algebras. Declared in FormalConjectures/Mathoverflow/486451.lean, line 32.

Mathoverflow486451.exists_semiring_unique_left_right_maximal_ne

Solved: stated here; a Lean proof is at https://github.com/google-deepmind/formal-conjectures/blob/f7502b9ed3e32d193ab8fee53d2e28f7d67f2dc3/FormalConjectures/Mathoverflow/486451.lean#L333.

There exists a semiring with a unique left maximal ideal and a unique right maximal ideal which are not the same as sets.

This has been shown by Goran Žužić and Moritz Firsching using an experimental pipeline: An example is the monoid algebra of the monoid of maps from \(\mathbb{N}\) to \(\mathbb{N}\) over \(\mathbb{N}\).

theorem exists_semiring_unique_left_right_maximal_ne :
    ∃ (R : Type) (_ : Semiring R) (hI : ∃! I : Ideal R, I.IsMaximal)
      (hJ : ∃! J : Ideal Rᵐᵒᵖ, J.IsMaximal),
        (hI.choose : Set R) ≠ MulOpposite.op ⁻¹' hJ.choose

Category research solved; AMS 16 Associative rings and algebras. Declared in FormalConjectures/Mathoverflow/486451.lean, line 46.

Sources
LeanMathoverflow486451.exists_semiring_unique_left_maximal_not_unique_right_maximal · Mathoverflow486451.exists_semiring_unique_left_right_maximal_ne

TheoremMathoverflow 507128#

Reference: mathoverflow/507128 asked by user Junyan Xu

Quoted from FormalConjectures/Mathoverflow/507128.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 solved.

Mathoverflow507128.exists_isFractionRing_self_ideal_ne_top_invertible

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/mo507128-lean/blob/e9507429c01c4288089e4af1c92a03b7d1e17f74/MO507128.lean#L265.

There exists a proper ideal I in a (commutative) total ring R of fractions that is an invertible module. If I ⊊ R is such an example, I must have infinite order in the Picard group. Moreover, R must not be Noetherian (otherwise it must be semi-local and therefore have trivial Picard group).

The linked formal proof gives the following explicit construction.

Let D = ℂ[X, Y] / (Y² - X³) be the coordinate ring of the cuspidal cubic. Let P = (X - 1, Y - 1), which is an invertible ideal. Let M be the direct sum of the evaluation fibres at cusp parameters r ≠ 1. Form the idealization R = D ⋉ M. The desired ideal is the range of the multiplication map R ⊗[D] P → R.

theorem exists_isFractionRing_self_ideal_ne_top_invertible :
    ∃ (R : Type) (_ : CommRing R) (_ : IsFractionRing R R) (I : Ideal R),
      I ≠ ⊤ ∧ Module.Invertible R I

Category research solved; AMS 13 Commutative algebra. Declared in FormalConjectures/Mathoverflow/507128.lean, line 46.

Sources
LeanMathoverflow507128.exists_isFractionRing_self_ideal_ne_top_invertible

TheoremMathOverflow 508539#

Edge-vertex inequality \(EV \geq 4^{n-1}\).

References: - MathOverflow 508539, asked by Paata Ivanisvili. - [DIRX26] Durcik, P., Ivanisvili, P., Roos, J., and Xie, X., Sharp isoperimetric inequalities on the Hamming cube II: The critical exponent (2026), arXiv:2602.20462, inequality (1.2).

Quoted from FormalConjectures/Mathoverflow/508539.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 solved. It also has 2 test statements, counted here but not shown.

Mathoverflow508539.mathoverflow_508539

Solved: stated here without proof.

For any set \(A \subset \{0,1\}^n\) of half size \(2^{n-1}\), we have \(EV \geq 4^{n-1}\), where \(E\) denotes the edge boundary (the number of edges between \(A\) and its complement), and \(V\) denotes the inner vertex boundary (the number of points in \(A\) having a neighbor outside \(A\)).

This is the half-size case of [DIRX26, (1.2)]. The hypothesis \(n > 0\) is necessary: in dimension zero the cardinality hypothesis allows the whole cube, whose boundaries are empty.

theorem mathoverflow_508539 {n : ℕ} (A : Finset (Fin n → Bool))
    (hA : #A = 2 ^ (n - 1)) (hn : 0 < n) :
    4 ^ (n - 1) ≤ #((hypercube n).edgeBoundary A) *
      #((hypercube n).innerVertexBoundary A)

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Mathoverflow/508539.lean, line 66.

Sources
LeanMathoverflow508539.mathoverflow_508539

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.