TxGraffiti Conjecture 2: zero… to The Dixmier Conjecture

TheoremTxGraffiti Conjecture 2: zero forcing versus independence (cubic graphs)#

Reference: arxiv/2507.17780 In Reverie Together: Ten Years of Mathematical Discovery with a Machine Collaborator by Randy Davila, Boris Brimkov, Ryan Pepper

Conjecture 2 (open since 2017) asserts that for every connected graph \(G\) with maximum degree at most \(3\) and \(G \ne K_4\),

\[Z(G) \le \alpha(G) + 1,\]

where \(Z(G)\) is the zero forcing number and \(\alpha(G)\) the independence number.

Quoted from FormalConjectures/Arxiv/2507.17780/2.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.

Arxiv.«2507.17780».tx_graffiti_conjecture_2

Solved: stated here without proof.

TxGraffiti Conjecture 2: for every connected graph \(G\) with \(\Delta(G) \le 3\) and \(G \ne K_4\),

\[Z(G) \le \alpha(G) + 1.\]

This conjecture is false. Fischer gives a connected 24-vertex counterexample with maximum degree \(3\); see arXiv:2607.23664.

theorem tx_graffiti_conjecture_2 :
    ¬ ∀ (V : Type) [Fintype V] [DecidableEq V] (G : SimpleGraph V)
      [DecidableRel G.Adj] (_hConn : G.Connected)
      (_hDeg : G.maxDegree ≤ 3)
      (_hNotK4 : G = ⊤ → Fintype.card V ≠ 4),
      zeroForcingNumber G ≤ G.indepNum + 1

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Arxiv/2507.17780/2.lean, line 73.

Sources
LeanArxiv.«2507.17780».tx_graffiti_conjecture_2

TheoremTxGraffiti Conjecture 3: independent domination versus saturation (regular)#

Reference: arxiv/2507.17780 In Reverie Together: Ten Years of Mathematical Discovery with a Machine Collaborator by Randy Davila, Boris Brimkov, Ryan Pepper

Conjecture 3 (open since 2020) asserts that for every \(r\)-regular graph \(G\) (every vertex has degree \(r\)),

\[i(G) \le \mu^*(G),\]

where \(i(G)\) is the independent domination number and \(\mu^*(G)\) the saturation number (minimum size of a maximal matching).

Quoted from FormalConjectures/Arxiv/2507.17780/3.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.

Arxiv.«2507.17780».tx_graffiti_conjecture_3

Open: stated without proof.

TxGraffiti Conjecture 3: for every \(r\)-regular graph \(G\) (\(r \ge 1\)),

\[i(G) \le \mu^*(G).\]

This conjecture is open.

theorem tx_graffiti_conjecture_3 (V : Type) [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj]
    (r : ℕ) (_hReg : ∀ v, G.degree v = r) (_hr : 1 ≤ r) :
    G.indepDominationNumber ≤ G.saturationNumber

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/Arxiv/2507.17780/3.lean, line 48.

Sources
LeanArxiv.«2507.17780».tx_graffiti_conjecture_3

TheoremTxGraffiti Conjecture 4: the saturation number versus the harmonic index#

Reference: arxiv/2507.17780 In Reverie Together: Ten Years of Mathematical Discovery with a Machine Collaborator by Randy Davila, Boris Brimkov, Ryan Pepper

TxGraffiti is an automated conjecturing program, a successor of Fajtlowicz's Graffiti and DeLaViña's Graffiti.pc. Conjecture 4 in the cited collection asserts a bound between two graph invariants:

  • the saturation number \(\mu^*(G)\) (SimpleGraph.saturationNumber), the minimum number of edges in a maximal matching of \(G\);
  • the harmonic index \(H(G)\) (SimpleGraph.harmonicIndex), \(\sum_{uv \in E(G)} 2 / (\deg u + \deg v)\).

The conjecture is false. It was first refuted by Bıyıkoğlu, who exhibited a family of counterexamples — a disjoint union of edges joined to an independent set — with unbounded ratio \(\mu^*/H\). That the smallest counterexample has order \(9\), namely the friendship graph \(F_4\) formalised below, and that the windmill family has an exact limiting ratio, are established in Gupta.

References: - A Note on the TxGraffiti Conjecture about Harmonic Index and Minimum Maximal Matching Number, Türker Bıyıkoğlu, MATCH Commun. Math. Comput. Chem. 96 (2026), no. 3, 1097–1099 — the first refutation. - The saturation number is not bounded by the harmonic index, C. Gupta — the order-\(9\) minimality of \(F_4\) (formalised below) and the exact windmill limit.

Quoted from FormalConjectures/Arxiv/2507.17780/4.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.

Arxiv.«2507.17780».tx_graffiti_conjecture_4

Proved here.

TxGraffiti Conjecture 4: for every nontrivial connected graph \(G\), the saturation number is at most the harmonic index, \(\mu^*(G) \le H(G)\).

This conjecture is FALSE.

Counterexample. The friendship graph \(F_4\) (friendshipF4) is connected and nontrivial, with \(\mu^*(F_4) = 4\) and \(H(F_4) = 18/5\). Indeed the four rim edges \(\{1,2\}, \{3,4\}, \{5,6\}, \{7,8\}\) form a maximal matching of size \(4\), and no maximal matching is smaller, so \(\mu^*(F_4) = 4\); the eight spokes contribute \(2/(8+2) = 1/5\) each and the four rim edges contribute \(2/(2+2) = 1/2\) each, giving \(H(F_4) = 8 \cdot 1/5 + 4 \cdot 1/2 = 18/5\). Since \(4 > 18/5\), the bound fails.

More generally the friendship graphs \(F_k\) satisfy \(\mu^*(F_k) = k\) and \(H(F_k) = 2k/(k+1) + k/2\), so the conjecture fails for every \(k \ge 4\). An exhaustive search confirms that \(F_4\) is the smallest counterexample (order \(9\)). The unbounded separation was first shown by Bıyıkoğlu, whose family of edges joined to an independent set makes \(\mu^*/H\) arbitrarily large; the windmill generalisation and its exact limit appear in arXiv:2606.15761.

theorem tx_graffiti_conjecture_4 :
    ¬ ∀ (V : Type) [Fintype V] [DecidableEq V] [Nontrivial V] (G : SimpleGraph V)
      [DecidableRel G.Adj] (_hConn : G.Connected),
      (G.saturationNumber : ℚ) ≤ G.harmonicIndex

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Arxiv/2507.17780/4.lean, line 95.

Sources
LeanArxiv.«2507.17780».tx_graffiti_conjecture_4

TheoremFirst Proof, Theorem 4#

Reference: arxiv/2602.05192v2 First Proof by Mohammed Abouzaid, Andrew J. Blumberg, Martin Hairer, Joe Kileel, Tamara G. Kolda, Paul D. Nelson, Daniel Spielman, Nikhil Srivastava, Rachel Ward, Shmuel Weinberger, Lauren Williams

Quoted from FormalConjectures/Arxiv/2602.05192/FirstProof4.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. It also has 3 test statements, counted here but not shown.

Arxiv.«2602.05192».four

Solved: stated here; a Lean proof is at https://github.com/frenzymath/Archon-FirstProof-Results/blob/main/FirstProof/FirstProof4/Problem4.lean.

Is it true that if \(p(x)\) and \(q(x)\) are monic real-rooted polynomials of degree \(n\), then

\[\frac{1}{\Phi_n(p\boxplus_n q)} \ge \frac{1}{\Phi_n(p)}+\frac{1}{\Phi_n(q)}?\]

arxiv/2602.05192v2 contains a proof.

theorem four : ∀ (p q : ℝ[X]) (n : ℕ), FourProp p q n

Category research solved; AMS 26 Real functions. Declared in FormalConjectures/Arxiv/2602.05192/FirstProof4.lean, line 158.

Arxiv.«2602.05192».four_2

Solved: stated here without proof.

Is it true that if \(p(x)\) and \(q(x)\) are monic real-rooted polynomials of degree \(2\), then

\[\frac{1}{\Phi_2(p\boxplus_n q)} \ge \frac{1}{\Phi_2(p)}+\frac{1}{\Phi_2(q)}?\]
theorem four_2 : ∀ (p q : ℝ[X]), FourProp p q 2

Category research solved; AMS 26 Real functions. Declared in FormalConjectures/Arxiv/2602.05192/FirstProof4.lean, line 167.

Arxiv.«2602.05192».four_3

Solved: stated here without proof.

Is it true that if \(p(x)\) and \(q(x)\) are monic real-rooted polynomials of degree \(3\), then

\[\frac{1}{\Phi_3(p\boxplus_n q)} \ge \frac{1}{\Phi_3(p)}+\frac{1}{\Phi_3(q)}?\]
theorem four_3 : ∀ (p q : ℝ[X]), FourProp p q 3

Category research solved; AMS 26 Real functions. Declared in FormalConjectures/Arxiv/2602.05192/FirstProof4.lean, line 176.

Sources
LeanArxiv.«2602.05192».four · Arxiv.«2602.05192».four_2 · Arxiv.«2602.05192».four_3

TheoremFirst Proof, Theorem 6#

Reference: arxiv/2602.05192v2 First Proof by Mohammed Abouzaid, Andrew J. Blumberg, Martin Hairer, Joe Kileel, Tamara G. Kolda, Paul D. Nelson, Daniel Spielman, Nikhil Srivastava, Rachel Ward, Shmuel Weinberger, Lauren Williams

Quoted from FormalConjectures/Arxiv/2602.05192/FirstProof6.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.

Arxiv.«2602.05192».epsilon_light_subset_exists

Solved: stated here; a Lean proof is at https://github.com/frenzymath/Archon-FirstProof-Results/blob/main/FirstProof/FirstProof6/Problem6.lean.

Does there exist a constant \(c > 0\) so that for every graph \(G\) and every \(\epsilon\) between \(0\) and \(1\), \(V\) contains an \(\epsilon\)-light subset \(S\) of size at least \(c \epsilon |V|\)?

theorem epsilon_light_subset_exists :
    ∃ (c : ℝ), c > 0 ∧ ∀ (n : ℕ) (G : SimpleGraph (Fin n)) (ε : ℝ),
    0 < ε → ε < 1 →
    ∃ (S : Finset (Fin n)), IsEpsilonLight G ε S ∧ (S.card : ℝ) ≥ c * ε * n

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Arxiv/2602.05192/FirstProof6.lean, line 61.

Sources
LeanArxiv.«2602.05192».epsilon_light_subset_exists

TheoremGroup structure via subgroup counts#

Reference: arXiv:2604.08040v1 Group Structure via Subgroup Counts by Angsuman Das, Hiranya Kishore Dey, Khyati Sharma (2026)

