Simple zeros of the Riemann… to Zagier's Conjecture on Multiple…

TheoremSimple zeros of the Riemann zeta function on the critical line#

References: - [Cl26] Claude (Anthropic), More than two thirds of the zeros of the Riemann zeta function are simple and on the critical line, August 2026. pdf, Lean formalisation. - Wikipedia

For a nontrivial zero ρ = β + iγ of ζ (or of a Dirichlet L-function) with multiplicity m_ρ, and 0 ≤ T₁ < T₂, write - N(T₁, T₂) = ∑_{T₁ < γ ≤ T₂} m_ρ for the zeros counted with multiplicity, - N_d(T₁, T₂) = #{ρ : T₁ < γ ≤ T₂} for the distinct zeros, and - Ns(T₁, T₂) = #{ρ : T₁ < γ ≤ T₂, β = 1/2, m_ρ = 1} for the simple zeros on the critical line.

[Cl26, Theorem A] proves unconditionally that Ns(T, 2T) ≥ (2/3 - o(1)) N(T, 2T) and N_d(T, 2T) ≥ (5/6 - o(1)) N(T, 2T), improving to 2 - c_MT⁻¹ = 0.6725… and (3 - c_MT⁻¹) / 2 = 0.8362… with the Montgomery–Taylor window, where c_MT⁻¹ = 1/2 + cot(1/√2)/√2; [Cl26, Theorem B] is the same for L(s, χ), χ primitive.

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

The file states 16 research or textbook statements: 8 open and 8 solved.

riemannZeta.simple_prop_two_thirds

Solved: stated here; a Lean proof is at https://github.com/anthropics/zeta-23-lean/blob/v1.0/Zeta23/FinalMult.lean#L350.

At least two thirds of the nontrivial zeros of ζ, counted with multiplicity, are simple and on the critical line [Cl26, Theorem A (i)].

theorem simple_prop_two_thirds : ∃ o : ℝ → ℝ, o =o[atTop] (1 : ℝ → ℝ) ∧
    ∀ T > 0, (2 / 3 - o T) * N riemannZeta T (2 * T) ≤ Ns riemannZeta T (2 * T)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Paper/RiemannZetaZeros.lean, line 82.

riemannZeta.distinct_prop_five_sixths

Solved: stated here; a Lean proof is at https://github.com/anthropics/zeta-23-lean/blob/v1.0/Zeta23/FinalMult.lean#L358.

At least five sixths of the nontrivial zeros of ζ, counted with multiplicity, are distinct [Cl26, Theorem A (ii)].

theorem distinct_prop_five_sixths : ∃ o : ℝ → ℝ, o =o[atTop] (1 : ℝ → ℝ) ∧
    ∀ T > 0, (5 / 6 - o T) * N riemannZeta T (2 * T) ≤ Nd riemannZeta T (2 * T)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Paper/RiemannZetaZeros.lean, line 91.

riemannZeta.simple_prop_montgomeryTaylor

Solved: stated here; a Lean proof is at https://github.com/anthropics/zeta-23-lean/blob/v1.0/Zeta23/ThmD/Mult.lean#L435.

The proportion of simple zeros of ζ on the critical line is at least 2 - c_MT⁻¹ = 0.6725…. [Cl26, Theorem A]

theorem simple_prop_montgomeryTaylor : ∃ o : ℝ → ℝ, o =o[atTop] (1 : ℝ → ℝ) ∧
    ∀ T > 0, (2 - montgomeryTaylorConst⁻¹ - o T) * N riemannZeta T (2 * T) ≤
      Ns riemannZeta T (2 * T)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Paper/RiemannZetaZeros.lean, line 100.

riemannZeta.distinct_prop_montgomeryTaylor

Solved: stated here; a Lean proof is at https://github.com/anthropics/zeta-23-lean/blob/v1.0/Zeta23/ThmD/Mult.lean#L449.

The proportion of distinct zeros of ζ is at least (3 - c_MT⁻¹) / 2 = 0.8362…, [Cl26, Theorem A].

theorem distinct_prop_montgomeryTaylor : ∃ o : ℝ → ℝ, o =o[atTop] (1 : ℝ → ℝ) ∧
    ∀ T > 0, ((3 - montgomeryTaylorConst⁻¹) / 2 - o T) * N riemannZeta T (2 * T) ≤
      Nd riemannZeta T (2 * T)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Paper/RiemannZetaZeros.lean, line 110.

riemannZeta.simple_prop_lt

Open: stated without proof.

Is the proportion of simple zeros of ζ on the critical line unconditionally larger than the Montgomery–Taylor bound 2 - c_MT⁻¹ = 0.6725…? [Cl26, §7.2] puts the ceiling of its method at about 0.682.

theorem simple_prop_lt : ∃ c > 2 - montgomeryTaylorConst⁻¹, ∃ o : ℝ → ℝ,
    o =o[atTop] (1 : ℝ → ℝ) ∧
      ∀ T > 0, (c - o T) * N riemannZeta T (2 * T) ≤ Ns riemannZeta T (2 * T)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Paper/RiemannZetaZeros.lean, line 119.

riemannZeta.simple_prop_one_hundred

Open: stated without proof.

Almost all nontrivial zeros of ζ are simple and on the critical line.

theorem simple_prop_one_hundred : ∃ o : ℝ → ℝ, o =o[atTop] (1 : ℝ → ℝ) ∧
    ∀ T > 0, (1 - o T) * N riemannZeta T (2 * T) ≤ Ns riemannZeta T (2 * T)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Paper/RiemannZetaZeros.lean, line 126.

riemannZeta.distinct_prop_lt

Open: stated without proof.

Is the proportion of distinct zeros of ζ unconditionally larger than the Montgomery–Taylor bound (3 - c_MT⁻¹) / 2 = 0.8362…?

theorem distinct_prop_lt : ∃ c > (3 - montgomeryTaylorConst⁻¹) / 2, ∃ o : ℝ → ℝ,
    o =o[atTop] (1 : ℝ → ℝ) ∧
    ∀ T > 0, (c - o T) * N riemannZeta T (2 * T) ≤ Nd riemannZeta T (2 * T)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Paper/RiemannZetaZeros.lean, line 133.

riemannZeta.distinct_prop_one_hundred

Open: stated without proof.

Almost all nontrivial zeros of ζ are simple.

