The Auslander-Reiten conjecture to Gourevitch's series identity

TheoremThe Auslander-Reiten conjecture#

Auslander-Reiten conjecture. Let \(\Lambda\) be an Artin algebra and let \(M\) be a finitely generated \(\Lambda\)-module with \(\operatorname{Ext}^i_\Lambda(M, M) = 0\) and \(\operatorname{Ext}^i_\Lambda(M, \Lambda) = 0\) for all \(i > 0\). Then \(M\) is projective.

An Artin algebra is a ring \(\Lambda\) that is an algebra over a commutative Artinian ring \(A\) and is finitely generated as an \(A\)-module.

Auslander and Reiten [AR75] derived this from the generalized Nakayama conjecture. The conjecture for Artin algebras is false: an internal OpenAI model gave an explicit counterexample in September 2026 [OAI26], a finite-dimensional algebra over the field \(\mathbb{F}_2(q, H_1, H_2)\) with a finite-dimensional non-projective module satisfying both vanishing conditions. The commutative version, obtained by replacing \(\Lambda\) with a commutative Noetherian ring \(R\), is open and is what the commutative algebra literature calls the Auslander-Reiten conjecture. The two hypotheses are together equivalent to \(\operatorname{Ext}^i_R(M, R \oplus M) = 0\) for all \(i > 0\).

Known cases of the commutative version include: \(R\) a locally excellent Cohen-Macaulay normal ring containing \(\mathbb Q\) [HL04]; \(R\) a Gorenstein normal ring [Ar09]; \(R\) a Cohen-Macaulay normal ring [KOT22]; and, most generally, \(R\) any normal ring [Ki23]. Auslander, Ding and Solberg [ADS93] proved it for local complete intersections. The commutative version is open in general, already for commutative Noetherian local rings.

References: - [AR75] M. Auslander, I. Reiten, On a generalized version of the Nakayama conjecture, Proc. Amer. Math. Soc. 52 (1975), 69-74. PDF - Wikipedia, Nakayama conjecture, on the generalized Nakayama conjecture of [AR75]. - [ADS93] M. Auslander, S. Ding, Ø. Solberg, Liftings and weak liftings of modules, J. Algebra 156 (1993), 273-317. - [HL04] C. Huneke, G. J. Leuschke, On a conjecture of Auslander and Reiten, J. Algebra 275 (2004), no. 2, 781-790. arXiv:math/0305001 - [Ar09] T. Araya, The Auslander-Reiten conjecture for Gorenstein rings, Proc. Amer. Math. Soc. 137 (2009), 1941-1944. - [KOT22] K. Kimura, Y. Otake, R. Takahashi, Maximal Cohen-Macaulay tensor products and vanishing of Ext modules, Bull. Lond. Math. Soc. 54 (2022), no. 6, 2456-2468. - [Ki23] K. Kimura, Auslander-Reiten conjecture for normal rings, arXiv:2304.03956. The statements of the conjecture formalised below follow this paper. - [OAI26] OpenAI, An explicit counterexample to the Auslander-Reiten conjecture. OpenAI Math Release preprint (2026). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/An-explicit-counterexample-to-the-Auslander-Reiten-conjecture-September-23-2026/paper.pdf

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

AuslanderReiten.auslander_reiten

Solved: stated here; a Lean proof is at https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Algebra/AuslanderReiten/All.lean#L738.

The Auslander-Reiten conjecture [AR75] is false. The conjecture states: let \(\Lambda\) be an Artin algebra and \(M\) a finitely generated \(\Lambda\)-module with \(\operatorname{Ext}^i_\Lambda(M, \Lambda) = 0\) and \(\operatorname{Ext}^i_\Lambda(M, M) = 0\) for all \(i > 0\). Then \(M\) is projective.

That \(\Lambda\) is an Artin algebra is the hypothesis that it is an algebra over some commutative Artinian ring A and is finitely generated as an A-module.

This was disproved by an internal OpenAI model in September 2026 [OAI26]; see the linked Lean proof. The counterexample is a finite-dimensional algebra over the field \(\mathbb{F}_2(q, H_1, H_2)\), which is the ring A there.

theorem auslander_reiten :
    ¬ ∀ (Λ : Type) [Ring Λ] (M : Type) [AddCommGroup M] [Module Λ M] [Module.Finite Λ M]
      (A : Type) [CommRing A] [IsArtinianRing A] [Algebra A Λ] [Module.Finite A Λ],
      (∀ i > 0, Subsingleton (Abelian.Ext (ModuleCat.of Λ M) (ModuleCat.of Λ Λ) i)) →
      (∀ i > 0, Subsingleton (Abelian.Ext (ModuleCat.of Λ M) (ModuleCat.of Λ M) i)) →
      Module.Projective Λ M

Category research solved; AMS 13 Commutative algebra, 16 Associative rings and algebras, 18 Category theory; homological algebra. Declared in FormalConjectures/Paper/AuslanderReiten.lean, line 109.

AuslanderReiten.auslander_reiten.variants.commutative

Open: stated without proof.

The Auslander-Reiten conjecture for commutative Noetherian rings [Ki23]. If \(R\) is a commutative Noetherian ring and \(M\) is a finitely generated \(R\)-module with \(\operatorname{Ext}^i_R(M, R \oplus M) = 0\) for all \(i > 0\), then \(M\) is projective.

theorem auslander_reiten.variants.commutative
    (hMR : ∀ i > 0, Subsingleton (Abelian.Ext (ModuleCat.of R M) (ModuleCat.of R R) i))
    (hMM : ∀ i > 0, Subsingleton (Abelian.Ext (ModuleCat.of R M) (ModuleCat.of R M) i)) :
    Module.Projective R M

Category research open; AMS 13 Commutative algebra, 18 Category theory; homological algebra. Declared in FormalConjectures/Paper/AuslanderReiten.lean, line 130.

AuslanderReiten.auslander_reiten.variants.local_free

Open: stated without proof.

Over a Noetherian local ring a finitely generated projective module is free, so the conjecture takes the following form there. It is open in this case too.

theorem auslander_reiten.variants.local_free [IsLocalRing R]
    (hMR : ∀ i > 0, Subsingleton (Abelian.Ext (ModuleCat.of R M) (ModuleCat.of R R) i))
    (hMM : ∀ i > 0, Subsingleton (Abelian.Ext (ModuleCat.of R M) (ModuleCat.of R M) i)) :
    Module.Free R M

Category research open; AMS 13 Commutative algebra, 18 Category theory; homological algebra. Declared in FormalConjectures/Paper/AuslanderReiten.lean, line 141.

AuslanderReiten.auslander_reiten.variants.normal

Solved: stated here without proof.

The conjecture holds for normal rings [Ki23, Corollary 1.2]. Stated here for normal domains, since Mathlib does not currently have a standalone class for normal rings, which are the rings whose localizations at all primes are normal domains.

theorem auslander_reiten.variants.normal [IsDomain R] [IsIntegrallyClosed R]
    (hMR : ∀ i > 0, Subsingleton (Abelian.Ext (ModuleCat.of R M) (ModuleCat.of R R) i))
    (hMM : ∀ i > 0, Subsingleton (Abelian.Ext (ModuleCat.of R M) (ModuleCat.of R M) i)) :
    Module.Projective R M

Category research solved; AMS 13 Commutative algebra, 18 Category theory; homological algebra. Declared in FormalConjectures/Paper/AuslanderReiten.lean, line 153.

AuslanderReiten.auslander_reiten.variants.regular_local

Textbook result, stated without proof.

Over a regular local ring the conjecture is standard: every finitely generated module has finite projective dimension \(p\), and if \(p > 0\) then \(\operatorname{Ext}^p_R(M, R) \ne 0\). Only the vanishing of \(\operatorname{Ext}^i_R(M, R)\) is used, and the conclusion is freeness.

theorem auslander_reiten.variants.regular_local [IsRegularLocalRing R]
    (hMR : ∀ i > 0, Subsingleton (Abelian.Ext (ModuleCat.of R M) (ModuleCat.of R R) i)) :
    Module.Free R M

Category textbook; AMS 13 Commutative algebra, 18 Category theory; homological algebra. Declared in FormalConjectures/Paper/AuslanderReiten.lean, line 166.

Sources

• FormalConjectures/Paper/AuslanderReiten.lean at 2055e5ad
• PDF

LeanAuslanderReiten.auslander_reiten · AuslanderReiten.auslander_reiten.variants.commutative · AuslanderReiten.auslander_reiten.variants.local_free · AuslanderReiten.auslander_reiten.variants.normal · AuslanderReiten.auslander_reiten.variants.regular_local

TheoremThe Bollobás–Eldridge–Catlin conjecture on graph packing (1978)#

References: * [BE78] Bollobás, B. and Eldridge, S. E. (1978). "Packings of graphs and applications to computational complexity." J. Combin. Theory Ser. B 25, pp. 105--124. * [Ca74] Catlin, P. A. (1974). "Subgraphs of graphs, I." Discrete Math. 10, pp. 225--233. * [SS78] Sauer, N. and Spencer, J. (1978). "Edge disjoint placement of graphs." J. Combin. Theory Ser. B 25, pp. 295--302. * [AF93] Aigner, M. and Brandt, S. (1993). "Embedding arbitrary graphs of maximum degree two." J. London Math. Soc. 48, pp. 39--51. * [CSS03] Csaba, B., Shokoufandeh, A. and Szemerédi, E. (2003). "Proof of a conjecture of Bollobás and Eldridge for graphs of maximum degree three." Combinatorica 23, pp. 35--72.

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

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

BollobasEldridgeCatlinConjecture.bollobas_eldridge_catlin_conjecture

Open: stated without proof.

The Bollobás–Eldridge–Catlin conjecture (1978).