For a finite group \(G\), let \(\mathrm{cyc}(G)\) denote the number of cyclic subgroups of \(G\), and let \(t = \pi(G)\) denote the number of distinct prime divisors of \(|G|\).

The paper establishes several structural results of the form "if \(\mathrm{cyc}(G)\) or \(\mathrm{sub}(G)\) is small relative to \(2^t\), then \(G\) has a strong structural property":

  • \(\mathrm{cyc}(G) < 5 \cdot 2^{t-2} \implies G\) is nilpotent (Theorem 3.1)
  • \(\mathrm{cyc}(G) < 2^{t+1} \implies G\) is supersolvable (Theorem 4.2)
  • \(\mathrm{sub}(G) < 59 \cdot 2^{t-3} \implies G\) is solvable (Theorem 5.3)

Conjecture 5.5 proposes the analogue for solvability via cyclic subgroup count: if \(\mathrm{cyc}(G) < 2^{t+2}\), then \(G\) is solvable.

  • In-Paper Location: Conjecture 5.5, Section 5 "Solvability of a group from \(\mathrm{sub}(G)\)" (PDF page 15)
  • OpenConjecture ID: 1512

Quoted from FormalConjectures/Arxiv/2604.08040/Conjecture5_5.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. It also has 5 test statements, counted here but not shown.

Arxiv.«2604.08040».solvable_of_cyc_lt

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/das-dey-sharma-conjecture-5-5/blob/7a2600dd6471536cf246ad8d78d756e130d2fe9e/lean/Conjecture55FC.lean#L15-L18.

Conjecture 5.5 (Das, Dey, Sharma 2026): If a finite group G satisfies \(\mathrm{cyc}(G) < 2^{t+2}\), where \(t = \pi(G)\) is the number of distinct prime divisors of \(|G|\), then G is solvable.

This is Theorem 7.1 of the second version of the paper, arXiv:2604.08040v2 (Das, Dey, Galindo, Sharma), proved there using the classification of finite simple groups.

The Lean proof here by Kenta Kitamura instead uses only the Feit–Thompson theorem and the Gorenstein–Walter classification of groups with dihedral Sylow 2-subgroups, together with counting arguments on Sylow 2-subgroups and families of cyclic subgroups.

theorem solvable_of_cyc_lt :
    ∀ (G : Type) [Group G] [Fintype G],
      cyc G < 2 ^ (numPrimeFactors G + 2) → Group.IsSolvable G

Category research solved; AMS 20 Group theory and generalizations. Declared in FormalConjectures/Arxiv/2604.08040/Conjecture5_5.lean, line 81.

Arxiv.«2604.08040».nilpotent_of_cyc_lt

Solved: stated here without proof.

Theorem 3.1. Below \(5 \cdot 2^{t-2}\) cyclic subgroups, the group is nilpotent.

theorem nilpotent_of_cyc_lt (h : cyc G < 5 * 2 ^ (numPrimeFactors G - 2)) :
    Group.IsNilpotent G

Category research solved; AMS 20 Group theory and generalizations. Declared in FormalConjectures/Arxiv/2604.08040/Conjecture5_5.lean, line 90.

Arxiv.«2604.08040».solvable_of_cyc_lt_two_pow_succ

Solved: stated here without proof.

Theorem 4.2. Below \(2^{t+1}\) cyclic subgroups, the group is supersolvable.

Stated here as solvability, which supersolvability implies, since Mathlib does not currently have a standalone IsSupersolvable class.

theorem solvable_of_cyc_lt_two_pow_succ (h : cyc G < 2 ^ (numPrimeFactors G + 1)) :
    Group.IsSolvable G

Category research solved; AMS 20 Group theory and generalizations. Declared in FormalConjectures/Arxiv/2604.08040/Conjecture5_5.lean, line 101.

Sources
LeanArxiv.«2604.08040».solvable_of_cyc_lt · Arxiv.«2604.08040».nilpotent_of_cyc_lt · Arxiv.«2604.08040».solvable_of_cyc_lt_two_pow_succ

TheoremDean's conjecture on cycles of length divisible by `k`#

References: - arxiv/2605.02731 Existence of cycles of length divisible by 3 or 4 by Ilkyoo Choi, Hojin Chu, Ringi Kim, Boram Park, where this is Conjecture 1.1. - [De88] Dean, N., Open problem, in Cycles and Rays. (1988). - [DeLeSa93] Dean, N. and Lesniak, L. and Saito, A., Cycles of length 0 modulo 4 in graphs. Discrete Math. (1993), 133--139. - [ChSa94] Chen, G. and Saito, A., Graphs with a cycle of length divisible by three. J. Combin. Theory Ser. B (1994), 277--292. - [LuMaZh26] Luo, Yufan and Ma, Jie and Zhao, Ziyuan, Dean's conjecture and cycles modulo k. arXiv:2601.13552 (2026).

Quoted from FormalConjectures/Arxiv/2605.02731/DeanCycles.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: 2 open and 3 solved. It also has 2 test statements, counted here but not shown.

Arxiv.«2605.02731».dean_conjecture

Open: stated without proof.

Conjecture 1.1 (Dean, 1988). For every integer \(k \geq 3\), every finite simple graph with minimum degree at least \(k\) contains a cycle whose length is divisible by \(k\).

A cycle has length at least 3, so the divisor is never 0 and the statement is not satisfied for a trivial reason. SimpleGraph.minDegree is 0 on a graph with no vertices and on a graph with no edges, so the hypothesis excludes both.

theorem dean_conjecture :
    ∀ (k : ℕ), 3 ≤ k → ∀ (V : Type) [Fintype V] [DecidableEq V]
      (G : SimpleGraph V) [DecidableRel G.Adj], k ≤ G.minDegree →
        ∃ m ∈ G.cycleLengths, k ∣ m

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/Arxiv/2605.02731/DeanCycles.lean, line 51.

Arxiv.«2605.02731».dean_conjecture.variants.five

Open: stated without proof.

The case \(k = 5\). This is the only case of the conjecture that is still open.

theorem dean_conjecture.variants.five :
    ∀ (V : Type) [Fintype V] [DecidableEq V] (G : SimpleGraph V)
      [DecidableRel G.Adj], 5 ≤ G.minDegree → ∃ m ∈ G.cycleLengths, 5 ∣ m

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/Arxiv/2605.02731/DeanCycles.lean, line 61.

Arxiv.«2605.02731».dean_conjecture.variants.three

Solved: stated here without proof.

The case \(k = 3\), proved by Chen and Saito [ChSa94].

theorem dean_conjecture.variants.three {V : Type} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (hG : 3 ≤ G.minDegree) :
    ∃ m ∈ G.cycleLengths, 3 ∣ m

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Arxiv/2605.02731/DeanCycles.lean, line 70.

Arxiv.«2605.02731».dean_conjecture.variants.four

Solved: stated here without proof.

The case \(k = 4\), proved by Dean, Lesniak and Saito [DeLeSa93].

theorem dean_conjecture.variants.four {V : Type} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (hG : 4 ≤ G.minDegree) :
    ∃ m ∈ G.cycleLengths, 4 ∣ m

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Arxiv/2605.02731/DeanCycles.lean, line 79.

Arxiv.«2605.02731».dean_conjecture.variants.six_le

Solved: stated here without proof.

The cases \(k \geq 6\), proved by Luo, Ma and Zhao [LuMaZh26]. With [ChSa94] and [DeLeSa93] this leaves dean_conjecture.variants.five as the only open case.

theorem dean_conjecture.variants.six_le {V : Type} [Fintype V] [DecidableEq V] {k : ℕ}
    (hk : 6 ≤ k) (G : SimpleGraph V) [DecidableRel G.Adj] (hG : k ≤ G.minDegree) :
    ∃ m ∈ G.cycleLengths, k ∣ m

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Arxiv/2605.02731/DeanCycles.lean, line 89.

Sources
LeanArxiv.«2605.02731».dean_conjecture · Arxiv.«2605.02731».dean_conjecture.variants.five · Arxiv.«2605.02731».dean_conjecture.variants.three · Arxiv.«2605.02731».dean_conjecture.variants.four · Arxiv.«2605.02731».dean_conjecture.variants.six_le

TheoremFernandes' conjecture on the 2-generation of even direct product permutation groups#

Reference: arxiv/2605.12342 Groups of permutations that are even on maximal proper subsets, and related monoids Reference: - arxiv/2605.12342 Groups of permutations that are even on maximal proper subsets, and related monoids by Vítor H. Fernandes - K26