theorem distinct_prop_one_hundred : ∃ o : ℝ → ℝ, o =o[atTop] (1 : ℝ → ℝ) ∧
    ∀ T > 0, (1 - o T) * N riemannZeta T (2 * T) ≤ Nd riemannZeta T (2 * T)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Paper/RiemannZetaZeros.lean, line 140.

DirichletCharacter.simple_prop_two_thirds

Solved: stated here; a Lean proof is at https://github.com/anthropics/zeta-23-lean/blob/v1.0/Zeta23/ThmE/Mult.lean#L324.

At least two thirds of the nontrivial zeros of L(s, χ), χ primitive, counted with multiplicity, are simple and on the critical line, [Cl26, Theorem B].

theorem simple_prop_two_thirds (hχ : χ.IsPrimitive) : ∃ o : ℝ → ℝ, o =o[atTop] (1 : ℝ → ℝ) ∧
    ∀ T > 0, (2 / 3 - o T) * N (LFunction χ) T (2 * T) ≤ Ns (LFunction χ) T (2 * T)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Paper/RiemannZetaZeros.lean, line 155.

DirichletCharacter.distinct_prop_five_sixths

Solved: stated here; a Lean proof is at https://github.com/anthropics/zeta-23-lean/blob/v1.0/Zeta23/ThmE/Mult.lean#L333.

At least five sixths of the nontrivial zeros of L(s, χ), χ primitive, counted with multiplicity, are distinct, [Cl26, Theorem B].

theorem distinct_prop_five_sixths (hχ : χ.IsPrimitive) : ∃ o : ℝ → ℝ, o =o[atTop] (1 : ℝ → ℝ) ∧
    ∀ T > 0, (5 / 6 - o T) * N (LFunction χ) T (2 * T) ≤ Nd (LFunction χ) T (2 * T)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Paper/RiemannZetaZeros.lean, line 164.

DirichletCharacter.simple_prop_montgomeryTaylor

Solved: stated here; a Lean proof is at https://github.com/anthropics/zeta-23-lean/blob/v1.0/Zeta23/ThmDE/Mult.lean#L429.

The proportion of simple zeros of L(s, χ), χ primitive, on the critical line is at least 2 - c_MT⁻¹ = 0.6725…, [Cl26, Theorem B].

theorem simple_prop_montgomeryTaylor (hχ : χ.IsPrimitive) :
    ∃ o : ℝ → ℝ, o =o[atTop] (1 : ℝ → ℝ) ∧
    ∀ T > 0, (2 - montgomeryTaylorConst⁻¹ - o T) * N (LFunction χ) T (2 * T) ≤
      Ns (LFunction χ) T (2 * T)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Paper/RiemannZetaZeros.lean, line 173.

DirichletCharacter.distinct_prop_montgomeryTaylor

Solved: stated here; a Lean proof is at https://github.com/anthropics/zeta-23-lean/blob/v1.0/Zeta23/ThmDE/Mult.lean#L437.

The proportion of distinct zeros of L(s, χ), χ primitive, is at least (3 - c_MT⁻¹) / 2 = 0.8362…, [Cl26, Theorem B].

theorem distinct_prop_montgomeryTaylor (hχ : χ.IsPrimitive) :
    ∃ o : ℝ → ℝ, o =o[atTop] (1 : ℝ → ℝ) ∧
    ∀ T > 0, ((3 - montgomeryTaylorConst⁻¹) / 2 - o T) * N (LFunction χ) T (2 * T) ≤
      Nd (LFunction χ) T (2 * T)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Paper/RiemannZetaZeros.lean, line 184.

DirichletCharacter.simple_prop_lt

Open: stated without proof.

Is the proportion of simple zeros of L(s, χ), χ primitive, on the critical line unconditionally larger than the Montgomery–Taylor bound 2 - c_MT⁻¹ = 0.6725…?

theorem simple_prop_lt (hχ : χ.IsPrimitive) : ∃ c > 2 - montgomeryTaylorConst⁻¹, ∃ o : ℝ → ℝ,
    o =o[atTop] (1 : ℝ → ℝ) ∧
    ∀ T > 0, (c - o T) * N (LFunction χ) T (2 * T) ≤ Ns (LFunction χ) T (2 * T)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Paper/RiemannZetaZeros.lean, line 193.

DirichletCharacter.simple_prop_one_hundred

Open: stated without proof.

Almost all nontrivial zeros of L(s, χ), χ primitive, are simple and on the critical line.

theorem simple_prop_one_hundred (hχ : χ.IsPrimitive) : ∃ o : ℝ → ℝ, o =o[atTop] (1 : ℝ → ℝ) ∧
    ∀ T > 0, (1 - o T) * N (LFunction χ) T (2 * T) ≤ Ns (LFunction χ) T (2 * T)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Paper/RiemannZetaZeros.lean, line 201.

DirichletCharacter.distinct_prop_lt

Open: stated without proof.

Is the proportion of distinct zeros of L(s, χ), χ primitive, unconditionally larger than the Montgomery–Taylor bound (3 - c_MT⁻¹) / 2 = 0.8362…?

theorem distinct_prop_lt (hχ : χ.IsPrimitive) : ∃ c > (3 - montgomeryTaylorConst⁻¹) / 2,
    ∃ o : ℝ → ℝ, o =o[atTop] (1 : ℝ → ℝ) ∧
      ∀ T > 0, (c - o T) * N (LFunction χ) T (2 * T) ≤ Nd (LFunction χ) T (2 * T)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Paper/RiemannZetaZeros.lean, line 208.

DirichletCharacter.distinct_prop_one_hundred

Open: stated without proof.

Almost all nontrivial zeros of L(s, χ), χ primitive, are simple.

theorem distinct_prop_one_hundred (hχ : χ.IsPrimitive) : ∃ o : ℝ → ℝ, o =o[atTop] (1 : ℝ → ℝ) ∧
    ∀ T > 0, (1 - o T) * N (LFunction χ) T (2 * T) ≤ Nd (LFunction χ) T (2 * T)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Paper/RiemannZetaZeros.lean, line 215.

Sources

• FormalConjectures/Paper/RiemannZetaZeros.lean at 2055e5ad
• pdf