If \(G_1\) and \(G_2\) are graphs on the same \(n\) vertices with maximum degrees \(\Delta_1\), \(\Delta_2\) satisfying \((\Delta_1 + 1)(\Delta_2 + 1) \le n + 1\), then \(G_1\) and \(G_2\) pack.

theorem bollobas_eldridge_catlin_conjecture :
    ∀ {V : Type} [Fintype V] [DecidableEq V] (G₁ G₂ : SimpleGraph V)
      [DecidableRel G₁.Adj] [DecidableRel G₂.Adj],
      (G₁.maxDegree + 1) * (G₂.maxDegree + 1) ≤ Fintype.card V + 1 → Packs G₁ G₂

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

BollobasEldridgeCatlinConjecture.bollobas_eldridge_catlin_conjecture.variants.sauer_spencer

Solved: stated here without proof.

The Sauer–Spencer theorem (1978).

If \(2\Delta_1\Delta_2 < n\) then \(G_1\) and \(G_2\) pack.

Reference: [SS78].

theorem bollobas_eldridge_catlin_conjecture.variants.sauer_spencer
    {V : Type} [Fintype V] [DecidableEq V] (G₁ G₂ : SimpleGraph V)
    [DecidableRel G₁.Adj] [DecidableRel G₂.Adj]
    (h : 2 * G₁.maxDegree * G₂.maxDegree < Fintype.card V) : Packs G₁ G₂

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

BollobasEldridgeCatlinConjecture.bollobas_eldridge_catlin_conjecture.variants.maxDegree_le_two

Solved: stated here without proof.

Maximum degree two (Aigner–Brandt 1993).

The conjecture holds whenever one of the graphs has maximum degree at most \(2\).

Reference: [AF93].

theorem bollobas_eldridge_catlin_conjecture.variants.maxDegree_le_two
    {V : Type} [Fintype V] [DecidableEq V] (G₁ G₂ : SimpleGraph V)
    [DecidableRel G₁.Adj] [DecidableRel G₂.Adj] (hΔ : G₁.maxDegree ≤ 2)
    (h : (G₁.maxDegree + 1) * (G₂.maxDegree + 1) ≤ Fintype.card V + 1) : Packs G₁ G₂

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

BollobasEldridgeCatlinConjecture.bollobas_eldridge_catlin_conjecture.variants.maxDegree_three_large_n

Solved: stated here without proof.

Maximum degree three, for large \(n\) (Csaba–Shokoufandeh–Szemerédi 2003).

There is an \(n_0\) such that the conjecture holds for all graphs on \(n \ge n_0\) vertices when one of them has maximum degree at most \(3\).

Reference: [CSS03].

theorem bollobas_eldridge_catlin_conjecture.variants.maxDegree_three_large_n :
    ∃ n₀ : ℕ, ∀ {V : Type} [Fintype V] [DecidableEq V] (G₁ G₂ : SimpleGraph V)
      [DecidableRel G₁.Adj] [DecidableRel G₂.Adj], n₀ ≤ Fintype.card V → G₁.maxDegree ≤ 3 →
      (G₁.maxDegree + 1) * (G₂.maxDegree + 1) ≤ Fintype.card V + 1 → Packs G₁ G₂

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

BollobasEldridgeCatlinConjecture.bollobas_eldridge_catlin_conjecture.variants.edgeless

Proved here.

The case where one graph has no edges.

If \(\Delta_2 = 0\) then \(G_2\) is edgeless and the conjecture holds trivially.

theorem bollobas_eldridge_catlin_conjecture.variants.edgeless
    {V : Type} [Fintype V] [DecidableEq V] (G₁ G₂ : SimpleGraph V)
    [DecidableRel G₁.Adj] [DecidableRel G₂.Adj] (h : G₂.maxDegree = 0) : Packs G₁ G₂

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

Sources

• FormalConjectures/Paper/BollobasEldridgeCatlinConjecture.lean at 2055e5ad

LeanBollobasEldridgeCatlinConjecture.bollobas_eldridge_catlin_conjecture · BollobasEldridgeCatlinConjecture.bollobas_eldridge_catlin_conjecture.variants.sauer_spencer · BollobasEldridgeCatlinConjecture.bollobas_eldridge_catlin_conjecture.variants.maxDegree_le_two · BollobasEldridgeCatlinConjecture.bollobas_eldridge_catlin_conjecture.variants.maxDegree_three_large_n · BollobasEldridgeCatlinConjecture.bollobas_eldridge_catlin_conjecture.variants.edgeless

TheoremDecidability of reachability for branching vector addition systems#

A branching vector addition system (BVAS) of dimension d is given by a finite list of axioms, a finite list of unary rules, and a finite list of binary rules, each of which is a vector in ℤ^d. A configuration is a vector in ℕ^d, which here is represented as a vector v ∈ ℤ^d subject to 0 ≤ v. The set of reachable configurations is defined inductively:

• every axiom that is a valid configuration (i.e. lies in ℕ^d) is reachable;
• if v is a reachable configuration, r is a unary rule and v + r ∈ ℕ^d, then v + r is reachable;
• if v₁, v₂ are both reachable configurations, r is a binary rule and v₁ + v₂ + r ∈ ℕ^d, then v₁ + v₂ + r is reachable.

Modelling axioms as vectors in ℤ^d and only counting the non-negative ones as reachable yields the same set of reachable configurations as the usual definition in which axioms are required to lie in ℕ^d.

Branching vector addition systems are distinguished from ordinary vector addition systems (VAS) by allowing binary rules. VAS reachability is known to be decidable.

References: - The covering and boundedness problems for branching vector addition systems (Stéphane Demri, Marcin Jurdziński, Oded Lachish, Ranko Lazić, FSTTCS 2009) Gives a similar definition of BVAS, and compares it to related equivalent definitions. - On the Reachability Problem for Two-Dimensional Branching VASS by Clotilde Bizière, Thibault Hilaire, Jérôme Leroux, Grégoire Sutre, MFCS 2025, which settles the two-dimensional case and states that "the decidability status of the reachability problem for BVASS remains open in higher dimensions". - The General Vector Addition System Reachability Problem by Presburger Inductive Invariants by Jérôme Leroux (2010), for the decidability of reachability for ordinary VAS. - Solving the Reachability Problem for Branching Vector Addition Systems via Semilinear Inductive Invariants by Clotilde Bizière, Jérôme Leroux, Grégoire Sutre (2026), a recent preprint claiming a positive resolution to the conjecture: reachability for branching vector addition systems is decidable.

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

BranchingVAS.reachability_decidable

Solved: stated here without proof.

The reachability problem for branching vector addition systems is decidable.

That is, the predicate taking a dimension d, a branching vector addition system b of dimension d and a target vector t ∈ ℤ^d, and returning whether t is reachable in b, is a computable predicate. Note that the dimension is part of the input: a single algorithm must work for all dimensions.

As of August 2026, the solution is quite recently announced and is not yet peer-reviewed.

theorem reachability_decidable :
    ComputablePred fun p : Σ d : ℕ, Bvas d × (Fin d → ℤ) => p.2.1.Reachable p.2.2

Category research solved; AMS 03 Mathematical logic and foundations, 68 Computer science. Declared in FormalConjectures/Paper/BranchingVAS.lean, line 143.

Sources

• FormalConjectures/Paper/BranchingVAS.lean at 2055e5ad
• The covering and boundedness problems for branching vector addition systems

LeanBranchingVAS.reachability_decidable

TheoremThe burning number conjecture#

References: * [BJR16] Bonato, A., Janssen, J., and Roshanbin, E. (2016). "How to burn a graph." Internet Math. 12, pp. 85--100. arXiv:1507.06524 * [NT24] Norin, S. and Turcotte, J. (2024). "The burning number conjecture holds asymptotically." J. Combin. Theory Ser. B 168, pp. 208--235. arXiv:2207.04035

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

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

BurningNumberConjecture.burning_number_conjecture

Open: stated without proof.

The burning number conjecture (Bonato–Janssen–Roshanbin [BJR16]).

Every connected graph on n vertices can be burned in at most ⌈√n⌉ rounds: fires started at one new vertex per round, each spreading to all neighbouring vertices every round, can burn the whole graph in ⌈√n⌉ rounds.

theorem burning_number_conjecture {V : Type} [Fintype V] (G : SimpleGraph V)
    (hc : G.Connected) :
    burningNumber G ≤ ⌈Real.sqrt (Fintype.card V)⌉₊

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

BurningNumberConjecture.burning_number_conjecture.variants.path

Solved: stated here without proof.

Paths attain the conjectured bound (Bonato–Janssen–Roshanbin [BJR16]).

The burning number of the path on n ≥ 1 vertices is exactly ⌈√n⌉, so the bound in the burning number conjecture cannot be improved.

theorem burning_number_conjecture.variants.path (n : ℕ) (hn : 1 ≤ n) :
    burningNumber (SimpleGraph.pathGraph n) = ⌈Real.sqrt n⌉₊

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

BurningNumberConjecture.burning_number_conjecture.variants.norin_turcotte

Solved: stated here without proof.

Norin–Turcotte (2024): the burning number conjecture holds asymptotically.

For every ε > 0, every sufficiently large connected graph on n vertices can be burned in at most (1 + ε) √n rounds.

Reference: [NT24].

theorem burning_number_conjecture.variants.norin_turcotte (ε : ℝ) (hε : 0 < ε) :
    ∃ n₀ : ℕ, ∀ (V : Type) [Fintype V] (G : SimpleGraph V), G.Connected →
      n₀ ≤ Fintype.card V →
        (burningNumber G : ℝ) ≤ (1 + ε) * Real.sqrt (Fintype.card V)

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

Sources

• FormalConjectures/Paper/BurningNumberConjecture.lean at 2055e5ad
• arXiv:1507.06524

LeanBurningNumberConjecture.burning_number_conjecture · BurningNumberConjecture.burning_number_conjecture.variants.path · BurningNumberConjecture.burning_number_conjecture.variants.norin_turcotte