For positive integers \(m, n \ge 2\), let \(\mathrm{S}_m \times \mathrm{S}_n\) be the direct product of symmetric groups on \([m] = \{1, \dots, m\}\) and \([n'] = \{1', \dots, n'\}\). Define

\[ \Gamma_{m \oplus n} = \{(\sigma_1, \sigma_2) \in \mathrm{S}_m \times \mathrm{S}_n : \mathrm{sgn}(\sigma_1) = \mathrm{sgn}(\sigma_2)\} \]

to be the index-\(2\) subgroup of pairs of permutations with equal parity, i.e., those whose product action on \([m] \cup [n']\) is an even permutation.

It is known that \(\mathrm{rank}(\Gamma_{2 \oplus 2}) = 1\), \(\mathrm{rank}(\Gamma_{3 \oplus 3}) = 3\), \(\mathrm{rank}(\Gamma_{4 \oplus 3}) = 3\), and \(\mathrm{rank}(\Gamma_{4 \oplus 4}) = 3\).

Conjecture 1 (Fernandes, 2026): For all integers \(m \ge n \ge 2\) such that \((m, n) \notin \{(2,2), (3,3), (4,3), (4,4)\}\), the group \(\Gamma_{m \oplus n}\) has rank \(2\) (i.e., is \(2\)-generated).

Quoted from FormalConjectures/Arxiv/2605.12342/Conjecture1.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: 5 solved.

Arxiv.«2605.12342».conjecture_1

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/fernandes-conjecture-1-lean/blob/c9360c5608ed2bb3bb5670a68d683cd5a83089d6/lean/FernandesConjecture/FormalConjecturesWrapper.lean#L14-L24.

Conjecture 1 (Fernandes, 2026): Let \(m \ge n \ge 2\) be integers with \((m, n) \notin \{(2,2), (3,3), (4,3), (4,4)\}\). Then the group

\[ \Gamma_{m \oplus n} = \{(\sigma_1, \sigma_2) \in \mathrm{S}_m \times \mathrm{S}_n : \mathrm{sgn}(\sigma_1) = \mathrm{sgn}(\sigma_2)\} \]

has rank \(2\), i.e., minimal generating set of size \(2\).

Note: Fernandes states the conjecture for groups of exact rank \(2\), which is why \((2,2)\) is in the exception list: \(\Gamma_{2 \oplus 2} \cong C_2\) has rank \(1\). The formalised conclusion ∃ g₁ g₂, closure {g₁, g₂} = ⊤ encodes 2-generation (at most \(2\) generators), which \(\Gamma_{2 \oplus 2}\) also satisfies. The other three exceptions \((3,3), (4,3), (4,4)\) have rank \(3\) and are genuinely not 2-generated.

The proof was developed and formalized by Kenta Kitamura, see [K26] for more details.

theorem conjecture_1 {m n : ℕ} (hm2 : 2 ≤ m) (hn2 : 2 ≤ n) (hmn : n ≤ m)
    (h_except : (m, n) ∉ ({(2, 2), (3, 3), (4, 3), (4, 4)} : Set (ℕ × ℕ))) :
    ∃ g₁ g₂ : gammaSubgroup m n, Subgroup.closure {g₁, g₂} = ⊤

Category research solved; AMS 20 Group theory and generalizations. Declared in FormalConjectures/Arxiv/2605.12342/Conjecture1.lean, line 97.

Arxiv.«2605.12342».conjecture_1.variants.rank_2_2

Proved here.

It is known that \(\Gamma_{2 \oplus 2} \cong C_2\) has rank \(1\): it is cyclic, generated by a single element.

theorem conjecture_1.variants.rank_2_2 :
    ∃ g : gammaSubgroup 2 2, Subgroup.closure {g} = ⊤

Category research solved; AMS 20 Group theory and generalizations. Declared in FormalConjectures/Arxiv/2605.12342/Conjecture1.lean, line 107.

Arxiv.«2605.12342».conjecture_1.variants.rank_3_3

Solved: stated here without proof.

It is known that \(\Gamma_{3 \oplus 3}\) has rank \(3\): it is not \(2\)-generated.

theorem conjecture_1.variants.rank_3_3 :
    ∀ h₁ h₂ : gammaSubgroup 3 3, Subgroup.closure {h₁, h₂} ≠ ⊤

Category research solved; AMS 20 Group theory and generalizations. Declared in FormalConjectures/Arxiv/2605.12342/Conjecture1.lean, line 129.

Arxiv.«2605.12342».conjecture_1.variants.rank_4_3

Solved: stated here without proof.

It is known that \(\Gamma_{4 \oplus 3}\) has rank \(3\): it is not \(2\)-generated.

theorem conjecture_1.variants.rank_4_3 :
    ∀ h₁ h₂ : gammaSubgroup 4 3, Subgroup.closure {h₁, h₂} ≠ ⊤

Category research solved; AMS 20 Group theory and generalizations. Declared in FormalConjectures/Arxiv/2605.12342/Conjecture1.lean, line 137.

Arxiv.«2605.12342».conjecture_1.variants.rank_4_4

Solved: stated here without proof.

It is known that \(\Gamma_{4 \oplus 4}\) has rank \(3\): it is not \(2\)-generated.

theorem conjecture_1.variants.rank_4_4 :
    ∀ h₁ h₂ : gammaSubgroup 4 4, Subgroup.closure {h₁, h₂} ≠ ⊤

Category research solved; AMS 20 Group theory and generalizations. Declared in FormalConjectures/Arxiv/2605.12342/Conjecture1.lean, line 145.

Sources
LeanArxiv.«2605.12342».conjecture_1 · Arxiv.«2605.12342».conjecture_1.variants.rank_2_2 · Arxiv.«2605.12342».conjecture_1.variants.rank_3_3 · Arxiv.«2605.12342».conjecture_1.variants.rank_4_3 · Arxiv.«2605.12342».conjecture_1.variants.rank_4_4

TheoremConvexity of Fisher information along the heat flow#

Can the functional \(\mathcal{D}[f]\) be negative for an admissible density \(f\)? Equivalently, is the Fisher information of the Gaussian heat flow always convex in time? This is Problem (iii) of [ZFGW26, Section 7.3]; it is known in dimensions \(d \le 4\) and left open for \(d \ge 5\) [ZFGW26, Section 7.2].

References: - [ZFGW26] J. Zou, L. Fan, J. Gao and J. Wang, A Hexagonal Counterexample to Log-Convexity of Fisher Information Along the Heat Flow, arXiv:2605.18081 (2026). https://arxiv.org/abs/2605.18081 - [Ki26] K. Kitamura, Fisher information along the heat flow is not convex, Lean 4 formalization (2026), GitHub repository.

Quoted from FormalConjectures/Arxiv/2605.18081/FisherInformationConvexity.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.

Arxiv.«2605.18081».fisherInformationConvexity

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/fisher-information-nonconvexity/blob/fe6ade9846c53e5cb0dcbc00eca359c83f8d0f55/lean/Fisher41/FC/Main.lean#L37.

Is the Fisher information convex along the heat flow for every admissible density [ZFGW26, Section 7.3, Problem (iii)]? The answer is no [Ki26].

theorem fisherInformationConvexity :
    ¬ ∀ (d : ℕ) (f : EuclideanSpace ℝ (Fin d) → ℝ), IsAdmissible f →
      ConvexOn ℝ (Set.Ioi 0) (fun t => fisherInformation (heatFlow f t))

Category research solved; AMS 35 Partial differential equations, 60 Probability theory and stochastic processes. Declared in FormalConjectures/Arxiv/2605.18081/FisherInformationConvexity.lean, line 84.

Arxiv.«2605.18081».fisherInformationConvexity.variants.smooth

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/fisher-information-nonconvexity/blob/fe6ade9846c53e5cb0dcbc00eca359c83f8d0f55/lean/Fisher41/FC/Main.lean#L48.

The same question for every smooth positive probability density with finite Fisher information. The answer is no [Ki26].

theorem fisherInformationConvexity.variants.smooth :
    ¬ ∀ (d : ℕ) (f : EuclideanSpace ℝ (Fin d) → ℝ), IsWeaklyAdmissible f →
      ConvexOn ℝ (Set.Ioi 0) (fun t => fisherInformation (heatFlow f t))

Category research solved; AMS 35 Partial differential equations, 60 Probability theory and stochastic processes. Declared in FormalConjectures/Arxiv/2605.18081/FisherInformationConvexity.lean, line 94.

Sources
LeanArxiv.«2605.18081».fisherInformationConvexity · Arxiv.«2605.18081».fisherInformationConvexity.variants.smooth

TheoremBondy's conjecture on longest cycles in highly connected graphs#

References: - arxiv/2606.03696 Longest cycles and Dirac-type results in highly connected graphs by Jie Ma, Bo Ning, Ziyuan Zhao, where this is Conjecture 1. - [Bo80] Bondy, J. A., Longest paths and cycles in graphs of high degree. (1980).

Take a k-connected graph with a large minimum degree. Bondy says that the graph outside any longest cycle holds no long path.

The case k = 1 is Dirac's theorem and the case k = 2 is the theorem of Nash-Williams. The case k = 3 is proved. The cases k ≥ 4 are open.

Quoted from FormalConjectures/Arxiv/2606.03696/BondyLongestCycles.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: 1 open and 5 solved.

Arxiv.«2606.03696».bondy_conjecture

Open: stated without proof.

Conjecture 1 (Bondy, 1980). Let \(k \geq 1\) and let \(G\) be a \(k\)-connected graph on \(n\) vertices. If \(\delta(G) \geq \frac{n + k(k-1)}{k+1}\), then for every longest cycle \(C\) of \(G\), every path in \(G - V(C)\) has at most \(k-1\) vertices.

The bound on the number of vertices of a path is written as + 1 ≤ k rather than ≤ k - 1, because subtraction on ℕ is truncated. The two forms agree for k ≥ 1.

A longest cycle is a cycle whose length is the circumference of G.

theorem bondy_conjecture :
    ∀ (k : ℕ), 1 ≤ k → ∀ (V : Type) [Fintype V] [DecidableEq V]
      (G : SimpleGraph V) [DecidableRel G.Adj], IsKConnected G k →
      ((Fintype.card V : ℝ) + k * (k - 1)) / (k + 1) ≤ G.minDegree →
      ∀ (a : V) (C : G.Walk a a), C.IsCycle → C.length = G.circumference →
      ∀ (u v : offWalk C) (P : (G.induce (offWalk C)).Walk u v), P.IsPath →
        P.support.length + 1 ≤ k

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/Arxiv/2606.03696/BondyLongestCycles.lean, line 60.

Arxiv.«2606.03696».bondy_conjecture.variants.one

Solved: stated here without proof.

The case \(k = 1\) is Dirac's theorem. The condition reads \(\delta(G) \geq n/2\), and no path in \(G - V(C)\) can hold a vertex, so a longest cycle covers every vertex.

theorem bondy_conjecture.variants.one {G : SimpleGraph V} [DecidableRel G.Adj]
    (hG : IsKConnected G 1) (hd : ((Fintype.card V : ℝ)) / 2 ≤ G.minDegree)
    {a : V} (C : G.Walk a a) (hC : C.IsCycle) (hlong : C.length = G.circumference)
    (u v : offWalk C) (P : (G.induce (offWalk C)).Walk u v) (hP : P.IsPath) :
    P.support.length + 1 ≤ 1

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Arxiv/2606.03696/BondyLongestCycles.lean, line 74.

Arxiv.«2606.03696».bondy_conjecture.variants.two

Solved: stated here without proof.

The case \(k = 2\) is the theorem of Nash-Williams.

theorem bondy_conjecture.variants.two {G : SimpleGraph V} [DecidableRel G.Adj]
    (hG : IsKConnected G 2) (hd : ((Fintype.card V : ℝ) + 2) / 3 ≤ G.minDegree)
    {a : V} (C : G.Walk a a) (hC : C.IsCycle) (hlong : C.length = G.circumference)
    (u v : offWalk C) (P : (G.induce (offWalk C)).Walk u v) (hP : P.IsPath) :
    P.support.length + 1 ≤ 2

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Arxiv/2606.03696/BondyLongestCycles.lean, line 85.

Arxiv.«2606.03696».bondy_conjecture.variants.three

Solved: stated here without proof.

The case \(k = 3\) is proved.

theorem bondy_conjecture.variants.three {G : SimpleGraph V} [DecidableRel G.Adj]
    (hG : IsKConnected G 3) (hd : ((Fintype.card V : ℝ) + 6) / 4 ≤ G.minDegree)
    {a : V} (C : G.Walk a a) (hC : C.IsCycle) (hlong : C.length = G.circumference)
    (u v : offWalk C) (P : (G.induce (offWalk C)).Walk u v) (hP : P.IsPath) :
    P.support.length + 1 ≤ 3

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Arxiv/2606.03696/BondyLongestCycles.lean, line 96.

Arxiv.«2606.03696».bondy_conjecture.variants.large_explicit

Solved: stated here without proof.

Theorem 1.1 (Ma-Ning-Zhao, 2026), explicit threshold. Bondy's conjecture holds when \(n \geq 5k^2 + 7k\). This value of \(n_k\) is given after Theorem 1.1 and in its reduction from Theorem 2.2.

theorem bondy_conjecture.variants.large_explicit :
    ∀ k : ℕ, 1 ≤ k → ∀ (V : Type) [Fintype V] [DecidableEq V]
      (G : SimpleGraph V) [DecidableRel G.Adj],
      5 * k ^ 2 + 7 * k ≤ Fintype.card V → IsKConnected G k →
      ((Fintype.card V : ℝ) + k * (k - 1)) / (k + 1) ≤ G.minDegree →
      ∀ (a : V) (C : G.Walk a a), C.IsCycle → C.length = G.circumference →
      ∀ (u v : offWalk C) (P : (G.induce (offWalk C)).Walk u v), P.IsPath →
        P.support.length + 1 ≤ k

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Arxiv/2606.03696/BondyLongestCycles.lean, line 109.

Arxiv.«2606.03696».bondy_conjecture.variants.large

Proved here.

Theorem 1.1 (Ma-Ning-Zhao, 2026). The conjecture holds for every graph with enough vertices. The full conjecture, for graphs of every size, stays open.

theorem bondy_conjecture.variants.large :
    ∀ k : ℕ, 1 ≤ k → ∃ N : ℕ, ∀ (V : Type) [Fintype V] [DecidableEq V]
      (G : SimpleGraph V) [DecidableRel G.Adj], N ≤ Fintype.card V → IsKConnected G k →
      ((Fintype.card V : ℝ) + k * (k - 1)) / (k + 1) ≤ G.minDegree →
      ∀ (a : V) (C : G.Walk a a), C.IsCycle → C.length = G.circumference →
      ∀ (u v : offWalk C) (P : (G.induce (offWalk C)).Walk u v), P.IsPath →
        P.support.length + 1 ≤ k

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Arxiv/2606.03696/BondyLongestCycles.lean, line 124.

Sources
LeanArxiv.«2606.03696».bondy_conjecture · Arxiv.«2606.03696».bondy_conjecture.variants.one · Arxiv.«2606.03696».bondy_conjecture.variants.two · Arxiv.«2606.03696».bondy_conjecture.variants.three · Arxiv.«2606.03696».bondy_conjecture.variants.large_explicit · Arxiv.«2606.03696».bondy_conjecture.variants.large

TheoremPlanar \(L_p\)-Rogers-Shephard, the equality case#

Reference: arxiv/2607.03582 \(L_p\)-Rogers-Shephard type inequalities for \(L_p\)-zonoids and symmetric bodies by Matthieu Fradelizi, Auttawich Manui, Mark Meyer, Cheikh Saliou Ndiaye

Formal proof of Conjecture 5: Kenta Kitamura, Lean proofs for the symmetric L_p Rogers–Shephard conjectures.

Corollary 29 bounds \(|K \oplus_p -K|\) against \(|K|\) for planar convex bodies with a centre of symmetry containing the origin, and notes that parallelograms with a vertex at the origin attain it. Conjecture 5 asks whether they are the only bodies that do.

Quoted from FormalConjectures/Arxiv/2607.03582/LpRogersShephard.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. It also has 1 API statement, counted here but not shown.

Arxiv.«2607.03582».volume_lpSum_le

Solved: stated here without proof.

Corollary 29 (Fradelizi-Manui-Meyer-Ndiaye, 2026). For a planar convex body \(K\) with a centre of symmetry containing the origin and \(p > 1\),

\[|K \oplus_p -K| \leq \left(\frac{2\Gamma(1+1/q)^2}{\Gamma(1+2/q)} + 2\right)|K|,\]

where \(q\) is the Hölder conjugate of \(p\).

theorem volume_lpSum_le (K : Set ℝ²) (hK : Convex ℝ K) (hKc : IsCompact K)
    (hKi : (interior K).Nonempty) (hsym : HasCentreOfSymmetry K) (h0 : (0 : ℝ²) ∈ K)
    (p q : ℝ) (hp : 1 < p) (hq : 1 / p + 1 / q = 1) :
    volume (lpSum p K (-K)) ≤ ENNReal.ofReal (rsConstant q) * volume K

Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/Arxiv/2607.03582/LpRogersShephard.lean, line 75.

Arxiv.«2607.03582».volume_lpSum_eq_of_isParallelogramAtOrigin

Solved: stated here without proof.

Parallelograms with a vertex at the origin attain the bound, which is the sharpness half of Corollary 29.

theorem volume_lpSum_eq_of_isParallelogramAtOrigin (K : Set ℝ²)
    (hpar : IsParallelogramAtOrigin K) (p q : ℝ) (hp : 1 < p) (hq : 1 / p + 1 / q = 1) :
    volume (lpSum p K (-K)) = ENNReal.ofReal (rsConstant q) * volume K

Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/Arxiv/2607.03582/LpRogersShephard.lean, line 86.

Arxiv.«2607.03582».isParallelogramAtOrigin_of_volume_lpSum_eq

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/lp-rogers-shephard-conjectures-lean/blob/c646c668c0568b8533bf5534abcf02aab4d2df72/lean/LpRogersShephardFC.lean#L108-L128.

Conjecture 5 (Fradelizi-Manui-Meyer-Ndiaye, 2026). Among planar convex bodies with a centre of symmetry containing the origin, for \(p > 1\), equality in Corollary 29 holds only for parallelograms with a vertex at the origin.

theorem isParallelogramAtOrigin_of_volume_lpSum_eq :
    ∀ (K : Set ℝ²), Convex ℝ K → IsCompact K → (interior K).Nonempty →
      HasCentreOfSymmetry K → (0 : ℝ²) ∈ K → ∀ p q : ℝ, 1 < p → 1 / p + 1 / q = 1 →
        volume (lpSum p K (-K)) = ENNReal.ofReal (rsConstant q) * volume K →
          IsParallelogramAtOrigin K

Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/Arxiv/2607.03582/LpRogersShephard.lean, line 100.

Sources
LeanArxiv.«2607.03582».volume_lpSum_le · Arxiv.«2607.03582».volume_lpSum_eq_of_isParallelogramAtOrigin · Arxiv.«2607.03582».isParallelogramAtOrigin_of_volume_lpSum_eq

TheoremThe microscopic weighting on a metric space#

Reference: arxiv/2607.05349 The microscopic weighting on a metric space by Emily Roff, Simon Willerton

Quoted from FormalConjectures/Arxiv/2607.05349/MicroscopicWeighting.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.

Arxiv.«2607.05349».concentration_unique

Textbook result, proved here.

All gaugings of a symmetric matrix share one concentration, so \(\mathrm{con}\) is an attribute of the matrix. The source records this after Definition 2.3, as the calculation \(c = c\mathbf{1}^T v' = (v^TA^T)v' = v^T(c'\mathbf{1}) = c'\), and Definition 2.4 rests on it.

theorem concentration_unique {M : Matrix X X ℝ} (hM : M.IsSymm) {g g' : X → ℝ} {c c' : ℝ}
    (h : IsGauging M g c) (h' : IsGauging M g' c') : c = c'

Category textbook; AMS 15 Linear and multilinear algebra; matrix theory. Declared in FormalConjectures/Arxiv/2607.05349/MicroscopicWeighting.lean, line 70.

Arxiv.«2607.05349».microscopic_weighting_iff_finite_concentration

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/microscopic-weighting-counterexample/blob/eff8979/lean/MicroscopicWeightingCounterexampleFC.lean#L886-L894.

Conjecture 3.3 (Roff-Willerton, 2026). A finite metric space admits a microscopic weighting if and only if its distance matrix has finite concentration.

Nonempty is needed and not just tidiness. On the empty space every gauging condition fails, since ∑ i, g i is 0 rather than 1, while X → ℝ is a subsingleton so the weighting converges trivially. The equivalence would be false there for reasons that have nothing to do with the question.

The answer is false as proved by Kenta Kitamura assisted by ChatGPT 5.6 sol.

The proof proceeds by constructing an explicit counterexample: a finite metric space on 10 points that has finite concentration but does not admit a microscopic weighting. The metric space is defined by the following \(10 \times 10\) distance matrix \(A\):

\[ \begin{pmatrix} 0 & 116 & 236 & 231 & 260 & 124 & 64 & 290 & 266 & 64 \cr 116 & 0 & 312 & 268 & 296 & 112 & 64 & 280 & 296 & 64 \cr 236 & 312 & 0 & 68 & 40 & 236 & 288 & 68 & 36 & 288 \cr 231 & 268 & 68 & 0 & 34 & 237 & 288 & 72 & 40 & 288 \cr 260 & 296 & 40 & 34 & 0 & 264 & 320 & 40 & 68 & 320 \cr 124 & 112 & 236 & 237 & 264 & 0 & 64 & 280 & 264 & 64 \cr 64 & 64 & 288 & 288 & 320 & 64 & 0 & 312 & 320 & 120 \cr 290 & 280 & 68 & 72 & 40 & 280 & 312 & 0 & 40 & 312 \cr 266 & 296 & 36 & 40 & 68 & 264 & 320 & 40 & 0 & 320 \cr 64 & 64 & 288 & 288 & 320 & 64 & 120 & 312 & 320 & 0 \end{pmatrix} \]

The space has finite concentration, demonstrated by the explicit gauging \(g\):

\[ g = \frac{1}{24842973905} \begin{pmatrix} 3672468740 \cr 6389133731 \cr 9124217512 \cr 5612262448 \cr -6875621136 \cr 2754831248 \cr 0 \cr 10758780188 \cr -6593098826 \cr 0 \end{pmatrix} \]

which gives \(A g = \frac{4111107017312}{24842973905} \mathbf{1}\).

To prove that it does not admit a microscopic weighting, we provide a vector \(v \in \ker A\):

\[ v = \begin{pmatrix} -2 \cr -1 \cr 3 \cr 4 \cr -4 \cr -2 \cr 2 \cr 2 \cr -4 \cr 2 \end{pmatrix} \]

along with a row-space certificate \(q\) for the entrywise square matrix \(B = A^{\circ 2}\) satisfying \(q A = v^\top B\):

\[ q^\top = \frac{1}{128472094291} \begin{pmatrix} 43681853675722 \cr -53873248293642 \cr -66890627544007 \cr -81187181670120 \cr 24308499983196 \cr 40819375894674 \cr 0 \cr 54690260644468 \cr 35226831040652 \cr 0 \end{pmatrix} \]

This certificate shows that the obstruction \(v^\top B\) annihilates \(\ker A\), making it impossible to construct a convergent weighting.

theorem microscopic_weighting_iff_finite_concentration :
    ¬ ∀ (X : Type) [Fintype X] [DecidableEq X] [Nonempty X] [MetricSpace X],
      HasMicroscopicWeighting X ↔ HasFiniteConcentration (distanceMatrix X)

Category research solved; AMS 15 Linear and multilinear algebra; matrix theory, 51 Geometry. Declared in FormalConjectures/Arxiv/2607.05349/MicroscopicWeighting.lean, line 146.

Arxiv.«2607.05349».hasFiniteConcentration_of_hasMicroscopicWeighting

Solved: stated here without proof.

One direction is known: a microscopic weighting implies finite concentration (Theorem 3.1(3)). Together with the conjecture above this leaves the converse, that finite concentration is enough.

theorem hasFiniteConcentration_of_hasMicroscopicWeighting
    (h : HasMicroscopicWeighting X) : HasFiniteConcentration (distanceMatrix X)

Category research solved; AMS 15 Linear and multilinear algebra; matrix theory, 51 Geometry. Declared in FormalConjectures/Arxiv/2607.05349/MicroscopicWeighting.lean, line 156.

Arxiv.«2607.05349».hasMicroscopicWeighting_iff_of_isUnit

Solved: stated here without proof.

Theorem 3.8: the conjecture is known when the distance matrix is invertible, and the microscopic weighting is then the unique gauging.

theorem hasMicroscopicWeighting_iff_of_isUnit (h : IsUnit (distanceMatrix X).det) :
    HasMicroscopicWeighting X ↔ HasFiniteConcentration (distanceMatrix X)

Category research solved; AMS 15 Linear and multilinear algebra; matrix theory, 51 Geometry. Declared in FormalConjectures/Arxiv/2607.05349/MicroscopicWeighting.lean, line 165.

Sources
LeanArxiv.«2607.05349».concentration_unique · Arxiv.«2607.05349».microscopic_weighting_iff_finite_concentration · Arxiv.«2607.05349».hasFiniteConcentration_of_hasMicroscopicWeighting · Arxiv.«2607.05349».hasMicroscopicWeighting_iff_of_isUnit

TheoremInteger values of \(\tan(\arctan 1 + \arctan 2 + \cdots + \arctan n)\)#

References: - arxiv/2607.05739 Integer values of \(\tan(\arctan 1+\arctan 2+\cdots+\arctan n)\) are rare by Ken Ono - [AMM08] T. Amdeberhan, L. A. Medina, and V. H. Moll, Arithmetical properties of a sequence arising from an arctangent sum, J. Number Theory 128 (2008), no. 6, 1807-1846. - TanArctan, a Lean formalisation of the three results of [Ono26], MIT licensed. Its P, A, B and x are the definitions used here.

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

Arxiv.«2607.05739».tan_arctan_sum_not_integer

Open: stated without proof.

Conjecture (Amdeberhan-Medina-Moll, 2008). For every integer \(n \geq 5\), the value

\[x_n = \tan(\arctan 1 + \arctan 2 + \cdots + \arctan n)\]

is not an integer.

theorem tan_arctan_sum_not_integer :
    ∀ n : ℕ, 5 ≤ n → ¬ IsIntegerValue n

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Arxiv/2607.05739/TanArctanSum.lean, line 67.

Arxiv.«2607.05739».x_succ

Textbook result, stated without proof.

\(x_n\) satisfies \(x_1 = 1\) and \(x_n = \dfrac{x_{n-1} + n}{1 - n x_{n-1}}\), which is the tangent addition formula.

theorem x_succ (n : ℕ) (hn : 1 ≤ n) :
    x (n + 1) = (x n + (n + 1)) / (1 - (n + 1) * x n)

Category textbook; AMS 11 Number theory. Declared in FormalConjectures/Arxiv/2607.05739/TanArctanSum.lean, line 74.

Arxiv.«2607.05739».x_eq_tan_sum_arctan

Textbook result, stated without proof.

\(x_n\) is the tangent of the partial sum of arctangents it is named for.

theorem x_eq_tan_sum_arctan (n : ℕ) (hn : 1 ≤ n) :
    (x n : ℝ) = Real.tan (∑ k ∈ Finset.Icc 1 n, Real.arctan k)

Category textbook; AMS 11 Number theory. Declared in FormalConjectures/Arxiv/2607.05739/TanArctanSum.lean, line 80.

Arxiv.«2607.05739».kernel_dvd_of_eq_intCast

Solved: stated here; a Lean proof is at https://github.com/AxiomMath/TanArctan/blob/5382d3c20ee3f30e2cbd84362eb07a7e93250348/output/solution.lean#L176.

An integer value is divisible in a way that forces it to be large: if \(x_n = m\) then \(K_n \mid 1 + m^2\), and \(|m| \geq \sqrt{K_n - 1}\) once \(K_n > 1\).

theorem kernel_dvd_of_eq_intCast {n : ℕ} (hn : 1 ≤ n) (hA : A n ≠ 0) {m : ℤ}
    (hx : x n = (m : ℚ)) :
    ((kernel n : ℤ) ∣ (1 + m ^ 2)) ∧
      (1 < kernel n → Real.sqrt ((kernel n : ℝ) - 1) ≤ |(m : ℝ)|)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Arxiv/2607.05739/TanArctanSum.lean, line 106.

Arxiv.«2607.05739».exists_near_half_pi

Solved: stated here; a Lean proof is at https://github.com/AxiomMath/TanArctan/blob/5382d3c20ee3f30e2cbd84362eb07a7e93250348/output/solution.lean#L453.

Every exceptional index sits close to a multiple of \(\pi/2\) in angle.

theorem exists_near_half_pi {n : ℕ} (hn : n ∈ exceptional) :
    ∃ j : ℤ, |angleSum n - (j : ℝ) * (Real.pi / 2)| < 2 / (n : ℝ)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Arxiv/2607.05739/TanArctanSum.lean, line 116.

Arxiv.«2607.05739».exceptional_ncard_le

Solved: stated here; a Lean proof is at https://github.com/AxiomMath/TanArctan/blob/5382d3c20ee3f30e2cbd84362eb07a7e93250348/output/solution.lean#L975.

The exceptional indices are sparse: \(\#(E \cap [1,N]) = O(\log N)\). This is the sense in which integer values are rare, and it is what [Ono26] proves.

theorem exceptional_ncard_le : ∃ (C : ℝ) (N₀ : ℕ), 0 < C ∧ ∀ N : ℕ, N₀ ≤ N →
    ((exceptional ∩ Set.Icc 1 N).ncard : ℝ) ≤ C * Real.log N

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Arxiv/2607.05739/TanArctanSum.lean, line 125.

Sources
LeanArxiv.«2607.05739».tan_arctan_sum_not_integer · Arxiv.«2607.05739».x_succ · Arxiv.«2607.05739».x_eq_tan_sum_arctan · Arxiv.«2607.05739».kernel_dvd_of_eq_intCast · Arxiv.«2607.05739».exists_near_half_pi · Arxiv.«2607.05739».exceptional_ncard_le

TheoremThe Alon-Tarsi short cycle cover conjecture#

References: - [AlTa85] Alon, N. and Tarsi, M., Covering multigraphs by simple circuits. SIAM J. Algebraic Discrete Methods (1985), 345--350. - arxiv/2607.06396 Some new results on Sylvester colorings of cubic graphs by Luca Ferrarini, Vahan Mkrtchyan, where this is Conjecture 4.

This file states the finite simple-graph specialization of the source, which allows parallel edges.

Every bridgeless simple graph has a list of cycles covering every edge whose lengths sum to at most \(\frac{7}{5}|E|\).

Quoted from FormalConjectures/Arxiv/2607.06396/AlonTarsi.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. It also has 2 test statements and 5 API statements, counted here but not shown.

Arxiv.«2607.06396».alon_tarsi_short_cycle_cover

Open: stated without proof.

Conjecture 4 (Alon-Tarsi, 1985), simple-graph specialization. Every bridgeless simple graph has a list of cycles covering every edge, with \(\sum_{C} |E(C)| \leq \frac{7}{5}|E(G)|\).

theorem alon_tarsi_short_cycle_cover :
    ∀ (V : Type) [Fintype V] [DecidableEq V] (G : SimpleGraph V)
      [DecidableRel G.Adj], G.IsBridgeless →
      ∃ C : Multiset (Cycle G), IsCycleCover G C ∧
        (totalLength C : ℚ) ≤ 7 / 5 * #G.edgeFinset

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/Arxiv/2607.06396/AlonTarsi.lean, line 89.

Sources
LeanArxiv.«2607.06396».alon_tarsi_short_cycle_cover

TheoremMinimum modulus for the unique multiset-sum problem#

References: - arxiv/2607.08366 Minimum modulus for the unique multiset-sum problem by José A. R. Fonollosa - jarfo/min-modulus, the author's Lean development of the paper's Main Theorem. Section 7 of the paper describes it.

The paper's Main Theorem fixes the super-increasing set \(\{2^k - 1\}\) and pins the least modulus at which it is valid. Conjecture 1 says no other set of \(n\) residues does better, and is open.

Quoted from FormalConjectures/Arxiv/2607.08366/MinModulus.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 5 API statements, counted here but not shown.

Arxiv.«2607.08366».min_modulus

Open: stated without proof.

Conjecture 1 (Fonollosa, 2026). For every \(n \geq 2\) and every \(N < 2^n - 2^{\lfloor \log_2 n\rfloor}\), no set of \(n\) residues mod \(N\) is valid.

Equivalently the super-increasing set \(\{2^k - 1 : 0 \leq k \leq n-1\}\) attains the least valid modulus, which is minModulus n.

0 < N excludes N = 0, where ZMod 0 is ℤ rather than a finite modulus and {1, 2} is valid, which would make the statement false for a reason unrelated to the question.

theorem min_modulus :
    ∀ n N : ℕ, 2 ≤ n → 0 < N → N < minModulus n →
      ∀ A : Finset (ZMod N), #A = n → ¬ IsValidMod A

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Arxiv/2607.08366/MinModulus.lean, line 85.

Arxiv.«2607.08366».exists_isValidMod_minModulus

Solved: stated here; a Lean proof is at https://github.com/jarfo/min-modulus/blob/e7c78dd63955092b5f8d8a5fa826476337c0f4be/MinModulus/UniqueSums.lean#L837-L838.

Theorem A (Fonollosa, 2026). minModulus n admits a valid set of n residues, the super-increasing set \(\{2^k - 1 : 0 \leq k \leq n - 1\}\). This bounds the least valid modulus from above; that no smaller modulus works is the open half, stated in min_modulus.

theorem exists_isValidMod_minModulus (n : ℕ) (hn : 2 ≤ n) :
    ∃ A : Finset (ZMod (minModulus n)), #A = n ∧ IsValidMod A

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Arxiv/2607.08366/MinModulus.lean, line 99.

Sources
LeanArxiv.«2607.08366».min_modulus · Arxiv.«2607.08366».exists_isValidMod_minModulus

TheoremThe Balister–Győri–Schelp conjecture#

References: - Perfect Matchings with Prescribed Differences Beyond Hall: The Two-Hole Problem by Aryeh Lev Zabokritskiy (Yohananov) (2026) - Coloring vertices and edges of a graph by nonempty subsets of a set by P. N. Balister, E. Győri, and R. H. Schelp, European Journal of Combinatorics 32(4), 533–537 (2011)

Quoted from FormalConjectures/Arxiv/2607.08630/BalisterGyoriSchelp.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.

Arxiv.«2607.08630».balister_gyori_schelp_conjecture

Open: stated without proof.

The Balister–Győri–Schelp conjecture (Conjecture 1): for \(s \ge 2\), every zero-sum list of \(2^{s-1}\) nonzero vectors in \(\mathbb{F}_2^s\) is the prescribed-difference profile of a perfect matching of \(\mathbb{F}_2^s\).

The equivalence \(e\) indexes the two endpoints of each pair and ensures that the pairs are disjoint and exhaust the ambient vector space.

theorem balister_gyori_schelp_conjecture (s : ℕ) (hs : 2 ≤ s)
    (v : Fin (2 ^ (s - 1)) → 𝔽₂ s)
    (hv_nonzero : ∀ i, v i ≠ 0)
    (hv_sum : ∑ i, v i = 0) :
    ∃ e : Fin (2 ^ (s - 1)) × Fin 2 ≃ 𝔽₂ s,
      ∀ i, e (i, 0) + e (i, 1) = v i

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/Arxiv/2607.08630/BalisterGyoriSchelp.lean, line 45.

Sources
LeanArxiv.«2607.08630».balister_gyori_schelp_conjecture

TheoremThe Maxwell conjecture#

References: - arXiv:2607.27197 The Maxwell Conjecture is False by Philip Arathoon, Gavin Ball and Matthew D. Kvalheim (2026) - Mystery of point charges by Andrei Gabrielov, Dmitry Novikov and Boris Shapiro, Proc. London Math. Soc. 95 (2007), 443-472 - Maxwell's conjecture on three point charges with equal magnitudes by Ya-Lun Tsai, Phys. D 309 (2015), 86-98

In his 1873 Treatise on Electricity and Magnetism (§113) J. C. Maxwell discusses the number of equilibria of the electric field generated by \(n\) point charges. Based on their reading of that passage, Gabrielov, Novikov and Shapiro formulated the Maxwell conjecture: if the critical points of the electrostatic potential

\[V(x) = \sum_{j=1}^n \frac{q_j}{\|x - a_j\|}\]

generated by \(n\) point charges are all non-degenerate, then their number is at most \((n-1)^2\).

Arathoon, Ball and Kvalheim disproved the conjecture by exhibiting a configuration of five positive point charges — three unit charges at the vertices of an equilateral triangle together with two small charges placed symmetrically on the axis of the triangle — whose potential has at least \(24\) non-degenerate critical points, whereas \((5-1)^2 = 16\).

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

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

Arxiv.«2607.27197».maxwell_conjecture.counterexample_morse

Solved: stated here without proof.

The second half of Theorem 1 of Arathoon–Ball–Kvalheim: after a small perturbation of the charge strengths, the counterexample potential is a Morse function, i.e. it has finitely many critical points, all of which are non-degenerate, and there are still at least \(24\) of them.

Reference: arXiv:2607.27197

theorem maxwell_conjecture.counterexample_morse :
    ∃ (q : Fin 5 → ℝ) (a : Fin 5 → EuclideanSpace ℝ (Fin 3)), Function.Injective a ∧
      (∀ j, 0 < q j) ∧
      (∀ x ∈ equilibria q a, HasNondegenerateHessianAt (potential q a) x) ∧
      (equilibria q a).Finite ∧ 24 ≤ (equilibria q a).encard

Category research solved; AMS 31 Potential theory, 78 Optics, electromagnetic theory. Declared in FormalConjectures/Arxiv/2607.27197/MaxwellConjecture.lean, line 94.

Arxiv.«2607.27197».maxwell_conjecture

Proved here.

Maxwell's conjecture is false: Arathoon, Ball and Kvalheim exhibit five point charges whose potential is a Morse function with at least \(24 > 16 = (5-1)^2\) critical points.

Reference: arXiv:2607.27197

theorem maxwell_conjecture : ¬ Conjecture

Category research solved; AMS 31 Potential theory, 78 Optics, electromagnetic theory. Declared in FormalConjectures/Arxiv/2607.27197/MaxwellConjecture.lean, line 108.

Arxiv.«2607.27197».maxwell_conjecture.counterexample

Solved: stated here without proof.

Theorem 1 of Arathoon–Ball–Kvalheim: there is an \(\varepsilon_0 > 0\) such that for all \(0 < \varepsilon < \varepsilon_0\) the potential generated by the five charges located at \(a_1, \dots, a_5\) with respective strengths \(1, 1, 1, q_\varepsilon, q_\varepsilon\), where \(q_\varepsilon = \frac{3}{4}\varepsilon^3 - \frac{5}{32}\varepsilon^5\), admits at least \(24\) non-degenerate critical points.

Reference: arXiv:2607.27197

theorem maxwell_conjecture.counterexample :
    ∃ ε₀ > 0, ∀ ε ∈ Set.Ioo 0 ε₀,
      24 ≤ (nondegenerateEquilibria (counterexampleCharges ε)
        (counterexamplePositions ε)).encard

Category research solved; AMS 31 Potential theory, 78 Optics, electromagnetic theory. Declared in FormalConjectures/Arxiv/2607.27197/MaxwellConjecture.lean, line 159.

Arxiv.«2607.27197».maxwell_conjecture.phiZero_critical_points

Solved: stated here without proof.

Lemma 2 of Arathoon–Ball–Kvalheim: the polynomial \(\Phi_0\) has exactly \(21\) critical points, all of which are non-degenerate. These are the critical points into which the central equilibrium of the equilateral triangle bifurcates when the two axial charges are added.

Reference: arXiv:2607.27197

theorem maxwell_conjecture.phiZero_critical_points :
    {p : EuclideanSpace ℝ (Fin 3) | ∇ phiZero p = 0}.encard = 21 ∧
      ∀ p, ∇ phiZero p = 0 → HasNondegenerateHessianAt phiZero p

Category research solved; AMS 31 Potential theory, 78 Optics, electromagnetic theory. Declared in FormalConjectures/Arxiv/2607.27197/MaxwellConjecture.lean, line 187.

Arxiv.«2607.27197».maxwell_conjecture.iterated

Solved: stated here without proof.

Proposition 1 of Arathoon–Ball–Kvalheim: iterating the construction, for every \(m \geq 0\) there is a configuration of \(3 + 2m\) positive point charges whose potential has a finite number \(k \geq 4 + 20m\) of critical points, all of which are non-degenerate. In particular the ratio of critical points to charges is asymptotically at least \(10\).

Reference: arXiv:2607.27197

theorem maxwell_conjecture.iterated (m : ℕ) :
    ∃ (q : Fin (3 + 2 * m) → ℝ) (a : Fin (3 + 2 * m) → EuclideanSpace ℝ (Fin 3)),
      Function.Injective a ∧ (∀ j, 0 < q j) ∧
      (∀ x ∈ equilibria q a, HasNondegenerateHessianAt (potential q a) x) ∧
      (equilibria q a).Finite ∧ 4 + 20 * m ≤ (equilibria q a).encard

Category research solved; AMS 31 Potential theory, 78 Optics, electromagnetic theory. Declared in FormalConjectures/Arxiv/2607.27197/MaxwellConjecture.lean, line 201.

Arxiv.«2607.27197».maxwell_conjecture.variants.two_charges

Textbook result, stated without proof.

Maxwell's bound is trivially achieved for \(n = 2\): the potential of two point charges at distinct locations has at most \((2-1)^2 = 1\) critical point.

Reference: arXiv:2607.27197

theorem maxwell_conjecture.variants.two_charges (q : Fin 2 → ℝ)
    (a : Fin 2 → EuclideanSpace ℝ (Fin 3)) (ha : Function.Injective a) (hq : ∀ j, q j ≠ 0) :
    (equilibria q a).encard ≤ 1

Category textbook; AMS 31 Potential theory, 78 Optics, electromagnetic theory. Declared in FormalConjectures/Arxiv/2607.27197/MaxwellConjecture.lean, line 215.

Arxiv.«2607.27197».maxwell_conjecture.variants.three_equal_magnitudes

Solved: stated here without proof.

Maxwell's conjecture holds for three point charges of equal magnitudes: the potential of three such charges, if all of its critical points are non-degenerate, has at most \((3-1)^2 = 4\) of them.

Reference: Maxwell's conjecture on three point charges with equal magnitudes by Ya-Lun Tsai

theorem maxwell_conjecture.variants.three_equal_magnitudes (q : Fin 3 → ℝ)
    (a : Fin 3 → EuclideanSpace ℝ (Fin 3)) (ha : Function.Injective a) (hq : ∀ j, q j ≠ 0)
    (hq' : ∀ i j, |q i| = |q j|)
    (hnd : ∀ x ∈ equilibria q a, HasNondegenerateHessianAt (potential q a) x) :
    (equilibria q a).encard ≤ 4

Category research solved; AMS 31 Potential theory, 78 Optics, electromagnetic theory. Declared in FormalConjectures/Arxiv/2607.27197/MaxwellConjecture.lean, line 229.

Arxiv.«2607.27197».maxwell_conjecture.variants.three_charges

Open: stated without proof.

Maxwell's conjecture for three point charges of arbitrary strengths: if all critical points of the potential of three point charges are non-degenerate, then there are at most \((3-1)^2 = 4\) of them. This remains open.

Reference: arXiv:2607.27197

theorem maxwell_conjecture.variants.three_charges :
    ∀ (q : Fin 3 → ℝ) (a : Fin 3 → EuclideanSpace ℝ (Fin 3)), Function.Injective a →
      (∀ j, q j ≠ 0) →
      (∀ x ∈ equilibria q a, HasNondegenerateHessianAt (potential q a) x) →
      (equilibria q a).encard ≤ 4

Category research open; AMS 31 Potential theory, 78 Optics, electromagnetic theory. Declared in FormalConjectures/Arxiv/2607.27197/MaxwellConjecture.lean, line 244.

Arxiv.«2607.27197».maxwell_conjecture.variants.polynomial_bound

Open: stated without proof.

Is the number of equilibria of \(n\) point charges bounded by a polynomial in \(n\)?

With the quadratic bound of Maxwell's conjecture gone, the gap between the known bounds is wide: the constructions of Arathoon–Ball–Kvalheim give configurations with at least \(10n\) equilibria asymptotically, while the best known upper bounds — \(2^{2n^2}(3n)^{2n}\) by Gabrielov–Novikov–Shapiro, \(5 \cdot 9^{3+n}\) by Zolotov and \(2^n (3n-2)^3\) by Edelsbrunner–Fillmore–Oliveira — are all exponential in \(n\).

References: arXiv:2607.27197, Counting equilibria of the electrostatic potential

theorem maxwell_conjecture.variants.polynomial_bound :
    ∃ C d : ℕ, ∀ (n : ℕ), 0 < n → ∀ (q : Fin n → ℝ) (a : Fin n → EuclideanSpace ℝ (Fin 3)),
      Function.Injective a → (∀ j, q j ≠ 0) →
      (∀ x ∈ equilibria q a, HasNondegenerateHessianAt (potential q a) x) →
      (equilibria q a).encard ≤ (C * n ^ d : ℕ)

Category research open; AMS 31 Potential theory, 78 Optics, electromagnetic theory. Declared in FormalConjectures/Arxiv/2607.27197/MaxwellConjecture.lean, line 264.

Sources
LeanArxiv.«2607.27197».maxwell_conjecture.counterexample_morse · Arxiv.«2607.27197».maxwell_conjecture · Arxiv.«2607.27197».maxwell_conjecture.counterexample · Arxiv.«2607.27197».maxwell_conjecture.phiZero_critical_points · Arxiv.«2607.27197».maxwell_conjecture.iterated · Arxiv.«2607.27197».maxwell_conjecture.variants.two_charges · Arxiv.«2607.27197».maxwell_conjecture.variants.three_equal_magnitudes · Arxiv.«2607.27197».maxwell_conjecture.variants.three_charges · Arxiv.«2607.27197».maxwell_conjecture.variants.polynomial_bound

TheoremBanach-Mazur Rotation Problem#

References: - arxiv/math.0110202 A note on Banach--Mazur problem by Beata Randrianantoanina - mathoverflow/41211 Easy proof of the fact that isotropic spaces are Euclidean

Quoted from FormalConjectures/Arxiv/math.0110202/BanachMazurRotation.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 3 API statements, counted here but not shown.

Arxiv.«math.0110202».banach_mazur_rotation_problem

Open: stated without proof.

The Banach--Mazur rotation problem asks whether every separable Banach space whose group of linear isometric equivalences acts transitively on the unit sphere is linearly isometric to a Hilbert space.

theorem banach_mazur_rotation_problem :
    ∀ (E : Type*) [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [SeparableSpace E]
      [IsPretransitive (E ≃ₗᵢ[ℝ] E) (sphere (0 : E) 1)], ∃ (H : Type*) (_ : NormedAddCommGroup H)
      (_ : InnerProductSpace ℝ H),
      Nonempty (E ≃ₗᵢ[ℝ] H)

Category research open; AMS 46 Functional analysis. Declared in FormalConjectures/Arxiv/math.0110202/BanachMazurRotation.lean, line 90.

Arxiv.«math.0110202».banach_mazur_rotation_problem.finite_dimensional

Solved: stated here without proof.

Every finite-dimensional real normed space whose isometry group acts transitively on the unit sphere is Euclidean.

theorem banach_mazur_rotation_problem.finite_dimensional {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E] [FiniteDimensional ℝ E] [IsPretransitive (E ≃ₗᵢ[ℝ] E) (sphere (0 : E) 1)] :
    InnerProductSpaceable E

Category research solved; AMS 46 Functional analysis. Declared in FormalConjectures/Arxiv/math.0110202/BanachMazurRotation.lean, line 100.

Sources
LeanArxiv.«math.0110202».banach_mazur_rotation_problem · Arxiv.«math.0110202».banach_mazur_rotation_problem.finite_dimensional

TheoremFinite generation of the cohomology of finite-dimensional Hopf algebras#

Let \(A\) be a finite-dimensional Hopf algebra over a field \(k\), and view \(k\) as an \(A\)-module through the counit. The cohomology ring

\[H^*(A, k) = \mathrm{Ext}^*_A(k, k) = \bigoplus_{n \ge 0} \mathrm{Ext}^n_A(k, k)\]

is a graded-commutative \(k\)-algebra under the Yoneda product. The finite generation conjecture asserts that it is a finitely generated \(k\)-algebra, and that \(\mathrm{Ext}^*_A(k, M)\) is a finitely generated module over it for every finite-dimensional \(A\)-module \(M\). Etingof and Ostrik state it for every finite tensor category; the finite-dimensional modules over a finite-dimensional Hopf algebra form the main class of examples, and the conjecture is open already in this case.

The conjecture is not due to any one author. The question for a finite-dimensional Hopf algebra was asked by a number of mathematicians and had circulated since at least the 1990s: Friedlander and Suslin record it while expressly declining to answer it ("We do not know whether it is reasonable to expect finite generation of the cohomology of an arbitrary finite dimensional Hopf algebra"), and Friedlander and Negron later describe the conjecture as having "existed as a question at least since the 90's" and as "recently stated explicitly in the work of Etingof and Ostrik". What Etingof and Ostrik contribute is that explicit statement, together with its extension from Hopf algebras to every finite tensor category; it is their Conjecture 2.18 that is formalised here.

The conjecture holds when \(A\) is cocommutative, that is, when \(A\) is the group algebra of a finite group scheme (Friedlander–Suslin). For the group algebra \(k[G]\) of a finite group \(G\) it is the theorem of Evens and Venkov, proved for a \(p\)-group by Golod. Etingof and Ostrik note that it also holds when \(A\) is commutative.

Etingof and Ostrik work throughout the section containing the conjecture under the standing assumption that \(k\) is algebraically closed, whereas the statements below are for an arbitrary field. The generalisation is valid. For a field extension \(K/k\) one has \(\mathrm{Ext}^*_{A \otimes_k K}(K, K) \cong \mathrm{Ext}^*_A(k, k) \otimes_k K\), because \(k\) admits a resolution by finitely generated free \(A\)-modules and \(K\) is flat over \(k\); and finite generation descends, because the finitely many elements of \(R = \mathrm{Ext}^*_A(k, k)\) occurring in a finite set of \(K\)-algebra generators of \(R \otimes_k K\) generate a \(k\)-subalgebra \(R'\) with \(R' \otimes_k K = R \otimes_k K\), whence \(R' = R\) by faithful flatness. The same argument applies to the module statement. The theorems of Friedlander–Suslin and of Evens–Venkov are stated below over an arbitrary field because that is the generality in which they are proved.

\(\mathrm{Ext}\) is taken in the category of all \(A\)-modules rather than in the finite tensor category of finite-dimensional ones. For finite-dimensional \(A\) the two agree on finite-dimensional modules, as the module docstring of FormalConjecturesForMathlib.RingTheory.Bialgebra.Cohomology explains.

References: * arXiv:math/0301027 P. Etingof, V. Ostrik, Finite tensor categories, Mosc. Math. J. 4 (2004), no. 3, 627–654; Conjecture 2.18. * Friedlander–Suslin E. M. Friedlander, A. Suslin, Cohomology of finite group schemes over a field, Invent. Math. 127 (1997), 209–270. * Evens L. Evens, The cohomology ring of a finite group, Trans. Amer. Math. Soc. 101 (1961), 224–239. * B. B. Venkov, Cohomology algebras for some classifying spaces, Dokl. Akad. Nauk SSSR 127 (1959), 943–944. * E. S. Golod, The cohomology ring of a finite \(p\)-group, Dokl. Akad. Nauk SSSR 125 (1959), 703–706. * Friedlander–Negron E. M. Friedlander, C. Negron, Cohomology for Drinfeld doubles of some infinitesimal group schemes, Algebra Number Theory 12 (2018), 1281–1309; the conjecture and its history, p. 1281. * Oberwolfach H. Krause, S. Witherspoon, J. J. Zhang (organisers), Mini-Workshop: Cohomology of Hopf Algebras and Tensor Categories, Oberwolfach Rep. (2019), 663–693; "asked by a number of mathematicians", p. 664.

Quoted from FormalConjectures/Arxiv/math.0301027/FiniteGenerationOfCohomology.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: 2 open and 3 solved. It also has 2 test statements, counted here but not shown.

HopfAlgebraCohomology.cohomologyRing_finiteType

Open: stated without proof.

Finite generation conjecture (Etingof–Ostrik, Conjecture 2.18, algebra part). For every finite-dimensional Hopf algebra \(A\) over a field \(k\), the cohomology ring \(H^*(A, k) = \mathrm{Ext}^*_A(k, k)\) is a finitely generated \(k\)-algebra.

theorem cohomologyRing_finiteType : Algebra.FiniteType k (cohomologyRing k A)

Category research open; AMS 16 Associative rings and algebras, 18 Category theory; homological algebra. Declared in FormalConjectures/Arxiv/math.0301027/FiniteGenerationOfCohomology.lean, line 96.

HopfAlgebraCohomology.cohomology_finite

Open: stated without proof.

Finite generation conjecture (Etingof–Ostrik, Conjecture 2.18, module part). For every finite-dimensional Hopf algebra \(A\) over a field \(k\) and every finite-dimensional \(A\)-module \(M\), the cohomology \(H^*(A, M) = \mathrm{Ext}^*_A(k, M)\) is a finitely generated module over \(H^*(A, k)\).

theorem cohomology_finite (M : ModuleCat.{u} A) [FiniteDimensional k M] :
    Module.Finite (cohomologyRing k A) (cohomology k A M)

Category research open; AMS 16 Associative rings and algebras, 18 Category theory; homological algebra. Declared in FormalConjectures/Arxiv/math.0301027/FiniteGenerationOfCohomology.lean, line 104.

HopfAlgebraCohomology.cohomologyRing_finiteType_of_isCocomm

Solved: stated here without proof.

Friedlander–Suslin. If \(A\) is a finite-dimensional cocommutative Hopf algebra over a field \(k\), that is, the group algebra of a finite group scheme over \(k\), then \(H^*(A, k)\) is a finitely generated \(k\)-algebra.

theorem cohomologyRing_finiteType_of_isCocomm [Coalgebra.IsCocomm k A] :
    Algebra.FiniteType k (cohomologyRing k A)

Category research solved; AMS 14 Algebraic geometry, 16 Associative rings and algebras, 18 Category theory; homological algebra. Declared in FormalConjectures/Arxiv/math.0301027/FiniteGenerationOfCohomology.lean, line 112.

HopfAlgebraCohomology.cohomology_finite_of_isCocomm

Solved: stated here without proof.

Friedlander–Suslin. If \(A\) is a finite-dimensional cocommutative Hopf algebra over a field \(k\) and \(M\) is a finite-dimensional \(A\)-module, then \(H^*(A, M)\) is a finitely generated module over \(H^*(A, k)\).

theorem cohomology_finite_of_isCocomm [Coalgebra.IsCocomm k A] (M : ModuleCat.{u} A)
    [FiniteDimensional k M] : Module.Finite (cohomologyRing k A) (cohomology k A M)

Category research solved; AMS 14 Algebraic geometry, 16 Associative rings and algebras, 18 Category theory; homological algebra. Declared in FormalConjectures/Arxiv/math.0301027/FiniteGenerationOfCohomology.lean, line 120.

HopfAlgebraCohomology.cohomologyRing_finiteType_monoidAlgebra

Solved: stated here without proof.

Evens–Venkov. For a finite group \(G\) and a field \(k\), the cohomology ring \(H^*(G, k) = \mathrm{Ext}^*_{k[G]}(k, k)\) of the group algebra \(k[G]\) is a finitely generated \(k\)-algebra.

theorem cohomologyRing_finiteType_monoidAlgebra (G : Type u) [Group G] [Finite G] :
    Algebra.FiniteType k (cohomologyRing k (MonoidAlgebra k G))

Category research solved; AMS 16 Associative rings and algebras, 20 Group theory and generalizations. Declared in FormalConjectures/Arxiv/math.0301027/FiniteGenerationOfCohomology.lean, line 128.

Sources
LeanHopfAlgebraCohomology.cohomologyRing_finiteType · HopfAlgebraCohomology.cohomology_finite · HopfAlgebraCohomology.cohomologyRing_finiteType_of_isCocomm · HopfAlgebraCohomology.cohomology_finite_of_isCocomm · HopfAlgebraCohomology.cohomologyRing_finiteType_monoidAlgebra

TheoremThe Dixmier Conjecture#

References: - [Dix68] Sur les algèbres de Weyl by Jacques Dixmier, Bull. Soc. Math. France 96 (1968), 209–242. The conjecture is Problem 1 (for the first Weyl algebra). - [BCW82] The Jacobian conjecture: reduction of degree and formal expansion of the inverse by Hyman Bass, Edwin H. Connell, David Wright, Bull. Amer. Math. Soc. 7 (1982), 287–330. Proves \(DC_n \Longrightarrow JC_n\). - [AvdE07] arxiv/math.0608009 On the equivalence of the Jacobian, Dixmier and Poisson Conjectures in any characteristic by Kossivi Adjamagbo, Arno van den Essen. Published as A proof of the equivalence of the Dixmier, Jacobian and Poisson conjectures, Acta Math. Vietnam. 32 (2007), 205–214. - [Tsu05] Endomorphisms of Weyl algebra and p-curvatures by Yoshifumi Tsuchimoto, Osaka J. Math. 42 (2005), 435–452. Proves the stable equivalence \(JC \Longleftrightarrow DC\) independently. - [BKK07] The Jacobian Conjecture is stably equivalent to the Dixmier Conjecture by Alexei Belov-Kanel, Maxim Kontsevich, Moscow Math. J. 7 (2007), 209–218. Independent proof of the stable equivalence. - [Bav20] The Jacobian Conjecture implies the Dixmier Problem by Vladimir Bavula; published in Springer Proceedings in Mathematics & Statistics 317 (2020). A third proof. - [Alp26] Counterexample to the Jacobian conjecture by Levent Alpöge (2026), disproving the Jacobian conjecture in dimension \(3\) - [Lon26] An Explicit Counterexample to the Rank-Two Poisson Conjecture by Christopher D. Long (2026), disproving \(PC_2\)

The Dixmier Conjecture \(DC_n\) asserts that, over a field K of characteristic zero, every endomorphism of the n-th Weyl algebra \(A_n(K)\) is an automorphism. For \(n = 1\) this is Problem 1 of [Dix68] and remains open.

By [BCW82], \(DC_n \Longrightarrow JC_n\) (the Jacobian conjecture in dimension n) over a fixed field K. By [AvdE07], Theorem 7, the chain

\[JC_{2n} \Longrightarrow PC_n \Longrightarrow DC_n \Longrightarrow JC_n\]

holds when each conjecture is quantified over all fields of characteristic zero ([AvdE07], Notations 5 and 7). Since the Jacobian conjecture fails in every dimension \(n ≥ 3\) [Alp26], the contrapositive of [BCW82] gives that \(DC_n\) is false for all \(n ≥ 3\). \(DC_1\) and \(DC_2\) remain open. The chain only propagates falsity upwards, so the failure of \(PC_2\) [Lon26] does not settle \(DC_2\).

The Weyl algebra \(A_n(K)\) is WeylAlgebra K (Fin n), with the \(2n\) generators indexed by Fin n ⊕ Fin n as in FormalConjecturesForMathlib/Algebra/WeylAlgebra.lean; the Poisson side of the chain is stated in PoissonConjecture.lean in this directory.

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

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

Arxiv.«math.0608009».dixmier_conjecture

Solved: stated here without proof.

The Dixmier Conjecture (generalised to all dimensions; Problem 1 of [Dix68] for \(n = 1\)): for every n, every endomorphism of the n-th Weyl algebra over a field of characteristic zero is an automorphism. This is false: the Jacobian conjecture fails in dimension \(3\) [Alp26], and \(DC_n \Longrightarrow JC_n\) [BCW82], so \(DC_3\) fails.

theorem dixmier_conjecture : ¬ ∀ n, DixmierConjectureFor K n

Category research solved; AMS 16 Associative rings and algebras. Declared in FormalConjectures/Arxiv/math.0608009/DixmierConjecture.lean, line 89.

Arxiv.«math.0608009».dixmier_conjecture.variants.dimension_one

Open: stated without proof.

The Dixmier Conjecture in dimension \(1\) — Problem 1 of [Dix68] — is open. By [AvdE07], Theorem 7, it is implied by \(PC_1\), and hence by \(JC_2\) (Keller's problem).

theorem dixmier_conjecture.variants.dimension_one : DixmierConjectureFor K 1

Category research open; AMS 16 Associative rings and algebras. Declared in FormalConjectures/Arxiv/math.0608009/DixmierConjecture.lean, line 97.

Arxiv.«math.0608009».dixmier_conjecture.variants.dimension_two

Open: stated without proof.

The Dixmier Conjecture in dimension \(2\) (\(DC_2\)) is open. It implies Keller's two-variable Jacobian conjecture \(JC_2\) [BCW82]. It is implied by \(JC_4\) ([AvdE07], Theorem 7), but \(JC_4\) and \(PC_2\) are false ([Alp26], [Lon26]).

theorem dixmier_conjecture.variants.dimension_two : DixmierConjectureFor K 2

Category research open; AMS 16 Associative rings and algebras. Declared in FormalConjectures/Arxiv/math.0608009/DixmierConjecture.lean, line 106.

Arxiv.«math.0608009».dixmier_conjecture.variants.dimension_three

Solved: stated here without proof.

The Dixmier Conjecture is false in dimension \(3\): \(DC_3\) implies the Jacobian conjecture in dimension \(3\) [BCW82], which fails by the counterexample of [Alp26].

theorem dixmier_conjecture.variants.dimension_three : ¬ DixmierConjectureFor K 3

Category research solved; AMS 16 Associative rings and algebras. Declared in FormalConjectures/Arxiv/math.0608009/DixmierConjecture.lean, line 114.

Arxiv.«math.0608009».dixmier_conjecture.variants.dimension_ge_three

Solved: stated here without proof.

The Dixmier Conjecture is false in every dimension \(n ≥ 3\), since the Jacobian conjecture is false in every dimension \(n ≥ 3\) (padding the counterexample of [Alp26] with identity coordinates) and \(DC_n \Longrightarrow JC_n\) [BCW82].

theorem dixmier_conjecture.variants.dimension_ge_three (n : ℕ) (hn : 3 ≤ n) :
    ¬ DixmierConjectureFor K n

Category research solved; AMS 16 Associative rings and algebras. Declared in FormalConjectures/Arxiv/math.0608009/DixmierConjecture.lean, line 123.

Arxiv.«math.0608009».dixmier_conjecture.variants.jacobian_implication

Solved: stated here without proof.

The Dixmier conjecture in dimension n implies the Jacobian conjecture in dimension n ([BCW82]; see also [AvdE07], Theorem 7).

theorem dixmier_conjecture.variants.jacobian_implication (n : ℕ)
    (h : DixmierConjectureFor K n) : JacobianConjectureProp K (Fin n)

Category research solved; AMS 14 Algebraic geometry, 16 Associative rings and algebras. Declared in FormalConjectures/Arxiv/math.0608009/DixmierConjecture.lean, line 132.

Arxiv.«math.0608009».dixmier_conjecture.variants.poisson_implication

Solved: stated here without proof.

If the Poisson conjecture in dimension n holds over every field of characteristic zero, then so does the Dixmier conjecture in dimension n. This is \(CPC(n, 0) \Longrightarrow CDC(n, 0)\) in [AvdE07], Theorem 7, where both statements quantify over all fields of characteristic zero (Notations 5 and 7). The proof reduces to prime characteristic and uses the Azumaya property of Weyl algebras in characteristic p.

theorem dixmier_conjecture.variants.poisson_implication (n : ℕ)
    (h : ∀ (L : Type) [Field L] [CharZero L], PoissonConjectureFor L n)
    (L : Type) [Field L] [CharZero L] : DixmierConjectureFor L n

Category research solved; AMS 14 Algebraic geometry, 16 Associative rings and algebras, 17 Nonassociative rings and algebras. Declared in FormalConjectures/Arxiv/math.0608009/DixmierConjecture.lean, line 144.

Sources
LeanArxiv.«math.0608009».dixmier_conjecture · Arxiv.«math.0608009».dixmier_conjecture.variants.dimension_one · Arxiv.«math.0608009».dixmier_conjecture.variants.dimension_two · Arxiv.«math.0608009».dixmier_conjecture.variants.dimension_three · Arxiv.«math.0608009».dixmier_conjecture.variants.dimension_ge_three · Arxiv.«math.0608009».dixmier_conjecture.variants.jacobian_implication · Arxiv.«math.0608009».dixmier_conjecture.variants.poisson_implication

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.