LeanriemannZeta.simple_prop_two_thirds · riemannZeta.distinct_prop_five_sixths · riemannZeta.simple_prop_montgomeryTaylor · riemannZeta.distinct_prop_montgomeryTaylor · riemannZeta.simple_prop_lt · riemannZeta.simple_prop_one_hundred · riemannZeta.distinct_prop_lt · riemannZeta.distinct_prop_one_hundred · DirichletCharacter.simple_prop_two_thirds · DirichletCharacter.distinct_prop_five_sixths · DirichletCharacter.simple_prop_montgomeryTaylor · DirichletCharacter.distinct_prop_montgomeryTaylor · DirichletCharacter.simple_prop_lt · DirichletCharacter.simple_prop_one_hundred · DirichletCharacter.distinct_prop_lt · DirichletCharacter.distinct_prop_one_hundred

TheoremRingel's Conjecture#

Reference: G. Ringel, Problem 25, in Theory of Graphs and its Applications (Proc. Sympos. Smolenice, 1963), Academia, Prague, 1964.

Ringel's conjecture (1963): the complete graph \(K_{2n+1}\) decomposes into copies of any tree with \(n\) edges. It remains open; the case of all sufficiently large \(n\) is proved by Montgomery–Pokrovskiy–Sudakov, see Arxiv/2001.02665/RingelConjecture.lean.

Quoted from FormalConjectures/Paper/RingelConjecture.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.

RingelConjecture.ringel_conjecture

Open: stated without proof.

For any tree \(T\) with \(n\) edges, the complete graph \(K_{2n+1}\) decomposes into \(2n+1\) edge-disjoint copies of \(T\).

A "copy" of \(T\) is the image \(T.\text{map}(f_i)\) of \(T\) under a vertex embedding \(f_i : V \hookrightarrow \text{Fin}(2n+1)\); the copies are pairwise edge-disjoint and together cover every edge of \(K_{2n+1}\).

theorem ringel_conjecture {V : Type} [Finite V]
    (T : SimpleGraph V) (hT : T.IsTree)
    (n : ℕ) (hn : T.edgeSet.ncard = n) :
    ∃ f : Fin (2 * n + 1) → (V ↪ Fin (2 * n + 1)),
      Pairwise (fun i j => Disjoint (T.map (f i)).edgeSet (T.map (f j)).edgeSet) ∧
      ⨆ i, T.map (f i) = (⊤ : SimpleGraph (Fin (2 * n + 1)))

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/Paper/RingelConjecture.lean, line 45.

Sources

• FormalConjectures/Paper/RingelConjecture.lean at 2055e5ad

LeanRingelConjecture.ringel_conjecture

TheoremIs Every Convex Polyhedron Rupert?#

A polyhedron is Rupert if one can cut a hole in it and pass another copy of the same polyhedron through that hole.

More formally: a convex body in ℝ³ is a compact, convex set with nonempty interior. A convex body X is said to be Rupert if there are two affine transforms T₁, T₂ ∈ SE(3) such that π(T₁(X)) ⊆ int(π(T₂(X))), where π : ℝ³ → ℝ² is the evident projection, and int denotes topological interior.

Not all convex bodies are Rupert. For example, - the unit ball is not Rupert - the circular cylinder of unit diameter and height closed on each end by disks is not Rupert

However, many convex polyhedra are Rupert. All Platonic solids, and most Archimedean and Catalan solids are known to be Rupert.

Question: are all convex polyhedra with nonempty interior Rupert?

References:

• Platonic Passages, R. P. Jerrard, J. E. Wetzel, and L. Yuan., Math. Mag., 90(2):87–98,

• conjectures ("with a certain hesitancy") that perhaps all convex polyhedra are Rupert.

• However, An Algorithmic Approach to Rupert's Problem describes experimental evidence to suggest that three Archimedean solids may not be Rupert.

• Optimizing for the Rupert property is the source of some of the Catalan solid results, and has more results for Johnson polyhedra as well.

• This video by David Renshaw visualizes known results for Platonic, Archimedean, and Catalan solids.

• This problem's name comes from the fact that it is a generalization of Prince Rupert's Cube.

• A convex polyhedron without Rupert's property, Jakob Steininger and Sergey Yurkevich, 2025. Constructs a convex polyhedron and a proof that it is not Rupert, resolving the open question.

Quoted from FormalConjectures/Paper/Rupert.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.

Rupert.is_every_convex_polyhedron_rupert

Solved: stated here; a Lean proof is at https://github.com/jcreedcmu/Noperthedron/blob/1ee88118097acc9db768b44b3c6ea9f60a4e4b67/KernelCaseAnalysis/ProofOfMainTheorem.lean#L21.

There exists a convex polyhedron with nonempty interior for which the Rupert property does not hold.

theorem is_every_convex_polyhedron_rupert :
    ¬ ∀ (vertices : Finset ℝ³),
       (interior (convexHull ℝ vertices : Set ℝ³)).Nonempty → IsRupert vertices

Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/Paper/Rupert.lean, line 115.

Sources

• FormalConjectures/Paper/Rupert.lean at 2055e5ad
• Platonic Passages

LeanRupert.is_every_convex_polyhedron_rupert

TheoremSerre's uniformity conjecture over the rationals#

Is there a bound \(C\), independent of the non-CM elliptic curve \(E/\mathbb{Q}\), such that the Galois action on \(E[p]\) is surjective onto \(\mathrm{GL}_2(\mathbb{F}_p)\) for every prime \(p > C\)? This is the \(\mathbb{Q}\) case of Serre's question [Ser72], recalled in the introduction of [Lem17].

We express surjectivity without choosing a basis: every additive automorphism of \(E[p]\) must be induced by an element of \(G_{\mathbb{Q}}\). For prime \(p\), these automorphisms are exactly the \(\mathbb{F}_p\)-linear automorphisms. The non-CM condition uses the classification of rational CM \(j\)-invariants.

References: - [Ser72] J.-P. Serre, Propriétés galoisiennes des points d'ordre fini des courbes elliptiques. Inventiones Mathematicae 15 (1972), 259–331. https://doi.org/10.1007/BF01405086 - [Lem17] P. Lemos, Serre's uniformity conjecture for elliptic curves with rational cyclic isogenies, introduction. https://arxiv.org/abs/1702.01985

Quoted from FormalConjectures/Paper/SerreUniformity.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.

SerreUniformity.serre_uniformity

Open: stated without proof.

Serre's uniformity question over \(\mathbb{Q}\) [Ser72, Lem17]: is there a bound \(C\) such that every non-CM elliptic curve over \(\mathbb{Q}\) has surjective mod-\(p\) Galois representation for every prime \(p > C\)?