TheoremConjecture about cardinality of Lindelöf spaces#

The conjecture asks for a Lindelöf Tychonoff space where all singletons are G_δ sets and which has cardinality > 𝔠.

This is Problem 1 in https://www.math.md/files/basm/y2013-n2-3/y2013-n2-3-(pp37-46).pdf.pdf

Reference: * Selected Old Open Problems in General Topology by A. V. Arhangel’skii

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

CardinalityLindelof.HasGδSingletons.lindelof_card

Open: stated without proof.

Is there a Lindelöf Tychonoff space with singletons as Gδ sets with cardinality greater than the continuum?

Note: the cited paper uses a blanket convention that all spaces are Tychonoff.

theorem HasGδSingletons.lindelof_card :
    ∃ (X : Type) (_ : TopologicalSpace X),
      T35Space X ∧ HasGδSingletons X ∧ LindelofSpace X ∧ 𝔠 < #X

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

Sources

• FormalConjectures/Paper/CardinalityLindelof.lean at 2055e5ad
• Selected Old Open Problems in General Topology

LeanCardinalityLindelof.HasGδSingletons.lindelof_card

TheoremCasas-Alvero Conjecture#

References: * The Casas-Alvero conjecture for infinitely many degrees * MathOverflow

The Casas-Alvero conjecture states that if a univariate polynomial P of degree d over a field of characteristic zero shares a non-trivial factor with its Hasse derivatives up to order d-1, then P must be of the form (X - α)ᵈ for some α in the field.

The conjecture has been proven for: * Degrees d ≤ 8 * Degrees of the form p^k where p is prime * Degrees of the form 2p^k where p is prime

The conjecture is false in positive characteristic p for polynomials of degree p+1.

The conjecture is now claimed to be proven in this paper: * Proof of the Casas-Alvero conjecture: Soham Ghosh)

Quoted from FormalConjectures/Paper/CasasAlvero.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: 1 open and 3 solved. It also has 4 API statements, counted here but not shown.

CasasAlvero.casas_alvero_conjecture

Open: stated without proof.

The Casas-Alvero conjecture states that in characteristic zero, if a monic polynomial P has the Casas-Alvero property, then P = (X - α)ᵈ for some α.