theorem serre_uniformity :
    ∃ C : ℕ, ∀ (E : WeierstrassCurve ℚ) [E.IsElliptic], E.j ∉ cmJInvariants →
      ∀ p : ℕ, p.Prime → C < p → HasFullTorsionAction E p

Category research open; AMS 11 Number theory, 14 Algebraic geometry. Declared in FormalConjectures/Paper/SerreUniformity.lean, line 68.

SerreUniformity.serre_uniformity.variants.bound_37

Open: stated without proof.

Serre's uniformity conjecture over \(\mathbb{Q}\), explicit form: the bound \(C = 37\) works, i.e. every non-CM elliptic curve over \(\mathbb{Q}\) has surjective mod-\(p\) Galois representation for every prime \(p > 37\). From the introduction of [Lem17]: "This conjecture remains open today, but, over the last forty years, there has been a lot of progress towards a proof for \(K = \mathbb{Q}\) — it is believed that, in this case, \(p_K = 37\)."

theorem serre_uniformity.variants.bound_37 :
    ∀ (E : WeierstrassCurve ℚ) [E.IsElliptic], E.j ∉ cmJInvariants →
      ∀ p : ℕ, p.Prime → 37 < p → HasFullTorsionAction E p

Category research open; AMS 11 Number theory, 14 Algebraic geometry. Declared in FormalConjectures/Paper/SerreUniformity.lean, line 81.

Sources

• FormalConjectures/Paper/SerreUniformity.lean at 2055e5ad
• https://doi.org/10.1007/BF01405086

LeanSerreUniformity.serre_uniformity · SerreUniformity.serre_uniformity.variants.bound_37

TheoremShelah-Spencer's Zero-One Law for Sparse Random Graphs#

References:

• Shelah and Spencer, Zero-one laws for sparse random graphs, Journal of the American Mathematical Society, 1(1), 97-115 (1988).
• Glebskii et al., Range and degree of realizability of formulas in the restricted predicate calculus, Cybernetics, 5(2), 142-154 (1969) (for \(\alpha = 0\)).

Quoted from FormalConjectures/Paper/ShelahSpencerZeroOneLaw.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.

ShelahSpencerZeroOneLaw.zeroOne_irrational

Solved: stated here without proof.

If \(0 < \alpha < 1\) is irrational, then for every first-order sentence \(\varphi\) in the language of graphs, the probability that \(G(n, n^{-\alpha})\) satisfies \(\varphi\) tends to either zero or one as \(n \to \infty\).

theorem zeroOne_irrational
   (α : ℝ) (hα : 0 < α ∧ α < 1) (hirr : Irrational α) (φ : Language.graph.Sentence) :
   Tendsto (fun n =>
     sparseRandomGraph n α hα.1
       {G | @Language.Sentence.Realize Language.graph (Fin n) G.structure φ}) atTop (𝓝 0) ∨
   Tendsto (fun n =>
     sparseRandomGraph n α hα.1
       {G | @Language.Sentence.Realize Language.graph (Fin n) G.structure φ}) atTop (𝓝 1)

Category research solved; AMS 03 Mathematical logic and foundations, 05 Combinatorics. Declared in FormalConjectures/Paper/ShelahSpencerZeroOneLaw.lean, line 60.

ShelahSpencerZeroOneLaw.zeroOne_rational

Solved: stated here without proof.

If \(0 < \alpha < 1\) is rational, then there is a first-order sentence \(\varphi\) in the language of graphs whose probability in \(G(n, n^{-\alpha})\) does not converge as \(n \to \infty\).

theorem zeroOne_rational
   (α : ℝ) (hα : 0 < α ∧ α < 1) (hrat : ¬Irrational α) :
   ∃ φ : Language.graph.Sentence,
   ∀ b : ENNReal,
   ¬ Tendsto (fun n =>
     sparseRandomGraph n α hα.1
       {G | @Language.Sentence.Realize Language.graph (Fin n) G.structure φ}) atTop (𝓝 b)

Category research solved; AMS 03 Mathematical logic and foundations, 05 Combinatorics. Declared in FormalConjectures/Paper/ShelahSpencerZeroOneLaw.lean, line 74.

Sources

• FormalConjectures/Paper/ShelahSpencerZeroOneLaw.lean at 2055e5ad
• Shelah and Spencer, Zero-one laws for sparse random graphs

LeanShelahSpencerZeroOneLaw.zeroOne_irrational · ShelahSpencerZeroOneLaw.zeroOne_rational

TheoremSize, Order, and Connected Domination#

References: - S. Mukwembi, Size, order, and connected domination, Canad. Math. Bull. 57 (2014), no. 1, 141–144

Quoted from FormalConjectures/Paper/SizeOrderConnectedDomination.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.

SizeOrderConnectedDomination.mukwembi_theorem_2_1

Solved: stated here; a Lean proof is at https://github.com/henrykmichalewski/formal-conjectures/blob/238fcea04077aee1d63c9201aa4b4b794f3a674d/FormalConjectures/Paper/SizeOrderConnectedDomination.lean#L156.

Theorem 2.1 of S. Mukwembi, Size, order, and connected domination, Canad. Math. Bull. 57 (2014), no. 1, 141–144 claims: if \(G\) is a connected triangle-free graph of order \(n\) and size \(m\) with connected domination number \(\gamma_c\), then

\[m \le \frac{(n - \gamma_c)^2}{4} + n - 1.\]

The claim is false: the 3-dimensional hypercube \(Q_3\) is a counterexample, with \(n = 8\), \(m = 12\) and \(\gamma_c = 4\), so the asserted bound reads \(12 \le (8-4)^2/4 + 8 - 1 = 11\). The gap in the paper's proof (p. 143) is the unjustified assertion that there is an edge \(uv\) with \(\gamma_c(G) \le \gamma_c(G - \{u, v\})\): in \(Q_3\), removing any adjacent pair of vertices leaves a graph with connected domination number \(2 < 4\).

The corollaries of the paper (Corollary 2.2 and 2.3, on leaf numbers of triangle-free graphs) remain true; Corollary 2.2 is Graffiti.pc Conjecture 1.1, recorded as WrittenOnTheWallII.GraphConjecture2.conjecture2.

theorem mukwembi_theorem_2_1 :
    ¬ ∀ (α : Type) [Fintype α] [DecidableEq α] [Nontrivial α]
      (G : SimpleGraph α) [DecidableRel G.Adj],
      G.Connected → G.CliqueFree 3 →
      (G.edgeFinset.card : ℝ) ≤
        ((Fintype.card α : ℝ) - (G.connectedDominationNumber : ℝ)) ^ 2 / 4
          + (Fintype.card α : ℝ) - 1

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Paper/SizeOrderConnectedDomination.lean, line 57.

Sources

• FormalConjectures/Paper/SizeOrderConnectedDomination.lean at 2055e5ad
• S. Mukwembi, Size, order, and connected domination, Canad. Math. Bull. 57 (2014), no. 1, 141–144

LeanSizeOrderConnectedDomination.mukwembi_theorem_2_1

TheoremStrong Sensitivity Conjecture (`bs(f) ≤ s(f)^2`)#

This file formalizes the strong sensitivity conjecture, asserting:

For every Boolean function f : {0,1}^n → {0,1}, bs(f) ≤ s(f)^2, where bs(f) denotes block sensitivity and s(f) denotes sensitivity.

Huang's theorem proves a quartic upper bound, bs(f) ≤ s(f)^4, thereby resolving the most widely known form of the sensitivity conjecture.