theorem casas_alvero_conjecture (hP' : HasCasasAlveroProp P) :
    ∃ α : K, P = (X - C α) ^ P.natDegree

Category research open; AMS 12 Field theory and polynomials. Declared in FormalConjectures/Paper/CasasAlvero.lean, line 124.

CasasAlvero.casas_alvero.prime_power

Solved: stated here without proof.

The Casas-Alvero conjecture holds for polynomials of prime power degree. This was proved by Graf von Bothmer, Labs, Schicho, and van de Woestijne.

Reference: The Casas-Alvero conjecture for infinitely many degrees

theorem casas_alvero.prime_power (p k : ℕ) (hp : p.Prime) (hd : P.natDegree = p^k)
    (hP' : HasCasasAlveroProp P) : ∃ α : K, P = (X - C α) ^ P.natDegree

Category research solved; AMS 12 Field theory and polynomials. Declared in FormalConjectures/Paper/CasasAlvero.lean, line 135.

CasasAlvero.casas_alvero.double_prime_power

Solved: stated here without proof.

The Casas-Alvero conjecture holds for polynomials of degree 2p^k where p is prime. This was proved by Graf von Bothmer, Labs, Schicho, and van de Woestijne.

Reference: The Casas-Alvero conjecture for infinitely many degrees

theorem casas_alvero.double_prime_power (p k : ℕ) (hp : p.Prime) (hd : P.natDegree = 2 * p^k)
    (hP' : HasCasasAlveroProp P) : ∃ α : K, P = (X - C α) ^ P.natDegree

Category research solved; AMS 12 Field theory and polynomials. Declared in FormalConjectures/Paper/CasasAlvero.lean, line 146.

CasasAlvero.casas_alvero.positive_char_counterexample

Solved: stated here; a Lean proof is at https://github.com/mzhorvath1/formal-conjectures/blob/4f2343508f2c157f35abb7be4814bd550280ce81/FormalConjectures/Paper/CasasAlvero.lean#163.

The Casas-Alvero conjecture fails in positive characteristic p for polynomials of degree p + 1. This was shown by Graf von Bothmer, Labs, Schicho, and van de Woestijne.

Reference: The Casas-Alvero conjecture for infinitely many degrees

Formal proof linked here provided by AlphaProof.

theorem casas_alvero.positive_char_counterexample {p : ℕ} (hp : p.Prime) :
    ∃ (K : Type*) (_ : Field K) (_ : CharP K p),
      let P := X ^ (p + 1) - X ^ p
      Monic P ∧ HasCasasAlveroProp P ∧
      ¬∃ α : K, P = (X - C α) ^ P.natDegree

Category research solved; AMS 12 Field theory and polynomials. Declared in FormalConjectures/Paper/CasasAlvero.lean, line 162.

Sources

• FormalConjectures/Paper/CasasAlvero.lean at 2055e5ad
• The Casas-Alvero conjecture for infinitely many degrees

LeanCasasAlvero.casas_alvero_conjecture · CasasAlvero.casas_alvero.prime_power · CasasAlvero.casas_alvero.double_prime_power · CasasAlvero.casas_alvero.positive_char_counterexample

TheoremThe Catch-Up game and conjecture#

The game Catch-Up (Isaksen–Ismail–Brams–Nealen, 2015) is a two-player, perfect-information game played on a finite nonempty set S of positive integers. Each time a player removes a number from S, that number is added to the player’s score.

Rules. * The scores start at 0. Player p1 starts by removing exactly one number from S. * After the first move, players alternate turns. On a turn, the current player removes one or more numbers from S, one at a time, and must keep removing numbers until their score becomes at least the opponent’s score; before the final pick they must remain strictly behind. * If the current player cannot catch up (in particular, even taking all remaining numbers would still leave them behind), the game ends immediately: the current player receives all remaining numbers.

When S is empty, the player with higher score wins; equal scores give a draw.

In this file we define: * Player and Outcome, * the recursive evaluator value (optimal play), * the conjecture value_of_even_mul_succ_self_div_two.

Example

For S = {1,2,3,4} one play is: p1 takes 2, p2 takes 1 then 4, and p1 takes 3, ending with scores (5,5).

References

A. Isaksen, M. Ismail, S. J. Brams, A. Nealen, Catch-Up: A Game in Which the Lead Alternates, Game & Puzzle Design 1(2), 38–49 (2015).

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

CatchUp.value_of_even_mul_succ_self_div_two

Open: stated without proof.

Let \(T_N = \sum_{k=1}^{N} k = \frac{N(N+1)}{2}\). If \(T_N\) is even (equivalently \(N \equiv 0 \pmod 4\) or \(N \equiv 3 \pmod 4\)), then under optimal play the game Catch-Up($\{1, \ldots, N\}$) ends in a draw.

theorem value_of_even_mul_succ_self_div_two
    (N : ℕ) (h_even : Even (N * (N + 1) / 2)) :
    value (.Icc 1 N) = .draw

Category research open; AMS 11 Number theory, 91 Game theory, economics, social and behavioral sciences. Declared in FormalConjectures/Paper/CatchUpConjecture.lean, line 182.

Sources

• FormalConjectures/Paper/CatchUpConjecture.lean at 2055e5ad

LeanCatchUp.value_of_even_mul_succ_self_div_two

TheoremChvátal's Conjecture#

References:

• A Conjecture in Extremal Combinatorics
• Chvátal's Conjecture and Correlation Inequalities
• A proof of Chvátal's conjecture via a sharp correlation inequality

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

Chvatal.exists_maximal_star

Solved: stated here; a Lean proof is at https://github.com/boonsuan/chvatal/blob/c19ed3aaac9e42d446f963a862d39d8a09eddbf9/Solution.lean#L22-L33.

If F is a decreasing family of sets of some finite type α, then there is some element x of α such that the family consisting of all members of F containing x is an intersecting subfamily of F with maximal cardinality.

theorem exists_maximal_star :
    ∀ F : Finset (Finset α), Decreasing F →
        ∃ x : α, ∀ G, G ⊆ F → Intersecting G → G.card ≤ { A ∈ F | x ∈ A }.card

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

Sources

• FormalConjectures/Paper/Chvatal.lean at 2055e5ad
• A Conjecture in Extremal Combinatorics

LeanChvatal.exists_maximal_star

TheoremClaude's Cycles#

Reference: Claude's Cycles by Donald E. Knuth (2026)

Fix m ≥ 2. Consider the directed graph with vertex set (ZMod m)³, where from each vertex (i, j, k) there are directed arcs to (i+1, j, k), (i, j+1, k), and (i, j, k+1) (arithmetic mod m). The goal is to partition all 3m³ directed arcs into three edge-disjoint directed Hamiltonian cycles (each of length m³).

Knuth describes an explicit construction, found by Claude (Anthropic), that achieves this decomposition for all odd m ≥ 3. The case m = 2 is known to be impossible [Aub82]. The even case m > 2 is also settled. Knuth's paper says so in its final section, added in the 14 April 2026 revision: "Breaking news: The problem for even values of m is no longer in doubt!" Ho Boon Suan's algorithm [Ho26] is proved correct for even m ≥ 8 in [GPT26], and Aquino-Michaels [AM26] gives a decomposition for the even case that is simpler. The statement below starts at m = 4, which is below the range [GPT26] covers, so it also rests on the explicit solutions in [Kn26], whose header gives even m ≥ 4.

References

• [Knu26] D. E. Knuth, "Claude's Cycles" (2026).
• [Aub82] J. Aubert, B. Schneider, "Graphes orientés indécomposables en circuits hamiltoniens", J. Combin. Theory Ser. B 32 (1982), 347–349.
• [Ho26] Ho Boon Suan, closed-form construction for even m, https://cs.stanford.edu/~knuth/even_closed_form.c
• [GPT26] A proof that [Ho26] yields three m³-cycles for every even m ≥ 8, 14 pages, https://cs.stanford.edu/~knuth/even_closed_form_proof_final.pdf
• [AM26] K. Aquino-Michaels, "Completing Claude's cycles: Multi-agent structured exploration on an open combinatorial problem", https://github.com/no-way-labs/residue
• [Kn26] Explicit even solutions for even m ≥ 4, recorded with [Knu26], https://cs.stanford.edu/~knuth/even_solution.py
• [KM26] K. Morrison, a Lean formalisation of the odd case, https://github.com/kim-em/KnuthClaudeLean

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

ClaudesCycles.cube_hamiltonian_arc_decomposition

Solved: stated here; a Lean proof is at https://github.com/kim-em/KnuthClaudeLean/blob/bdda6025fb7954f614ed9a7ac7382455fd064940/Solution.lean#L5.

For odd m > 1, the cube digraph on (ZMod m)³ has a Hamiltonian arc decomposition into three directed cycles [Knu26].

theorem cube_hamiltonian_arc_decomposition {m : ℕ} [NeZero m] (hm : Odd m) (hm' : 1 < m) :
    HasHamiltonianArcDecomposition m

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

ClaudesCycles.cube_hamiltonian_arc_decomposition_impossible_m2

Solved: stated here without proof.

The case m = 2 is impossible: the cube digraph on (ZMod 2)³ does not have a Hamiltonian arc decomposition [Aub82].

theorem cube_hamiltonian_arc_decomposition_impossible_m2 :
    ¬ HasHamiltonianArcDecomposition 2

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

ClaudesCycles.cube_hamiltonian_arc_decomposition_even

Solved: stated here without proof.

For even m > 2, the cube digraph on (ZMod m)³ has a Hamiltonian arc decomposition. Knuth records this as settled in the final section of [Knu26], by [Ho26] with the proof in [GPT26] for even m ≥ 8, and by [AM26] for the even case generally.

theorem cube_hamiltonian_arc_decomposition_even :
    ∀ᵉ (m : ℕ) (_ : NeZero m) (_ : Even m) (_ : 2 < m),
      HasHamiltonianArcDecomposition m

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

Sources

• FormalConjectures/Paper/ClaudesCycles.lean at 2055e5ad
• Claude's Cycles

LeanClaudesCycles.cube_hamiltonian_arc_decomposition · ClaudesCycles.cube_hamiltonian_arc_decomposition_impossible_m2 · ClaudesCycles.cube_hamiltonian_arc_decomposition_even

TheoremThe \(S_3\)-conjecture (conjugacy classes of distinct sizes)#

References: * W. Zhou, I. Gorshkov, On \(\{2,3,5\}\)-groups with conjugacy classes of distinct sizes, arXiv:2606.22244 (2026). * F. M. Markel, Groups with many conjugate elements, J. Algebra 26 (1973), 69–74. (Origin of the \(S_3\)-conjecture.) * R. Knörr, W. Lempken, B. Thielcke, The \(S_3\)-conjecture for solvable groups, Israel J. Math. 91 (1995), 61–76. * J. Zhang, Finite groups with many conjugate elements, J. Algebra 170 (1994), 608–624. * Z. Arad, M. Muzychuk, A. Oliver, On groups with conjugacy classes of distinct sizes, J. Algebra 280 (2004), 537–576. * Conjugacy class

A finite group in which distinct conjugacy classes have distinct cardinalities is called an anti-homogeneous group (or ah-group). The symmetric group \(S_3\) is an ah-group: its three conjugacy classes have sizes \(1\), \(2\), and \(3\). Markel's \(S_3\)-conjecture (1973) asserts that, up to isomorphism, \(S_3\) is the only nontrivial finite ah-group. The conjecture has been proved for all solvable groups (independently by Zhang and by Knörr–Lempken–Thielcke), but the general non-solvable case remains open.

Quoted from FormalConjectures/Paper/ConjugacyClassSizes.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 test statements and 1 API statement, counted here but not shown.

ConjugacyClassSizes.conjClassSizes_iff_sym_three

Open: stated without proof.

Markel's \(S_3\)-conjecture (1973): any nontrivial finite ah-group is isomorphic to \(S_3\).

The conjecture is open in general; it is known to be true for solvable groups.

theorem conjClassSizes_iff_sym_three
    (G : Type) [Group G] [Fintype G] [Nontrivial G]
    (h : HasDistinctConjClassSizes (G := G)) :
    Nonempty (G ≃* Equiv.Perm (Fin 3))

Category research open; AMS 20 Group theory and generalizations. Declared in FormalConjectures/Paper/ConjugacyClassSizes.lean, line 135.

ConjugacyClassSizes.conjClassSizes_iff_sym_three_solvable

Solved: stated here without proof.

The \(S_3\)-conjecture holds for solvable groups: every nontrivial solvable finite ah-group is isomorphic to \(S_3\). This was proved independently by Zhang (1994) and by Knörr–Lempken–Thielcke (1995).

theorem conjClassSizes_iff_sym_three_solvable
    (G : Type) [Group G] [Fintype G] [Group.IsSolvable G] [Nontrivial G]
    (h : HasDistinctConjClassSizes (G := G)) :
    Nonempty (G ≃* Equiv.Perm (Fin 3))

Category research solved; AMS 20 Group theory and generalizations. Declared in FormalConjectures/Paper/ConjugacyClassSizes.lean, line 147.

Sources

• FormalConjectures/Paper/ConjugacyClassSizes.lean at 2055e5ad
• arXiv:2606.22244

LeanConjugacyClassSizes.conjClassSizes_iff_sym_three · ConjugacyClassSizes.conjClassSizes_iff_sym_three_solvable

TheoremThe Courtade–Kumar (most informative Boolean function) conjecture#

Let \(X\) be uniform on the Boolean cube \(\{0,1\}^n\). Independently of \(X\), let the coordinates of \(Z\) be i.i.d. Bernoulli random variables with parameter \(p \in [0, 1]\), and put \(Y = X \oplus Z\), so that \(Y\) is the output of \(n\) independent binary symmetric channels with crossover probability \(p\) on input \(X\). The Courtade–Kumar conjecture asserts that for every Boolean function \(f : \{0,1\}^n \to \{0,1\}\),

\(I(f(X); Y) \le 1 - h(p)\),

where mutual information and binary entropy are measured in bits.

The usual restriction to \(p \in [0, 1/2]\) is equivalent to the range used here. For \(p > 1/2\), complementing every output bit replaces \(Z\) by its bitwise complement, which is i.i.d. Bernoulli(\(1 - p\)) noise still independent of \(X\); this bijective relabelling of the output preserves \(I(f(X); Y)\), and \(h(1 - p) = h(p)\).

This file contains two formulations:

• CourtadeKumar.courtade_kumar is the elementary finite-sum statement used by the external Lean proof and its comparator check. Its definitions and statement are retained unchanged.
• CourtadeKumar.variants.courtade_kumar_random_variable is the random-variable formulation. Its product-law hypothesis specifies a uniform input and independent i.i.d. Bernoulli channel noise, and its conclusion is about the mutual information of the actual random variables.

CourtadeKumar.courtade_kumar_iff_random_variable proves that the two formulations are equivalent, without using either research statement. Shannon entropy and mutual information of finite-valued random variables are defined in FormalConjecturesForMathlib.InformationTheory.FiniteEntropy.

For \(n \ge 1\), coordinate dictators attain the bound: \(I(X_i; Y) = I(X_i; Y_i) = 1 - h(p)\), since the other output coordinates are independent of \((X_i, Y_i)\). The test mutualInfo_dictator checks \(n = 1\).

References: - [CK14] T. A. Courtade and G. R. Kumar, Which Boolean functions maximize mutual information on noisy inputs?, IEEE Trans. Inf. Theory 60 (2014), no. 8, 4515–4525.

Independent work on the conjecture from September 2026, in alphabetical order: - [CGJLMNW26] Z. Chen, A. Gohari, A. Javanmard, H. Lin, V. Mirrokni, C. Nair, D. P. Woodruff, A Proof of the Most Informative Boolean Function Conjecture, arXiv:2609.24931. A Lean 4 formalisation of the proof is at https://github.com/dpwoodru/general-courtade-kumar-lean. - [KS26] D. Kramer and M. Saglam, On the most informative Boolean function under noise, manuscript, https://github.com/deepinfra/courtade-kumar. - [KT26] Vu Khac Ky and Tuan Tran, Dictators are most informative, arXiv:2609.24184. See also their follow-up Stability of the Courtade–Kumar inequality, arXiv:2609.31797. - [MB26] H. Mahdavifar and A. Beirami, The Most Informative Bit and Beyond: A Proof of the Courtade–Kumar Conjecture and Multibit Extensions, arXiv:2609.26444.

Quoted from FormalConjectures/Paper/CourtadeKumar.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 2 test statements and 4 API statements, counted here but not shown.

CourtadeKumar.courtade_kumar

Solved: stated here; a Lean proof is at https://github.com/dpwoodru/general-courtade-kumar-lean/blob/c3599c05181ad357331b701edf8fd8ec75c88305/verification/comparator/CKChallenge/Solution.lean#L6.

The Courtade–Kumar conjecture. For every \(n\), every Boolean function \(f\) on \(\{0,1\}^n\) and every crossover probability \(p \in [0, 1]\), \(I(f(X); Y) \le 1 - h(p)\).

theorem courtade_kumar (n : ℕ) (f : Cube n → Bool) (p : ℝ) (hp₀ : 0 ≤ p) (hp₁ : p ≤ 1) :
    mutualInfo f p ≤ 1 - binEntropyBits p

Category research solved; AMS 94 Information and communication, circuits. Declared in FormalConjectures/Paper/CourtadeKumar.lean, line 119.

CourtadeKumar.variants.courtade_kumar_random_variable

Solved: stated here; a Lean proof is at https://github.com/dpwoodru/general-courtade-kumar-lean/blob/c3599c05181ad357331b701edf8fd8ec75c88305/verification/comparator/CKChallenge/Solution.lean#L6.

The Courtade–Kumar conjecture, in random-variable form.

The pushforward in the hypothesis is the joint distribution of \((X, Z)\). The uniform measure on Cube n is the law of \(n\) i.i.d. Bernoulli(\(1/2\)) bits. The product law makes the coordinates of \(Z\) i.i.d. Bernoulli(\(p\)) and makes the whole noise vector independent of \(X\). In bernoulliMeasure true false p, true has probability \(p\) and denotes a flip.

Conditional on \(X\), \(Y = X \oplus Z\) flips each input coordinate independently with probability \(p\): this is the memoryless binary symmetric channel with crossover probability \(p\) from \(X\) to \(Y\). Every Boolean function is allowed, including constants. All maps between these finite discrete types are measurable, so \(f \circ X\) and \(Y\) are measurable. The conclusion is \(I(f(X); Y) \le 1 - h(p)\) in bits, for the entire output vector \(Y\).

The linked proof proves the elementary statement CourtadeKumar.courtade_kumar, and CourtadeKumar.courtade_kumar_iff_random_variable transfers it to this formulation.

theorem courtade_kumar_random_variable :
    ∀ (n : ℕ) (f : Cube n → Bool) (p : ℝ) (hp₀ : 0 ≤ p) (hp₁ : p ≤ 1)
      (Ω : Type) [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ]
      (X Z : Ω → Cube n),
      Measurable X →
      Measurable Z →
      μ.map (fun ω => (X ω, Z ω)) =
        (PMF.uniformOfFintype (Cube n)).toMeasure.prod
          (Measure.pi fun _ : Fin n =>
            ProbabilityTheory.bernoulliMeasure true false
              (⟨p, hp₀, hp₁⟩ : unitInterval)) →
      let Y : Ω → Cube n := fun ω => cubeXor (X ω) (Z ω)
      InformationTheory.mutualInformationBits μ (f ∘ X) Y ≤ 1 - binEntropyBits p

Category research solved; AMS 94 Information and communication, circuits. Declared in FormalConjectures/Paper/CourtadeKumar.lean, line 164.

Sources

• FormalConjectures/Paper/CourtadeKumar.lean at 2055e5ad
• arXiv:2609.24931

LeanCourtadeKumar.courtade_kumar · CourtadeKumar.variants.courtade_kumar_random_variable

TheoremDe Giorgi's conjecture#

This file states a conjecture of De Giorgi about entire solutions to \(Δ u + u - u^3 = 0\). The conjecture is a rigidity theorem: in spatial dimension \(n ≤ 8\), the level sets of bounded solutions which satisfy \(∂₁u > 0\) everywhere are hyperplanes. It has been shown that the condition \(n ≤ 8\) is sharp.

The main theorems are: - DeGiorgi_le_eight: the conjecture holds in dimension \(n ≤ 8\). - DeGiorgi_ge_nine: the conclusion of the conjecture does not hold if \(n ≥ 9\).

The cases \(1 ≤ n ≤ 8\) are also listed individually to enable partial solutions. The cases \(1 ≤ n ≤ 3\) are solved, while \(4 ≤ n ≤ 8\) remains open.

Existing results

• The case \(n = 1\) trivially holds (\(u\) is injective since \(∂_1 u > 0\)).
• The case \(n = 2\) was proven by Ghoussoub and Gui.
• The case \(n = 3\) was proven by Ambrosio and Cabré.
• The case \(4 ≤ n ≤ 8\) was proven under an extra assumption by Savin.
• The counterexample for \(n ≥ 9\) was proven by Del Pino, Kowalczyk, and Wei.

References

• Ghoussoub, Gui, Mathematische Annalen 311 (1998) proves the conjecture for \(n = 2\).
• Ambrosio, Cabré, Journal of the American Mathematical Society 13 (2000) proves the conjecture for \(n = 3\).
• Savin, Annals of Mathematics 169 (2009) proves the case \(4 ≤ n ≤ 8\) under an additional assumption.
• Del Pino, Kowalczyk, Wei, Annals of Mathematics 174 (2011) shows that the condition \(n ≤ 8\) is sharp.

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

The file states 10 research or textbook statements: 6 open and 4 solved.

DeGiorgi.DeGiorgi_le_eight

Open: stated without proof.

De Giorgi's conjecture holds in dimension \(n ≤ 8\).

theorem DeGiorgi_le_eight (hn : n ≤ 8) : (DeGiorgi_conclusion n)

Category research open; AMS 35 Partial differential equations. Declared in FormalConjectures/Paper/DeGiorgi.lean, line 94.

DeGiorgi.DeGiorgi_ge_nine

Solved: stated here without proof.

In dimension \(n ≥ 9\), the conclusion of De Giorgi's conjecture does not hold.

theorem DeGiorgi_ge_nine (hn : n ≥ 9) : ¬(DeGiorgi_conclusion n)

Category research solved; AMS 35 Partial differential equations. Declared in FormalConjectures/Paper/DeGiorgi.lean, line 101.

DeGiorgi.DeGiorgi_one

Proved here.

De Giorgi's conjecture trivially holds in dimension \(n = 1\).

theorem DeGiorgi_one : (DeGiorgi_conclusion 1)

Category research solved; AMS 35 Partial differential equations. Declared in FormalConjectures/Paper/DeGiorgi.lean, line 108.

DeGiorgi.DeGiorgi_two

Solved: stated here without proof.

De Giorgi's conjecture holds in dimension \(n = 2\).

theorem DeGiorgi_two : (DeGiorgi_conclusion 2)

Category research solved; AMS 35 Partial differential equations. Declared in FormalConjectures/Paper/DeGiorgi.lean, line 128.

DeGiorgi.DeGiorgi_three

Solved: stated here without proof.

De Giorgi's conjecture holds in dimension \(n = 3\).

theorem DeGiorgi_three : (DeGiorgi_conclusion 3)

Category research solved; AMS 35 Partial differential equations. Declared in FormalConjectures/Paper/DeGiorgi.lean, line 135.

DeGiorgi.DeGiorgi_four

Open: stated without proof.

De Giorgi's conjecture holds in dimension \(n = 4\).

theorem DeGiorgi_four : (DeGiorgi_conclusion 4)

Category research open; AMS 35 Partial differential equations. Declared in FormalConjectures/Paper/DeGiorgi.lean, line 142.

DeGiorgi.DeGiorgi_five

Open: stated without proof.

De Giorgi's conjecture holds in dimension \(n = 5\).

theorem DeGiorgi_five : (DeGiorgi_conclusion 5)

Category research open; AMS 35 Partial differential equations. Declared in FormalConjectures/Paper/DeGiorgi.lean, line 149.

DeGiorgi.DeGiorgi_six

Open: stated without proof.

De Giorgi's conjecture holds in dimension \(n = 6\).

theorem DeGiorgi_six : (DeGiorgi_conclusion 6)

Category research open; AMS 35 Partial differential equations. Declared in FormalConjectures/Paper/DeGiorgi.lean, line 156.

DeGiorgi.DeGiorgi_seven

Open: stated without proof.

De Giorgi's conjecture holds in dimension \(n = 7\).

theorem DeGiorgi_seven : (DeGiorgi_conclusion 7)

Category research open; AMS 35 Partial differential equations. Declared in FormalConjectures/Paper/DeGiorgi.lean, line 163.

DeGiorgi.DeGiorgi_eight

Open: stated without proof.

De Giorgi's conjecture holds in dimension \(n = 8\).

theorem DeGiorgi_eight : (DeGiorgi_conclusion 8)

Category research open; AMS 35 Partial differential equations. Declared in FormalConjectures/Paper/DeGiorgi.lean, line 170.

Sources

• FormalConjectures/Paper/DeGiorgi.lean at 2055e5ad
• Ghoussoub, Gui

LeanDeGiorgi.DeGiorgi_le_eight · DeGiorgi.DeGiorgi_ge_nine · DeGiorgi.DeGiorgi_one · DeGiorgi.DeGiorgi_two · DeGiorgi.DeGiorgi_three · DeGiorgi.DeGiorgi_four · DeGiorgi.DeGiorgi_five · DeGiorgi.DeGiorgi_six · DeGiorgi.DeGiorgi_seven · DeGiorgi.DeGiorgi_eight

TheoremDegree sequences in triangle-free graphs#

Authors: P. Erdős, S. Fajtlowicz and W. Staton, Published in Discrete Mathematics 92 (1991) 85–88.

Quoted from FormalConjectures/Paper/DegreeSequencesTriangleFree.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. A definition with a category attribute is not counted among them. It also has 8 API statements, counted here but not shown.

SimpleGraph.theorem1

Solved: stated here without proof.

Theorem 1. If a triangle-free graph has f = 2, then it is bipartite, has minimum degree 1, and its degree sequence is compact.

theorem theorem1 (G : SimpleGraph α) (h_conn: G.Connected) [DecidableRel G.Adj]
    (h₁ : G.CliqueFree 3) (h₂ : degreeSequenceMultiplicity G = 2) :
    G.IsBipartite ∧ G.minDegree = 1 ∧ HasCompactdegreeSequence G

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

SimpleGraph.theorem2

Solved: stated here without proof.

Theorem 2. Every triangle-free graph is an induced subgraph of one with f = 3.

theorem theorem2 (G : SimpleGraph α) [DecidableRel G.Adj] (h_conn: G.Connected)
    (h : G.CliqueFree 3) :
    ∃ (β : Type*) (_ : Fintype β) (H : SimpleGraph β) (_ : DecidableRel H.Adj) (i : G ↪g H),
      H.CliqueFree 3 ∧ degreeSequenceMultiplicity H = 3

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

SimpleGraph.F

A definition (def), not a statement; its category attribute says research solved.

F n is the smallest number of vertices of a triangle-free graph with chromatic number n and f = 3.

noncomputable def F (n : ℕ) : ℕ

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

SimpleGraph.F_three

Solved: stated here; a Lean proof is at https://github.com/anatoliiohorodnyk/lean-fc-proofs/blob/fc4f1f1d43b54106b0f932518075fef57829d6fb/Proofs/T_SimpleGraph_F_three.lean#L569.

The smallest number of vertices of a triangle-free graph with chromatic number 3 and f=3 is 7.

theorem F_three : F 3 = 7

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

SimpleGraph.F_four_le

Solved: stated here; a Lean proof is at https://github.com/anatoliiohorodnyk/lean-fc-proofs/blob/fc4f1f1d43b54106b0f932518075fef57829d6fb/Proofs/T_SimpleGraph_F_four_le.lean#L469.

The smallest number of vertices of a triangle-free graph with chromatic number 4 and f=3 is at most 19.

theorem F_four_le : F 4 ≤ 19

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

SimpleGraph.F_four_le_fifteen

Solved: stated here; a Lean proof is at https://github.com/anatoliiohorodnyk/lean-fc-proofs/blob/fc4f1f1d43b54106b0f932518075fef57829d6fb/Proofs/T_SimpleGraph_F_four_le.lean#L464.

There is a triangle-free graph with chromatic number 4 and f=3 on 15 vertices: the Grötzsch graph with four more vertices, with degrees 2,2,2,3,3,3,4,4,4,5,5,5,6,6,6. This improves the bound 19 of Erdős, Fajtlowicz and Staton. An exhaustive computer search, not formalized, shows that 15 is optimal; see https://github.com/anatoliiohorodnyk/lean-fc-proofs/blob/fc4f1f1d43b54106b0f932518075fef57829d6fb/docs/EFS_F4.md.

theorem F_four_le_fifteen : F 4 ≤ 15

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

Sources

• FormalConjectures/Paper/DegreeSequencesTriangleFree.lean at 2055e5ad

LeanSimpleGraph.theorem1 · SimpleGraph.theorem2 · SimpleGraph.F · SimpleGraph.F_three · SimpleGraph.F_four_le · SimpleGraph.F_four_le_fifteen

TheoremComplete disjoint NP pairs#

References: * [Ra94] Razborov, A. A. (1994). "On provably disjoint NP-pairs." BRICS Report Series RS-94-36; ECCC TR94-006. * [KMT03] Köbler, J., Messner, J., and Torán, J. (2003). "Optimal proof systems imply complete sets for promise classes." Inform. and Comput. 184, pp. 71--92. * [GSSZ04] Glaßer, C., Selman, A. L., Sengupta, S., and Zhang, L. (2004). "Disjoint NP-pairs." SIAM J. Comput. 33, pp. 1369--1416. * [Pu17] Pudlák, P. (2017). "Incompleteness in the finite domain." Bull. Symbolic Logic 23, pp. 405--441. arXiv:1601.01487 * [Kh22] Khaniki, E. (2022). "New relations and separations of conjectures about incompleteness in the finite domain." J. Symbolic Logic 87, pp. 912--937. arXiv:1904.01362

Quoted from FormalConjectures/Paper/DisjointNPPairs.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, 2 solved and 1 textbook result. It also has 4 API statements, counted here but not shown.

DisjointNPPairs.no_complete_disjoint_NP_pair

Open: stated without proof.

There is no complete disjoint NP pair (Razborov [Ra94]; Pudlák's conjecture DisjNP [Pu17]).

No disjoint NP pair is complete under polynomial-time many-one reductions of pairs. This is the strongest of the "incompleteness in the finite domain" conjectures: it implies that no length-optimal propositional proof system exists [Ra94, KMT03], hence NP ≠ coNP and P ≠ NP. Equivalently [Pu17], for every consistent polynomial-time axiomatized theory T ⊇ S¹₂ some disjoint NP pair is not provably disjoint in T.

theorem no_complete_disjoint_NP_pair : ¬∃ A B : DecisionProblem, IsCompleteNPPair A B

Category research open; AMS 03 Mathematical logic and foundations, 68 Computer science. Declared in FormalConjectures/Paper/DisjointNPPairs.lean, line 113.

DisjointNPPairs.no_complete_disjoint_coNP_pair

Open: stated without proof.

There is no complete disjoint coNP pair (Pudlák's conjecture DisjCoNP [Pu17]).

No disjoint coNP pair is complete under polynomial-time many-one reductions of pairs. This implies that TFNP has no complete problem and that SAT has no p-optimal proof system [Pu17, Kh22].

theorem no_complete_disjoint_coNP_pair : ¬∃ A B : DecisionProblem, IsCompleteCoNPPair A B

Category research open; AMS 03 Mathematical logic and foundations, 68 Computer science. Declared in FormalConjectures/Paper/DisjointNPPairs.lean, line 124.

DisjointNPPairs.no_complete_disjoint_NP_pair.variants.exists_of_NP_eq_coNP

Solved: stated here without proof.

If NP = coNP then a complete disjoint NP pair exists [GSSZ04, Pu17].

The pair (SAT, ¬SAT) is then a disjoint NP pair, and every disjoint NP pair (A, B) reduces to it via a Cook–Levin reduction of A to SAT, since B is disjoint from A.

theorem no_complete_disjoint_NP_pair.variants.exists_of_NP_eq_coNP (h : NP = coNP) :
    ∃ A B : DecisionProblem, IsCompleteNPPair A B

Category research solved; AMS 03 Mathematical logic and foundations, 68 Computer science. Declared in FormalConjectures/Paper/DisjointNPPairs.lean, line 134.

DisjointNPPairs.no_complete_disjoint_NP_pair.variants.NP_ne_coNP

Proved here.

The conjecture implies NP ≠ coNP [Pu17].

theorem no_complete_disjoint_NP_pair.variants.NP_ne_coNP
    (h : ¬∃ A B : DecisionProblem, IsCompleteNPPair A B) : NP ≠ coNP

Category research solved; AMS 03 Mathematical logic and foundations, 68 Computer science. Declared in FormalConjectures/Paper/DisjointNPPairs.lean, line 142.

DisjointNPPairs.no_complete_disjoint_NP_pair.variants.pSeparable_of_P_eq_NP

Textbook result, proved here.

If P = NP then every disjoint NP pair is P-separable, and hence a complete pair exists: each A is then in P and separates (A, B).

theorem no_complete_disjoint_NP_pair.variants.pSeparable_of_P_eq_NP (h : P = NP)
    {A B : DecisionProblem} (hAB : IsDisjointNPPair A B) : IsPSeparable A B

Category textbook; AMS 03 Mathematical logic and foundations, 68 Computer science. Declared in FormalConjectures/Paper/DisjointNPPairs.lean, line 151.

Sources

• FormalConjectures/Paper/DisjointNPPairs.lean at 2055e5ad
• arXiv:1601.01487

LeanDisjointNPPairs.no_complete_disjoint_NP_pair · DisjointNPPairs.no_complete_disjoint_coNP_pair · DisjointNPPairs.no_complete_disjoint_NP_pair.variants.exists_of_NP_eq_coNP · DisjointNPPairs.no_complete_disjoint_NP_pair.variants.NP_ne_coNP · DisjointNPPairs.no_complete_disjoint_NP_pair.variants.pSeparable_of_P_eq_NP

TheoremDubner's conjecture#

Reference: Every even number greater than 4208 is the sum of two t-primes by Harvey Dubner.

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

DubnerConjecture.dubner_conjecture

Open: stated without proof.

Every even number greater than 4208 is the sum of two twin primes.

theorem dubner_conjecture (n : ℕ) (hn : 4208 < n) (h : Even n) :
    ∃ p q : ℕ,
      IsTwinPrime p ∧
      IsTwinPrime q ∧
      p + q = n

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

Sources

• FormalConjectures/Paper/Dubner.lean at 2055e5ad
• Every even number greater than 4208 is the sum of two t-primes

LeanDubnerConjecture.dubner_conjecture

TheoremThe Eisenbud-Green-Harris conjecture#

Let \(S = k[x_1, \dots, x_n]\) with \(x_1 > x_2 > \dots > x_n\) and let \(I \subseteq S\) be a homogeneous ideal. The Hilbert function of \(I\) is \(d \mapsto \dim_k I_d\).

A monomial ideal is an ideal generated by monomials. A monomial ideal \(L\) is lex if for any two monomials \(u, v\) of the same degree with \(u >_{\mathrm{lex}} v\) we have \(u \in L\) whenever \(v \in L\). Macaulay's theorem says that every homogeneous ideal has the same Hilbert function as a unique lex ideal.

Eisenbud-Green-Harris conjecture. If \(I\) contains a regular sequence of forms of degrees \(d_1 \le \dots \le d_c\), then there is a lex ideal \(L\) such that \(I\) has the same Hilbert function as \(L + (x_1^{d_1}, \dots, x_c^{d_c})\).

Eisenbud, Green and Harris proposed the conjecture in [EGH93] and [EGH96] to generalise a theorem of Castelnuovo and Cayley-Bacharach type theorems for zero-dimensional subschemes of \(\mathbb P^m\). It refines Macaulay's theorem, which is the case \(c = 0\).

The conjecture is open in general. It holds when the regular sequence is monomial, by the Clements-Lindström theorem [CL69], and when the degrees grow quickly, namely when \(d_i \ge \sum_{j < i} (d_j - 1)\) for all \(i \ge 3\): this is due to Caviglia and De Stefani [CDS20], improving on Caviglia and Maclagan [CM08], who assumed the strict inequality. Other known cases are \(c \le 2\), and \(d_1 = \dots = d_c = 2\) with \(c \le 5\) by Güntürkün and Hochster; [CDS20] lists these with references.

The Lex-plus-powers conjecture, attributed to Charalambous and Evans, predicts that the ideal \(L + (x_1^{d_1}, \dots, x_c^{d_c})\) above also has the largest graded Betti numbers among all ideals with that Hilbert function containing a regular sequence in those degrees. The Eisenbud-Green-Harris conjecture is its \(i = 0\) case [CS18]. It is not formalised here.

The Hilbert function MvPolynomial.hilbertFunction, lex ideals MvPolynomial.IsLexIdeal and the ideal of pure powers MvPolynomial.purePowersIdeal are defined in FormalConjecturesForMathlib.RingTheory.MvPolynomial.LexPlusPowers.

References: - [EGH93] D. Eisenbud, M. Green, J. Harris, Higher Castelnuovo theory, in Journées de Géométrie Algébrique d'Orsay, Astérisque 218 (1993), 187-202. - [EGH96] D. Eisenbud, M. Green, J. Harris, Cayley-Bacharach theorems and conjectures, Bull. Amer. Math. Soc. 33 (1996), 295-324. PDF - [CS18] G. Caviglia, A. Sammartano, On the Lex-plus-powers conjecture, Adv. Math. 340 (2018), 1148-1163. arXiv:1802.03035, Conjecture 1.1. - [CDS20] G. Caviglia, A. De Stefani, The Eisenbud-Green-Harris conjecture for fast-growing degree sequences, Trans. Amer. Math. Soc. 375 (2022), 2777-2792. arXiv:2007.15467, Definition 2.1, Conjecture 2.3 and Theorem A. The statement formalised below is Conjecture 2.3. - [CM08] G. Caviglia, D. Maclagan, Some cases of the Eisenbud-Green-Harris conjecture, Math. Res. Lett. 15 (2008), 427-433. - [CL69] G. F. Clements, B. Lindström, A generalization of a combinatorial theorem of Macaulay, J. Combin. Theory 7 (1969), 230-238. - [FR12] C. A. Francisco, B. P. Richert, Lex-plus-powers ideals, in Syzygies and Hilbert functions, Lect. Notes Pure Appl. Math. 254, 113-144. PDF

Quoted from FormalConjectures/Paper/EisenbudGreenHarris.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: 1 open and 3 solved.

EisenbudGreenHarris.eisenbud_green_harris

Open: stated without proof.

The Eisenbud-Green-Harris conjecture. Let \(I \subseteq k[x_1, \dots, x_n]\) be a homogeneous ideal containing a regular sequence of forms of degrees \(d_1 \le \dots \le d_c\). Then there is a lex ideal \(L\) such that \(I\) has the same Hilbert function as \(L + (x_1^{d_1}, \dots, x_c^{d_c})\).

theorem eisenbud_green_harris {c : ℕ} (hc : c ≤ n) (d : Fin c → ℕ) (hd : Monotone d)
    (I : Ideal (MvPolynomial (Fin n) k))
    (hI : I.IsHomogeneous (homogeneousSubmodule (Fin n) k))
    (f : Fin c → MvPolynomial (Fin n) k) (hfd : ∀ i, (f i).IsHomogeneous (d i))
    (hfI : ∀ i, f i ∈ I)
    (hf : RingTheory.Sequence.IsRegular (MvPolynomial (Fin n) k) (List.ofFn f)) :
    ∃ L : Ideal (MvPolynomial (Fin n) k), IsLexIdeal L ∧
      ∀ e, hilbertFunction I e = hilbertFunction (L + purePowersIdeal hc d) e

Category research open; AMS 13 Commutative algebra. Declared in FormalConjectures/Paper/EisenbudGreenHarris.lean, line 92.

EisenbudGreenHarris.eisenbud_green_harris.variants.macaulay

Solved: stated here without proof.

Macaulay's theorem: every homogeneous ideal has the same Hilbert function as a lex ideal. This is the case \(c = 0\) of eisenbud_green_harris, where the ideal of pure powers is zero (MvPolynomial.purePowersIdeal_zero).

theorem eisenbud_green_harris.variants.macaulay (I : Ideal (MvPolynomial (Fin n) k))
    (hI : I.IsHomogeneous (homogeneousSubmodule (Fin n) k)) :
    ∃ L : Ideal (MvPolynomial (Fin n) k), IsLexIdeal L ∧
      ∀ e, hilbertFunction I e = hilbertFunction L e

Category research solved; AMS 13 Commutative algebra. Declared in FormalConjectures/Paper/EisenbudGreenHarris.lean, line 108.

EisenbudGreenHarris.eisenbud_green_harris.variants.clements_lindstrom

Solved: stated here without proof.

The Clements-Lindström theorem [CL69]: the conjecture holds for an ideal that already contains the pure powers \(x_1^{d_1}, \dots, x_c^{d_c}\).

theorem eisenbud_green_harris.variants.clements_lindstrom {c : ℕ} (hc : c ≤ n) (d : Fin c → ℕ)
    (hd : Monotone d) (I : Ideal (MvPolynomial (Fin n) k))
    (hI : I.IsHomogeneous (homogeneousSubmodule (Fin n) k)) (hIp : purePowersIdeal hc d ≤ I) :
    ∃ L : Ideal (MvPolynomial (Fin n) k), IsLexIdeal L ∧
      ∀ e, hilbertFunction I e = hilbertFunction (L + purePowersIdeal hc d) e

Category research solved; AMS 13 Commutative algebra. Declared in FormalConjectures/Paper/EisenbudGreenHarris.lean, line 119.

EisenbudGreenHarris.eisenbud_green_harris.variants.caviglia_deStefani

Solved: stated here without proof.

The conjecture holds when the degrees grow quickly enough, namely when \(d_i \ge \sum_{j < i} (d_j - 1)\) for all \(i \ge 3\). This is [CDS20, Theorem A]; Caviglia and Maclagan [CM08] had proved it under the strict inequality. Indices here are 0-based, so \(i \ge 3\) becomes 2 ≤ i. The subtraction is on ℕ, which is harmless because a regular sequence of degrees d forces 1 ≤ d j.

theorem eisenbud_green_harris.variants.caviglia_deStefani {c : ℕ} (hc : c ≤ n) (d : Fin c → ℕ)
    (hd : Monotone d) (hgrow : ∀ i : Fin c, 2 ≤ (i : ℕ) → ∑ j ∈ Finset.Iio i, (d j - 1) ≤ d i)
    (I : Ideal (MvPolynomial (Fin n) k))
    (hI : I.IsHomogeneous (homogeneousSubmodule (Fin n) k))
    (f : Fin c → MvPolynomial (Fin n) k) (hfd : ∀ i, (f i).IsHomogeneous (d i))
    (hfI : ∀ i, f i ∈ I)
    (hf : RingTheory.Sequence.IsRegular (MvPolynomial (Fin n) k) (List.ofFn f)) :
    ∃ L : Ideal (MvPolynomial (Fin n) k), IsLexIdeal L ∧
      ∀ e, hilbertFunction I e = hilbertFunction (L + purePowersIdeal hc d) e

Category research solved; AMS 13 Commutative algebra. Declared in FormalConjectures/Paper/EisenbudGreenHarris.lean, line 134.

Sources

• FormalConjectures/Paper/EisenbudGreenHarris.lean at 2055e5ad
• PDF

LeanEisenbudGreenHarris.eisenbud_green_harris · EisenbudGreenHarris.eisenbud_green_harris.variants.macaulay · EisenbudGreenHarris.eisenbud_green_harris.variants.clements_lindstrom · EisenbudGreenHarris.eisenbud_green_harris.variants.caviglia_deStefani

TheoremEuclidean Ramsey configurations on a circle#

Reference: OpenAI, A classification of finite Euclidean Ramsey configurations (2026). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-classification-of-finite-Euclidean-Ramsey-configurations-September-23-2026/paper.pdf

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

EuclideanRamseyCircle.at_most_five_circle_points_ramsey

Solved: stated here without proof.

Every nonempty configuration of at most five distinct points on a circle is Euclidean Ramsey: every finite colouring of a suitable Euclidean space has a monochromatic copy with the same pairwise distances. Singletons and radius-zero circles are included.

theorem at_most_five_circle_points_ramsey {s : ℕ} (a : Fin s → E (Fin 2))
    (hs : 0 < s) (hs5 : s ≤ 5) (ha : Function.Injective a)
    (hsphere : ∃ c : E (Fin 2), ∃ r : ℝ, ∀ i, dist (a i) c = r) :
    ∀ colors : ℕ, 2 ≤ colors → ∃ D : ℕ, 1 ≤ D ∧
      ∀ c : E (Fin D) → Fin colors, ∃ b : Fin s → E (Fin D),
        (∀ i j, dist (b i) (b j) = dist (a i) (a j)) ∧
          ∃ k : Fin colors, ∀ i, c (b i) = k

Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/Paper/EuclideanRamseyCircle.lean, line 37.

Sources

• FormalConjectures/Paper/EuclideanRamseyCircle.lean at 2055e5ad
• https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-classification-of-finite-Euclidean-Ramsey-configurations-September-23-2026/paper.pdf

LeanEuclideanRamseyCircle.at_most_five_circle_points_ramsey

TheoremIs a finite locally free group scheme killed by its order?#

A finite locally free group scheme of rank n is the group scheme analogue of a finite group of order n. Lagrange's theorem gives g ^ n = 1 in a finite group of order n, and Grothendieck asked whether the n-th power map of such a group scheme is trivial. The answer is affirmative over a reduced base and for commutative group schemes, and negative in general. Which exponents kill every group scheme of a given rank is open.

A group scheme is represented here by its coordinate Hopf algebra A over the base ring R. A is not assumed to be cocommutative, so the group scheme is not assumed to be commutative. The base is a ring rather than a scheme: a finite locally free group scheme is affine over its base, and being killed by m is local on the base, so nothing is lost.

References: - M. Demazure and A. Grothendieck, Schémas en groupes (SGA 3), re-edition by P. Gille and P. Polo. Exp. VIII, Rem. 7.3.1 poses the question; an editors' note records that the re-edition drops the commutativity assumption there. Exp. VIIA, Prop. 8.5 settles the case of a field and Cor. 8.5.2 the case of a reduced base. - R. Schoof, Is a finite locally free group scheme killed by its order?, a survey of the question and of the cases that are known, written before the counterexample - J. Tate and F. Oort, Group schemes of prime order, p. 4 for Deligne's theorem and p. 5, which records the general question as open in 1970 - Mathlib, A finite free group scheme of rank four that is not killed by four, the counterexample

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

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

FiniteLocallyFreeGroupSchemeExponent.killed_by_rank

Solved: stated here; a Lean proof is at https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Counterexamples/GrothendieckPower.lean#L882-L892.

Grothendieck's question: is every finite locally free group scheme of rank \(n\), over every commutative ring, killed by \(n\)?

The answer is no. There is a commutative Hopf algebra of rank \(4\) over a finite non-reduced ring whose fourth power map is not trivial; its eighth power map is trivial. The formalised counterexample lives in Type, so the statement quantifies over rings and algebras in Type.

theorem killed_by_rank :
    ¬ ∀ n : ℕ+, IsUniversalKillingExponent.{0, 0} n n

Category research solved; AMS 14 Algebraic geometry, 16 Associative rings and algebras. Declared in FormalConjectures/Paper/FiniteLocallyFreeGroupSchemeExponent.lean, line 157.

FiniteLocallyFreeGroupSchemeExponent.killed_by_rank.variants.field

Solved: stated here without proof.

Over a field the answer is affirmative: a finite group scheme of rank \(n\) over a field is killed by \(n\). This is [SGA 3], Exp. VIIA, Prop. 8.5.

theorem killed_by_rank.variants.field (n : ℕ+) (k : Type*) [Field k] (A : Type*) [CommRing A]
    [HopfAlgebra k A] [Module.Finite k A] (hn : Module.finrank k A = (n : ℕ)) :
    IsKilledBy k A n

Category research solved; AMS 14 Algebraic geometry, 16 Associative rings and algebras. Declared in FormalConjectures/Paper/FiniteLocallyFreeGroupSchemeExponent.lean, line 166.

FiniteLocallyFreeGroupSchemeExponent.killed_by_rank.variants.reduced_base

Solved: stated here without proof.

Over a reduced base ring the answer is affirmative: every finite locally free group scheme of rank \(n\) over a reduced commutative ring is killed by \(n\). This is [SGA 3], Exp. VIIA, Cor. 8.5.2, deduced there from the case of a field.

theorem killed_by_rank.variants.reduced_base (n : ℕ+) (R : Type*) [CommRing R] [IsReduced R]
    (A : Type*) [CommRing A] [HopfAlgebra R A] [Module.Finite R A] [Module.Projective R A]
    (hn : Module.rankAtStalk (R := R) A = fun _ ↦ (n : ℕ)) :
    IsKilledBy R A n

Category research solved; AMS 14 Algebraic geometry, 16 Associative rings and algebras. Declared in FormalConjectures/Paper/FiniteLocallyFreeGroupSchemeExponent.lean, line 177.

FiniteLocallyFreeGroupSchemeExponent.killed_by_rank.variants.commutative

Solved: stated here without proof.

Deligne's theorem: a finite locally free commutative group scheme of rank \(n\) over any commutative ring is killed by \(n\). Commutativity of the group scheme is cocommutativity of its coordinate Hopf algebra. See [SGA 3], Exp. VIIA, Rem. 8.5.3 and [TO70], p. 4.

theorem killed_by_rank.variants.commutative (n : ℕ+) (R : Type*) [CommRing R] (A : Type*)
    [CommRing A] [HopfAlgebra R A] [Coalgebra.IsCocomm R A] [Module.Finite R A]
    [Module.Projective R A]
    (hn : Module.rankAtStalk (R := R) A = fun _ ↦ (n : ℕ)) :
    IsKilledBy R A n

Category research solved; AMS 14 Algebraic geometry, 16 Associative rings and algebras. Declared in FormalConjectures/Paper/FiniteLocallyFreeGroupSchemeExponent.lean, line 189.

FiniteLocallyFreeGroupSchemeExponent.optimal_exponent

Open: stated without proof.

Determine the function assigning to each positive integer \(n\) the least positive integer \(m\) such that every finite locally free group scheme of rank \(n\), over every commutative ring, is killed by \(m\). The value is \(0\) if there is no such \(m\), since sInf ∅ = 0 in ℕ. As in killed_by_rank, the rings and algebras are in Type.

Grothendieck asked whether this least exponent is \(n\) itself. It is not, already for \(n = 4\). If some positive exponent kills every group scheme of rank \(n\), then these exponents are the multiples of the least one, so minimality for \(\le\) agrees with minimality for divisibility.

theorem optimal_exponent :
    ∀ n, sInf ((↑) '' {m | IsUniversalKillingExponent.{0, 0} n m} : Set ℕ) = optimal_exponent.answer
      n

Category research open; AMS 14 Algebraic geometry, 16 Associative rings and algebras. Declared in FormalConjectures/Paper/FiniteLocallyFreeGroupSchemeExponent.lean, line 209.

Sources

• FormalConjectures/Paper/FiniteLocallyFreeGroupSchemeExponent.lean at 2055e5ad
• M. Demazure and A. Grothendieck, Schémas en groupes (SGA 3), re-edition by P. Gille and P. Polo

LeanFiniteLocallyFreeGroupSchemeExponent.killed_by_rank · FiniteLocallyFreeGroupSchemeExponent.killed_by_rank.variants.field · FiniteLocallyFreeGroupSchemeExponent.killed_by_rank.variants.reduced_base · FiniteLocallyFreeGroupSchemeExponent.killed_by_rank.variants.commutative · FiniteLocallyFreeGroupSchemeExponent.optimal_exponent

TheoremMain conjecture on fusible numbers#

References: - Fusible numbers and Peano Arithmetic, by Jeff Erickson, Gabriel Nivasch, and Junyan Xu. - Fusible numbers and Peano Arithmetic, Logical Methods in Computer Science, Volume 18, Issue 3 (July 28, 2022).

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

FusibleNumber.conj_7_1

Open: stated without proof.

If x is a fusible number and y is its successor, then the interval [x + 1, y + 1) can be divided into intervals [ℓₙ, ℓₙ₊₁), such that the fusible numbers in [ℓₙ, ℓₙ₊₁) are obtained by fusing the n + 1st successor of x with a fusible number. This formalization differs from Conjecture 7.1 in the paper in four ways: (1) it is obtained from Conjecture 7.1 by plugging in n + 1 into n, which simplifies the expressions and removes the need to assume n ≥ 1; (2) the n + 1st successor s^(n+1)(x) is replaced by the explicit value x + (2 - 1 / 2 ^ n) * m; (3) instead of defining y to be the successor of x, we assert that there is no fusible number strictly between x and y; (4) instead of using ∃ z, IsFusible z ∧ q = s^(n+1)(x) ~ z we use the value of z determined by the equality, namely z = 2 * q - 1 - s^(n+1)(x), and it is easy to see z ∈ [x + 1 - m / 2 ^ n, x + 1) as required.

theorem conj_7_1 (x y q : ℚ) (n : ℕ) (fus_x : IsFusible x) (fus_y : IsFusible y) (lt : x < y)
    (nmem_Ioo : ∀ z, IsFusible z → z ∉ Set.Ioo x y) :
    let m := y - x
    let ℓ (n : ℕ) := y + 1 - m / 2 ^ n
    IsFusible q → q ∈ Set.Ico (ℓ n) (ℓ (n + 1)) → IsFusible (2 * q - 1 - x - (2 - 1 / 2 ^ n) * m)

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

Sources

• FormalConjectures/Paper/FusibleNumber.lean at 2055e5ad
• Fusible numbers and Peano Arithmetic

LeanFusibleNumber.conj_7_1

TheoremGourevitch's series identity#

References: - About a New Kind of Ramanujan-Type Series by Jesús Guillera - [G2003] Guillera, Jesús. "About a new kind of Ramanujan-type series." Experimental Mathematics 12.4 (2003): 507-510. - [A2025] Au, Kam Cheong. "Wilf-Zeilberger seeds and non-trivial hypergeometric identities." Journal of Symbolic Computation 130 (2025): 102421. arXiv:2312.14051

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

Gourevitch.gourevitch_series_identity

Solved: stated here without proof.

The Gourevitch series identity: The following identity holds: \(\sum_{n=0}^{\infty} \frac{1 + 14 n + 76 n^2 + 168 n^3}{2^{20 n}} \binom{2n}{n}^7 = \frac{32}{\pi^3}.\) This was originally conjectured in [G2003] by Guillera and proven in [A2025] by Au.

theorem gourevitch_series_identity :
    ∑' n : ℕ, ((1 + 14 * n + 76 * n ^ 2 + 168 * n ^ 3) / (2 ^ (20 * n)) : ℝ)
      * Nat.centralBinom n ^ 7 = 32 / (Real.pi ^ 3)

Category research solved; AMS 11 Number theory, 33 Special functions. Declared in FormalConjectures/Paper/Gourevitch.lean, line 40.

Sources

• FormalConjectures/Paper/Gourevitch.lean at 2055e5ad
• About a New Kind of Ramanujan-Type Series

LeanGourevitch.gourevitch_series_identity

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.