We now ask whether a stronger upper bound holds. Interestingly, the original paper of Nisan and Szegedy, where the sensitivity conjecture first appeared, already speculated that a quadratic upper bound might be the correct relation. On the lower bound side, Rubinstein (https://link.springer.com/article/10.1007/BF01200762) constructed Boolean functions exhibiting the first quadratic separation. The best gap known before [OAI26], due to Ambainis and Sun (https://arxiv.org/abs/1108.3494), was bs(f) ≥ (2/3)⋅s(f)^2.

In September 2026 an internal OpenAI model disproved the quadratic bound [OAI26]: it constructs total Boolean functions with bs(f) / s(f)^2 arbitrarily large.

References: * [OAI26] A superquadratic separation between sensitivity and block sensitivity by OpenAI, OpenAI Math Release preprint (2026) * Induced Subgraphs of Hypercubes and a Proof of the Sensitivity Conjecture by Hao Huang (see Section 3, Concluding Remarks) * Variations on the Sensitivity Conjecture by Pooya Hatami, Raghav Kulkarni, and Denis Pankratov (see Question 3.1) * On the Degree of Boolean Functions as Real Polynomials by Noam Nisan, and Mario Szegedy (see Section 4, Open Problems)

Quoted from FormalConjectures/Paper/StrongSensitivityConjecture.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 3 test statements, counted here but not shown.

StrongSensitivityConjecture.strong_sensitivity_conjecture

Solved: stated here; a Lean proof is at https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Sensitivity/Separation.lean#L12.

Strong Sensitivity Conjecture, for every Boolean function f : {0,1}^n → {0,1}, bs(f) ≤ s(f)^2.

We call this the strong sensitivity conjecture because the original sensitivity conjecture only asked for a polynomial bound in terms of s(f). Huang's celebrated result (often called the sensitivity theorem) gives a quartic bound, bs(f) ≤ s(f)^4, thereby settling the original conjecture.

The quadratic bound is false. This was disproved by an internal OpenAI model in September 2026 [OAI26]; see the linked Lean proof.

theorem strong_sensitivity_conjecture :
    ¬ ∀ (n : ℕ) (f : (Fin n → Bool) → Bool), blockSensitivity f ≤ sensitivity f ^ 2

Category research solved; AMS 68 Computer science. Declared in FormalConjectures/Paper/StrongSensitivityConjecture.lean, line 113.

Sources

• FormalConjectures/Paper/StrongSensitivityConjecture.lean at 2055e5ad
• A superquadratic separation between sensitivity and block sensitivity

LeanStrongSensitivityConjecture.strong_sensitivity_conjecture

TheoremTu-Deng Conjecture#

References: * Tu, Z., Deng, Y., A conjecture about binary strings and its applications on constructing Boolean functions with optimal algebraic immunity, Des. Codes Cryptogr. 60 (2011), 1–14 * IACR ePrint 2009/272 * [LLX26] Liu, R., Luo, H., Xie, T., A Complete Proof for Tu-Deng Conjecture, arXiv:2608.05187v2 (2026) * [Cu26] Cusick, T. W., Proof of the TuDeng Conjecture, arXiv:2608.14821 (2026) * [Lean26] A Lean 4 proof of the count form of the conjecture, commit 3c005614, theorem TuDeng.FirstExit.tu_deng_conjecture_full

For an integer \(k \ge 2\), identify the residues modulo \(2^k - 1\) with the integers \(0, 1, \dots, 2^k - 2\), and let \(w(a)\) denote the binary weight of \(a\) (the number of ones in its binary expansion). The Tu-Deng conjecture states that for every residue \(t \ne 0\),

\[\#\{(a, b) : a + b \equiv t \pmod{2^k - 1},\ w(a) + w(b) \le k - 1\} \le 2^{k-1}.\]

Tu and Deng showed that this combinatorial statement implies that their constructions of Boolean functions (a bent class and a balanced class) achieve optimal algebraic immunity, which is the motivation for the conjecture. They verified the conjecture numerically for \(k \le 29\) (Remark 3.1 of the ePrint version).

The conjecture is no longer open: [LLX26] and, independently, [Cu26] give complete proofs. [Lean26] is a Lean 4 development of the same bound, stated for the count of natural-number representatives \(x < 2^k - 1\) rather than for the set of residue pairs used below.

Quoted from FormalConjectures/Paper/TuDengConjecture.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.

TuDengConjecture.tu_deng_conjecture

Solved: stated here without proof.

The Tu-Deng conjecture. For \(k \ge 2\) and a nonzero residue \(t\) modulo \(2^k - 1\), there are at most \(2^{k-1}\) pairs of residues \((a, b)\) with \(a + b = t\) whose binary weights (of their representatives in \(0, \dots, 2^k - 2\)) sum to at most \(k - 1\).

Proved in [LLX26] and independently in [Cu26]; see also the Lean development [Lean26].

theorem tu_deng_conjecture (k : ℕ) (hk : 2 ≤ k) (t : ZMod (2 ^ k - 1)) (ht : t ≠ 0) :
    {p : ZMod (2 ^ k - 1) × ZMod (2 ^ k - 1) |
        p.1 + p.2 = t ∧ binaryWeight p.1.val + binaryWeight p.2.val ≤ k - 1}.ncard
      ≤ 2 ^ (k - 1)

Category research solved; AMS 05 Combinatorics, 11 Number theory, 94 Information and communication, circuits. Declared in FormalConjectures/Paper/TuDengConjecture.lean, line 66.

Sources

• FormalConjectures/Paper/TuDengConjecture.lean at 2055e5ad
• Tu, Z., Deng, Y., A conjecture about binary strings and its applications on constructing Boolean functions with optimal algebraic immunity, Des. Codes Cryptogr. 60 (2011), 1–14

LeanTuDengConjecture.tu_deng_conjecture

TheoremVoronovskaja-type Formula for the Bezier Variant of the Bernstein Operators#

The Bézier-type Bernstein operators \(B_{n,\alpha}\) for \(\alpha > 0\) are defined for \(f : [0,1] \to \mathbb{R}\) by

\[ (B_{n,\alpha} f)(x) = \sum_{k=0}^n f\!\left(\frac{k}{n}\right) \left( J_{n,k}(x)^{\alpha} - J_{n,k+1}(x)^{\alpha} \right), \]

where

\[ J_{n,k}(x) = \sum_{j=k}^n p_{n,j}(x), \qquad p_{n,j}(x) = \binom{n}{j} x^j(1-x)^{n-j}, \]

and \(J_{n,n+1}(x) = 0\).

In the classical case \(\alpha = 1\), these operators reduce to the usual Bernstein operators. For \(f\) which are \(C^2\) on \([0,1]\), one has the classical Voronovskaja asymptotic formula

\[ \lim_{n \to \infty} n\bigl( B_{n,1} f(x) - f(x) \bigr) = \tfrac{1}{2} x(1-x) f''(x). \]

Known Results

• For \(\alpha = 1\), the asymptotics are completely understood.
• Numerical experiments indicate that for \(\alpha \neq 1\) the quantity

\[ \sqrt{n}\,\bigl( B_{n,\alpha} f(x) - f(x) \bigr) \]

may converge to a non-zero limit.

The Problem

Determine the asymptotic behaviour of the Bézier-type Bernstein operators for \(\alpha > 0\), \(\alpha \neq 1\): \textbf{Existence of the limit:} Prove (or disprove) the existence of the limit

\[ \lim_{n \to \infty} \sqrt{n}\,\bigl( B_{n,\alpha} f(x) - f(x) \bigr), \]

at least for sufficiently smooth functions \(f\). \textbf{Explicit form of the limit:} If the limit exists, determine an explicit expression for it in terms of \(f\), \(x\), and \(\alpha\).

Provenance

The limit formula recorded here, together with the elementary identities and the endpoint reduction in this file, was first proposed by Samuel Schlesinger. The first complete proof is the Lean 4 formalisation by Kenta Kitamura (KitaKen1 on GitHub) in [K26], which is linked from voronovskaja_theorem.bezier_bernstein_operators.

References:

• Voronovskaja-type Formula for the Bézier Variant of the Bernstein Operators, by Ulrich Abel, in Constructive Theory of Functions, Sozopol 2010.
• [K26] A Formal Conjectures Bézier--Bernstein Theorem in Lean, by Kenta Kitamura.

Quoted from FormalConjectures/Paper/VoronovskajaTypeFormula.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. It also has 21 API statements, counted here but not shown.

VoronovskajaTypeFormula.voronovskaja_theorem.bernstein_operators

Solved: stated here without proof.

Classical Voronovskaja theorem (α = 1).

For functions \(f\) that are \(C^2\) on \([0,1]\), the limit:

\[ n\bigl( B_n f(x) - f(x) \bigr) \;\longrightarrow\; \frac{1}{2}\, x(1 - x)\, f''(x) \]

theorem voronovskaja_theorem.bernstein_operators
    (f : ℝ → ℝ) (x : ℝ) (hx : x ∈ I)
    (hf : ContDiffOn ℝ 2 f I) :
    let f'' : ℝ := iteratedDerivWithin 2 f I x
    Tendsto (fun (n : ℕ) => (n : ℝ) * (bezierBernstein n 1 f x - f x))
    atTop
    (𝓝 ((1 / 2) * x * (1 - x) * f''))

Category research solved; AMS 26 Real functions, 40 Sequences, series, summability, 47 Operator theory. Declared in FormalConjectures/Paper/VoronovskajaTypeFormula.lean, line 448.

VoronovskajaTypeFormula.voronovskaja_theorem.bezier_bernstein_operators

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/bezier-bernstein-voronovskaja-lean/blob/3f35c631d215b3841242275bf3ed2c59ea153a2d/Voronovskaja.lean.

Voronovskaja-type formula for Bézier--Bernstein operators with shape parameter \(\alpha > 0\), \(\alpha \neq 1\).

The source asks for sufficiently smooth functions. This concrete version uses ContDiffOn ℝ 2 f I as a readable baseline regularity assumption; since the domain is the compact interval \([0,1]\), this also explains why no separate boundedness assumption is included here.

The limit exists and equals \(\mu(\alpha)\,\sqrt{x(1-x)}\,f'(x)\), where \(\mu(\alpha) = \int_0^\infty \bigl( (1 - \Phi(t))^{\alpha} - (1 - \Phi(t)^{\alpha}) \bigr)\,dt\) and \(\Phi\) is the standard normal distribution function.

Informal proof: the weights \(w_{n,k} = J_{n,k}(x)^{\alpha} - J_{n,k+1}(x)^{\alpha}\) are nonnegative and sum to \(1\), so the quadratic Taylor bound for \(f \in C^2\) gives

\[ B_{n,\alpha} f(x) - f(x) = \sum_{k=0}^{n} \bigl( f(k/n) - f(x) \bigr) w_{n,k} = f'(x) \sum_{k=0}^{n} (k/n - x)\, w_{n,k} + O\Bigl( \sum_{k=0}^{n} (k/n - x)^2 w_{n,k} \Bigr). \]

The two sums on the right satisfy

\[ \sqrt{n} \sum_{k=0}^{n} (k/n - x)\, w_{n,k} \longrightarrow \mu(\alpha)\,\sqrt{x(1-x)}, \qquad \sqrt{n} \sum_{k=0}^{n} (k/n - x)^2 w_{n,k} \longrightarrow 0, \]

so multiplying by \(\sqrt{n}\) gives the stated limit.

The linked formal proof is a self-contained Lean 4 formalisation by Kenta Kitamura (KitaKen1 on GitHub); see [K26].

theorem voronovskaja_theorem.bezier_bernstein_operators
    (α : ℝ) (hα_pos : 0 < α) (hα : α ≠ 1)
    (f : ℝ → ℝ) (x : ℝ) (hx : x ∈ I)
    (hf : ContDiffOn ℝ 2 f I) :
    Tendsto (fun n : ℕ => Real.sqrt n * (bezierBernstein n α f x - f x)) atTop
      (𝓝 ((voronovskaja_theorem.bezier_bernstein_operators.answer :
        ℝ → (ℝ → ℝ) → ℝ → ℝ) α f x))

Category research solved; AMS 26 Real functions, 40 Sequences, series, summability, 47 Operator theory. Declared in FormalConjectures/Paper/VoronovskajaTypeFormula.lean, line 498.

Sources

• FormalConjectures/Paper/VoronovskajaTypeFormula.lean at 2055e5ad
• Voronovskaja-type Formula for the Bézier Variant of the Bernstein Operators

LeanVoronovskajaTypeFormula.voronovskaja_theorem.bernstein_operators · VoronovskajaTypeFormula.voronovskaja_theorem.bezier_bernstein_operators

TheoremConjectures about Weakly First Countable spaces#

This file formalizes the notion of a weakly first countable topological space and some conjectures around those.

References: * [Ar2013] Arhangeliski, Alexandr. "Selected old open problems in general topology." Buletinul Academiei de Ştiinţe a Republicii Moldova. Matematica 73.2-3 (2013): 37-46. https://www.math.md/files/basm/y2013-n2-3/y2013-n2-3-(pp37-46).pdf.pdf * [Ya1976] Yakovlev, N. N. "On the theory of o-metrizable spaces." Doklady Akademii Nauk. Vol. 229. No. 6. Russian Academy of Sciences, 1976. https://www.mathnet.ru/links/016f74007f9f96fa3aadae05cbd98457/dan40570.pdf (in Russian)

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

WeaklyFirstCountable.exists_weakly_first_countable_not_first_countable

Textbook result, stated without proof.

There are weakly first countable spaces which are not first countable, for example the Arens Space.

theorem exists_weakly_first_countable_not_first_countable : ∃ (X : Type) (_ : TopologicalSpace X),
      WeaklyFirstCountableTopology X ∧ ¬ FirstCountableTopology X

Category textbook; AMS 54 General topology. Declared in FormalConjectures/Paper/WeaklyFirstCountable.lean, line 73.

WeaklyFirstCountable.existsWeaklyFirstCountableCompactBig

Open: stated without proof.

Problem 2 in [Ar2013]: Give an example in ZFC of a weakly first- countable compact Hausdorff space X such that \(𝔠 < |X|\).

Note: [Ar2013] uses a blanket convention that all spaces are Tychonoff and "compact" means compact Hausdorff.

theorem existsWeaklyFirstCountableCompactBig :
    ∃ (X : Type) (_ : TopologicalSpace X),
      WeaklyFirstCountableTopology X ∧ CompactSpace X ∧ T2Space X ∧
        𝔠 < #X

Category research open; AMS 54 General topology. Declared in FormalConjectures/Paper/WeaklyFirstCountable.lean, line 114.

WeaklyFirstCountable.existsWeaklyFirstCountableCompactNotFirstCountable

Open: stated without proof.

Problem 3 in [Ar2013]: Give an example in ZFC of a weakly first- countable compact Hausdorff space which is not first countable.

Note: [Ar2013] uses a blanket convention that all spaces are Tychonoff and "compact" means compact Hausdorff.

theorem existsWeaklyFirstCountableCompactNotFirstCountable :
    ∃ (X : Type) (_ : TopologicalSpace X),
      WeaklyFirstCountableTopology X ∧ CompactSpace X ∧ T2Space X ∧
        ¬ FirstCountableTopology X

Category research open; AMS 54 General topology. Declared in FormalConjectures/Paper/WeaklyFirstCountable.lean, line 126.

WeaklyFirstCountable.CH.existsWeaklyFirstCountableCompactNotFirstCountable

Solved: stated here without proof.

Under CH, such a space (for Problem 3 in [Ar2013]) exists as constructed in [Ya1976] by Yakovlev.

theorem CH.existsWeaklyFirstCountableCompactNotFirstCountable
    [Fact (ℵ₁ = 𝔠)] :
    ∃ (X : Type) (_ : TopologicalSpace X),
      WeaklyFirstCountableTopology X ∧ CompactSpace X ∧ T2Space X ∧
        ¬ FirstCountableTopology X

Category research solved; AMS 54 General topology. Declared in FormalConjectures/Paper/WeaklyFirstCountable.lean, line 135.

WeaklyFirstCountable.cardinalMk_le_continuum_of_weaklyFirstCountable_of_countableSouslinNumber

Open: stated without proof.

Problem 4 in [Ar2013]: If a Tychonoff weakly first-countable space has countable Souslin number, then does its cardinality not exceed the continuum?

theorem cardinalMk_le_continuum_of_weaklyFirstCountable_of_countableSouslinNumber :
    ∀ (X : Type) (_ : TopologicalSpace X), T35Space X →
      WeaklyFirstCountableTopology X → HasCountableSouslinNumber X → #X ≤ 𝔠

Category research open; AMS 54 General topology. Declared in FormalConjectures/Paper/WeaklyFirstCountable.lean, line 144.

Sources

• FormalConjectures/Paper/WeaklyFirstCountable.lean at 2055e5ad
• https://www.math.md/files/basm/y2013-n2-3/y2013-n2-3-(pp37-46

LeanWeaklyFirstCountable.exists_weakly_first_countable_not_first_countable · WeaklyFirstCountable.existsWeaklyFirstCountableCompactBig · WeaklyFirstCountable.existsWeaklyFirstCountableCompactNotFirstCountable · WeaklyFirstCountable.CH.existsWeaklyFirstCountableCompactNotFirstCountable · WeaklyFirstCountable.cardinalMk_le_continuum_of_weaklyFirstCountable_of_countableSouslinNumber

TheoremWeak tiling problems#

Problems 4.1, 4.2, and 4.3 from arxiv/2506.23631.

Reference: * Geometric implications of weak tiling

See also FormalConjectures.Wikipedia.Fuglede for Fuglede's spectral set conjecture, which motivates the study of weak tilings.

Quoted from FormalConjectures/Paper/WeakTiling.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.

WeakTiling.problem_4_1

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/weak-tiling-bounded-density/blob/5d10499e1932cc017b7aaf8e931926dc969bd8f7/lean/WeakTilingProblem41FC.lean#L11484-L11487.

Problem 4.1. Let \(\Omega \subset \mathbb{R}\) be a finite union of intervals and \(\nu\) a weak tiling measure for \(\Omega\). Must \(\mathrm{supp}(\nu)\) have bounded density?

The answer is positive: Kenta Kitamura (KitaKen1 on GitHub) has given a Lean proof (weak-tiling-bounded-density).

theorem problem_4_1 :
    ∀ (Ω : Set ℝ) (_ : IsFiniteUnionOfIntervals Ω)
      (ν : Measure ℝ) (_ : IsWeakTilingMeasure Ω ν), HasBoundedDensity ν.support

Category research solved; AMS 42 Harmonic analysis on Euclidean spaces, 46 Functional analysis. Declared in FormalConjectures/Paper/WeakTiling.lean, line 90.

WeakTiling.problem_4_2

Open: stated without proof.

Problem 4.2. Let \(\Omega \subset \mathbb{R}\) be a finite union of three or more intervals. If \(\Omega\) weakly tiles its complement, must it also tile its complement properly?

theorem problem_4_2 :
    ∀ (n : ℕ) (_ : 3 ≤ n) (Ω : Set ℝ)
      (_ : IsUnionOfNIntervals n Ω) (ν : Measure ℝ) (_ : IsWeakTilingMeasure Ω ν),
      ∃ T : Set ℝ, IsProperTiling Ω T

Category research open; AMS 42 Harmonic analysis on Euclidean spaces, 46 Functional analysis. Declared in FormalConjectures/Paper/WeakTiling.lean, line 99.

WeakTiling.problem_4_3

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/weak-tiling-counterexample/blob/5bf93234cc51f02fd7681407d77dcebde592f3ac/formal-conjectures-v4.27.0/WeakTilingCounterexample.lean.

Problem 4.3. Let \(\Omega \subset \mathbb{R}\) be a finite union of intervals and \(\nu\) a weak tiling measure for \(\Omega\). Must \(\nu\) be expressible as a convex combination of proper tiling measures?

The answer is negative.

An AI-assisted investigation by Kenta Kitamura produced a counterexample for \(\Omega = (0,1) \cup (2,3) \cup (12,13) \cup (30,31)\). A finite computation shows that every convex combination of proper tiling measures for this \(\Omega\) assigns equal mass to \(\{7\}\) and \(\{15\}\). However, the constructed weak tiling measure \(\nu\) satisfies \(\nu(\{7\}) = \frac{1}{2}\) and \(\nu(\{15\}) = 0\), so \(\nu\) cannot be expressed as a convex combination of proper tiling measures.

theorem problem_4_3 :
    ¬ ∀ (Ω : Set ℝ) (_ : IsFiniteUnionOfIntervals Ω)
      (ν : Measure ℝ) (_ : IsWeakTilingMeasure Ω ν),
      ∃ (T : ℕ → Set ℝ) (c : ℕ → ℝ≥0), (∀ i, IsProperTiling Ω (T i)) ∧ ∑' i : ℕ, c i = 1 ∧
      ν = Measure.sum
        (fun i => (c i : ℝ≥0∞) • Measure.sum (fun t : T i => Measure.dirac (t : ℝ)))

Category research solved; AMS 42 Harmonic analysis on Euclidean spaces, 46 Functional analysis. Declared in FormalConjectures/Paper/WeakTiling.lean, line 123.

Sources

• FormalConjectures/Paper/WeakTiling.lean at 2055e5ad
• Geometric implications of weak tiling

LeanWeakTiling.problem_4_1 · WeakTiling.problem_4_2 · WeakTiling.problem_4_3

TheoremZagier's Conjecture on Multiple Zeta Values#

References: - [Za94] Zagier, Don. "Values of zeta functions and their applications." First European Congress of Mathematics Paris, July 6–10, 1992: Vol. II: Invited Lectures (Part 2). Basel: Birkhäuser Basel, 1994. - [Co18] Combariza, Germán AG. "A few conjectures about the multiple zeta values." ACM Communications in Computer Algebra 52.1 (2018): 11-20. - [Te02] T. Terasoma. Mixed Tate motives and multiple zeta values. Invent. Math., 149(2):339–369, 2002. - [DG05] P. Deligne and A. Goncharov. Groupes fondamentaux motiviques de Tate mixte. Ann. Sci. Ecole Norm. Sup. (4), 38(1):1–56, 2005. - OEIS A000931

Quoted from FormalConjectures/Paper/ZagierMZV.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 7 test statements, counted here but not shown.

ZagierMZV.zagier_conjecture

Open: stated without proof.

Zagier's conjecture

The \(\mathbb{Q}\)-dimension of the vector space spanned by all multiple zeta values of weight \(n\) equals \(d_n\), where \(d_n\) is the Zagier dimension sequence satisfying \(d_0 = 1\), \(d_1 = 0\), \(d_2 = 1\), and \(d_n = d_{n-2} + d_{n-3}\) for \(n \geq 3\).

theorem zagier_conjecture :
    ∀ n : ℕ, Module.finrank ℚ (mzvSpanOfWeight n) = zagierDim n

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Paper/ZagierMZV.lean, line 97.

ZagierMZV.zagier_upper_bound

Solved: stated here without proof.

Upper bound [Te02, DG05]

The dimension of the \(\mathbb{Q}\)-vector space of MZVs of weight \(n\) is at most \(d_n\).

theorem zagier_upper_bound :
    ∀ n : ℕ, Module.finrank ℚ (mzvSpanOfWeight n) ≤ zagierDim n

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Paper/ZagierMZV.lean, line 107.

Sources

• FormalConjectures/Paper/ZagierMZV.lean at 2055e5ad
• OEIS A000931

LeanZagierMZV.zagier_conjecture · ZagierMZV.zagier_upper_bound

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.