The Hall ratio conjecture… to Moments of the Riemann zeta…

TheoremThe Hall ratio conjecture (Harris 2019) — disproved #

References: * [Ha19] Harris, D. G. (2019). "Some results on chromatic number as a function of triangle count." SIAM J. Discrete Math. 33, pp. 546--563. * [DOW20] Dvořák, Z., Ossona de Mendez, P. and Wu, H. (2020). "1-subdivisions, the fractional chromatic number and the Hall ratio." Combinatorica 40, pp. 759--774. arXiv:1812.07327 * [BLMNPV22] Blumenthal, A., Lidický, B., Martin, R. R., Norin, S., Pfender, F. and Volec, J. (2022). "Counterexamples to a conjecture of Harris on Hall ratio." SIAM J. Discrete Math. 36, pp. 1678--1686. arXiv:1811.11116 * [SU97] Scheinerman, E. R. and Ullman, D. H. (1997). Fractional Graph Theory. Wiley.

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

`HallRatioConjecture.hall_ratio_conjecture`

Solved: stated here without proof.

The Hall ratio conjecture (Harris 2019) — disproved.

Harris conjectured that the fractional chromatic number is bounded by a constant multiple of the Hall ratio: there is a constant \(C\) with \(\chi_f(G) \le C\,\rho(G)\) for every graph \(G\). This is false: Dvořák, Ossona de Mendez and Wu [DOW20] and, independently, Blumenthal, Lidický, Martin, Norin, Pfender and Volec [BLMNPV22] constructed graphs with \(\chi_f / \rho\) arbitrarily large.

theorem hall_ratio_conjecture : ¬
    ∃ C : ℝ, ∀ {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V),
      G.fractionalChromaticNumber ≤ C * hallRatio G

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

`HallRatioConjecture.hall_ratio_conjecture.variants.hallRatio_le_fractionalChromaticNumber`

Solved: stated here without proof.

The Hall ratio is a lower bound for the fractional chromatic number.

For every graph, \(\rho(G) \le \chi_f(G)\) (see [SU97]); the conjecture asked for an inequality in the other direction up to a constant.

theorem hall_ratio_conjecture.variants.hallRatio_le_fractionalChromaticNumber
    {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) :
    hallRatio G ≤ G.fractionalChromaticNumber

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

`HallRatioConjecture.hall_ratio_conjecture.variants.unbounded`

Solved: stated here without proof.

Unbounded ratio (Dvořák–Ossona de Mendez–Wu 2020; Blumenthal et al. 2022).

For every \(C\) there is a graph with \(\chi_f(G) > C\,\rho(G)\).

References: [DOW20], [BLMNPV22].

theorem hall_ratio_conjecture.variants.unbounded (C : ℝ) :
    ∃ (V : Type) (_ : Fintype V) (_ : DecidableEq V) (G : SimpleGraph V),
      C * hallRatio G < G.fractionalChromaticNumber

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

Sources

LeanHallRatioConjecture.hall_ratio_conjecture · HallRatioConjecture.hall_ratio_conjecture.variants.hallRatio_le_fractionalChromaticNumber · HallRatioConjecture.hall_ratio_conjecture.variants.unbounded

TheoremHartshorne's conjecture on Vector Bundles #

References: * [Har1974] R. Hartshorne, Varieties of small codimension in projective space. * [MO2010] Evidences on Hartshorne's conjecture? References?

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

`AlgebraicGeometry.Scheme.harthshorne_conjecture`

Open: stated without proof.

There are no indecomposable vector bundles of rank 2 on \(\mathbb{P}^n\) for \(n \ge 7\). This is Conjecture 6.3 in [Har1974].

theorem harthshorne_conjecture (n : ℕ) (hn : 7 ≤ n)
    (𝓕 : VectorBundles ℙ(Fin (n + 1); Spec (.of ℂ)))
    (h𝓕 : 𝓕.rank = 2) :
    Nonempty (𝓕.Splitting (Fin 2))

Category research open; AMS 14 Algebraic geometry. Declared in FormalConjectures/Paper/HartshorneConjecture.lean, line 85.

Sources

LeanAlgebraicGeometry.Scheme.harthshorne_conjecture

TheoremConjectures around homogeneous topological spaces #

This file formalizes the notions of a homogeneous topological space and of (ω-)monolithic topological spaces, and states some open problems about homogeneous and monolithic compact spaces.

References: * [Ar2013] Arhangeliski, Alexandr. "Selected old open problems in general topology." Buletinul Academiei de Ştiinţe a Republicii Moldova. Matematica 73.2-3 (2013): 37-46. https://www.math.md/files/basm/y2013-n2-3/y2013-n2-3-(pp37-46).pdf.pdf * [Ar1987] Arhangel'skii, A. V. "Topological homogeneity. Topological groups and their continuous images." Russian Mathematical Surveys 42.2 (1987): 83-131. https://doi.org/10.1070/RM1987v042n02ABEH001333

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

`Homogeneous.homogeneousSpace_exists_inj_tendsto`

Open: stated without proof.

Problem 13 in [Ar2013]: Is it true that every infinite homogeneous compact hausdorff space contains a non-trivial convergent sequence?

theorem homogeneousSpace_exists_inj_tendsto :
    ∀ (X : Type) (_ : TopologicalSpace X), ¬ Finite X → T2Space X → CompactSpace X →
      HomogeneousSpace X → ∃ s : ℕ → X, s.Injective ∧ ∃ a : X, Tendsto s atTop (nhds a)

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

`Homogeneous.homogeneousSpace_exists_surjective`

Open: stated without proof.

Problem 14 in [Ar2013]: Is it possible to represent an arbitrary compact hausdorff space as an image of a homogeneous compact space under a continuous mapping?

theorem homogeneousSpace_exists_surjective :
    ∀ (X : Type) (_ : TopologicalSpace X), T2Space X → CompactSpace X →
      ∃ (Y : Type) (_ : TopologicalSpace Y), T2Space Y ∧ CompactSpace Y ∧ HomogeneousSpace Y ∧
        ∃ f : Y → X, Continuous f ∧ f.Surjective

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

`Homogeneous.firstCountableTopology_of_countablyMonolithicSpace`

Open: stated without proof.

Problem 15 in [Ar2013]: Is every homogeneous ω-monolithic compact hausdorff space first countable?

theorem firstCountableTopology_of_countablyMonolithicSpace :
    ∀ (X : Type) (_ : TopologicalSpace X), T2Space X → CompactSpace X →
      HomogeneousSpace X → CountablyMonolithicSpace X → FirstCountableTopology X

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

`Homogeneous.countablyMonolithicSpace_card_lt`

Open: stated without proof.

Problem 16 in [Ar2013]: Is the cardinality of every homogeneous ω-monolithic compact hausdorff space not greater than 𝔠?

theorem countablyMonolithicSpace_card_lt :
    ∀ (X : Type) (_ : TopologicalSpace X), T2Space X → CompactSpace X →
      HomogeneousSpace X → CountablyMonolithicSpace X → #X ≤ 𝔠

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

`Homogeneous.monolithicSpace_exists_nhds_generated_countable`

Open: stated without proof.

Problem 17 in [Ar2013]: Is it true that every nonempty monolithic compact hausdorff space contains a point with a first countable neighborhood basis?

Note: Nonempty X is required since the conclusion asserts the existence of a point.

theorem monolithicSpace_exists_nhds_generated_countable :
    ∀ (X : Type) (_ : TopologicalSpace X), T2Space X → CompactSpace X →
      Nonempty X → MonolithicSpace X → ∃ x : X, (𝓝 x).IsCountablyGenerated

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

Sources

LeanHomogeneous.homogeneousSpace_exists_inj_tendsto · Homogeneous.homogeneousSpace_exists_surjective · Homogeneous.firstCountableTopology_of_countablyMonolithicSpace · Homogeneous.countablyMonolithicSpace_card_lt · Homogeneous.monolithicSpace_exists_nhds_generated_countable

TheoremKaplansky's problem on the values of the \(u\)-invariant #

The \(u\)-invariant \(u(F)\) of a field \(F\) is the largest dimension of an anisotropic quadratic form over \(F\), or \(\infty\) if there is no largest one; that is, \(u(F) = n\) exactly when IsGreatest (QuadraticForm.anisotropicDims F) n. Following [Kaplansky1953] and [MerkurjevParimala2025, §5.1], all fields are of characteristic not \(2\).

Kaplansky introduced the invariant (his \(C(F)\)) in [Kaplansky1953, p. 201], proved that \(u(F) \ne 3\) (his Theorem 2), observed that every power of \(2\) occurs (his Theorem 3 gives \(u(F((t))) = 2u(F)\)), and conjectured that \(u(F)\) is a power of \(2\) whenever it is finite [Kaplansky1953, p. 202]. It is classical that \(u(F) \notin \{3, 5, 7\}\) [Lam2005, Proposition XI.6.8], [EKM2008, Corollary 36.4]. Merkurjev disproved Kaplansky's conjecture with a field of \(u\)-invariant \(6\) [Merkurjev1989] and then showed that every positive even integer is a \(u\)-invariant [Merkurjev1991]. Izhboldin constructed a field of \(u\)-invariant \(9\) [Izhboldin2001], and Vishik fields of \(u\)-invariant \(2^r + 1\) for every \(r \ge 3\) [Vishik2009]. A 2026 preprint of Karpenko constructs fields of \(u\)-invariant \(n\) for every \(n\) that is neither of the form \(2^r - 1\) nor of the form \(2^r - 3\) [Karpenko2026]; as of September 2026 it is not yet peer-reviewed.

The problem (u_invariant_values) is to determine which integers are \(u\)-invariants of fields. The survey [MerkurjevParimala2025, §5.1] records the expectation that every odd integer \(\ge 9\) is a \(u\)-invariant (u_invariant_values.variants.odd). Given the results above, the problem is open exactly for the integers \(2^r - 1\) and \(2^r - 3\) with \(r \ge 4\), the smallest of which are \(13\) and \(15\).

References: - [Kaplansky1953] I. Kaplansky, Quadratic forms, J. Math. Soc. Japan 5 (1953), 200–207, doi:10.2969/jmsj/00520200. - [Lam2005] T. Y. Lam, Introduction to quadratic forms over fields, Grad. Stud. Math. 67, Amer. Math. Soc., 2005, doi:10.1090/gsm/067. - [EKM2008] R. Elman, N. Karpenko, A. Merkurjev, The algebraic and geometric theory of quadratic forms, Amer. Math. Soc. Colloq. Publ. 56, Amer. Math. Soc., 2008, doi:10.1090/coll/056. - [Merkurjev1989] A. S. Merkurjev, Kaplansky's conjecture in the theory of quadratic forms (Russian), Zap. Nauchn. Sem. LOMI 175 (1989), 75–89; English transl. J. Soviet Math. 57 (1991), no. 6, 3489–3497, doi:10.1007/BF01100118. - [Merkurjev1991] A. S. Merkurjev, Simple algebras and quadratic forms (Russian), Izv. Akad. Nauk SSSR Ser. Mat. 55 (1991), no. 1, 218–224; English transl. Math. USSR-Izv. 38 (1992), no. 1, 215–221, doi:10.1070/IM1992v038n01ABEH002195. - [Izhboldin2001] O. T. Izhboldin, Fields of \(u\)-invariant \(9\), Ann. of Math. (2) 154 (2001), no. 3, 529–587, doi:10.2307/3062141. - [Vishik2009] A. Vishik, Fields of \(u\)-invariant \(2^r + 1\), pp. 661–685 in Algebra, arithmetic, and geometry: in honor of Yu. I. Manin, Vol. II, Progr. Math. 270, Birkhäuser, 2009, doi:10.1007/978-0-8176-4747-6_22. - [Karpenko2026] N. A. Karpenko, Fields of any \(u\)-invariant but a 2-power minus 1 or 3, preprint, 5 August 2026, author's web page. - [MerkurjevParimala2025] A. Merkurjev, R. Parimala, Quadratic forms beyond arithmetic, Notices Amer. Math. Soc. 72 (2025), no. 7, 711–718, doi:10.1090/noti3192.

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

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

`KaplanskyUInvariant.u_invariant_values`

Open: stated without proof.

The values of the \(u\)-invariant, stated as in [MerkurjevParimala2025, §5.1]: which integers are \(u\)-invariants of fields (of characteristic not \(2\))? The question goes back to [Kaplansky1953], who conjectured that only powers of \(2\) occur (u_invariant_values.variants.kaplansky_conjecture). Every positive even integer is a \(u\)-invariant (u_invariant_values.variants.even), \(3\), \(5\) and \(7\) are not (u_invariant_values.variants.not_three, u_invariant_values.variants.not_five, u_invariant_values.variants.not_seven), and it is expected that every odd integer \(\ge 9\) is (u_invariant_values.variants.odd). Granting the preprint [Karpenko2026] (u_invariant_values.variants.karpenko), the answer is known for every \(n\) except \(n = 2^r - 1\) and \(n = 2^r - 3\) with \(r \ge 4\).

theorem u_invariant_values :
    ∀ n, n ∈ u_invariant_values.answer ↔ IsUInvariant n

Category research open; AMS 11 Number theory, 12 Field theory and polynomials. Declared in FormalConjectures/Paper/KaplanskyUInvariant.lean, line 136.

`KaplanskyUInvariant.u_invariant_values.variants.kaplansky_conjecture`

Solved: stated here without proof.

Kaplansky's conjecture [Kaplansky1953, p. 202]: the \(u\)-invariant of a field is a power of \(2\) whenever it is finite. Disproved by Merkurjev, who constructed a field of \(u\)-invariant \(6\) [Merkurjev1989] (u_invariant_values.variants.even).

theorem u_invariant_values.variants.kaplansky_conjecture :
    ¬ ∀ n, IsUInvariant n → ∃ k, n = 2 ^ k

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

`KaplanskyUInvariant.u_invariant_values.variants.not_three`

Solved: stated here without proof.

The \(u\)-invariant is never \(3\) [Kaplansky1953, Theorem 2]; see also [Lam2005, Proposition XI.6.8] and [EKM2008, Corollary 36.4].

theorem u_invariant_values.variants.not_three : ¬ IsUInvariant 3

Category research solved; AMS 11 Number theory, 12 Field theory and polynomials. Declared in FormalConjectures/Paper/KaplanskyUInvariant.lean, line 153.

`KaplanskyUInvariant.u_invariant_values.variants.not_five`

Solved: stated here without proof.

The \(u\)-invariant is never \(5\) [Lam2005, Proposition XI.6.8], [EKM2008, Corollary 36.4].

theorem u_invariant_values.variants.not_five : ¬ IsUInvariant 5

Category research solved; AMS 11 Number theory, 12 Field theory and polynomials. Declared in FormalConjectures/Paper/KaplanskyUInvariant.lean, line 158.

`KaplanskyUInvariant.u_invariant_values.variants.not_seven`

Solved: stated here without proof.

The \(u\)-invariant is never \(7\) [Lam2005, Proposition XI.6.8], [EKM2008, Corollary 36.4].

theorem u_invariant_values.variants.not_seven : ¬ IsUInvariant 7

Category research solved; AMS 11 Number theory, 12 Field theory and polynomials. Declared in FormalConjectures/Paper/KaplanskyUInvariant.lean, line 163.

`KaplanskyUInvariant.u_invariant_values.variants.two_pow`

Solved: stated here; a Lean proof is at https://github.com/anatoliiohorodnyk/lean-fc-proofs/blob/47cc44ab944b6fd29b98a256ed4f92c8316f86bf/Proofs/T_KaplanskyUInvariant_u_invariant_values_variants_two_pow.lean#L563.

Every power of \(2\) is a \(u\)-invariant [Kaplansky1953, p. 202]: Theorem 3 of [Kaplansky1953] gives \(u(F((t))) = 2u(F)\), so \(u(\mathbb{C}((t_1)) \cdots ((t_k))) = 2^k\); see also [EKM2008, §38].

theorem u_invariant_values.variants.two_pow (k : ℕ) : IsUInvariant (2 ^ k)

Category research solved; AMS 11 Number theory, 12 Field theory and polynomials. Declared in FormalConjectures/Paper/KaplanskyUInvariant.lean, line 173.

`KaplanskyUInvariant.u_invariant_values.variants.even`

Solved: stated here without proof.

Merkurjev's theorem [Merkurjev1991], see also [EKM2008, Theorem 38.4]: every positive even integer is a \(u\)-invariant. The case \(6\), the first counterexample to Kaplansky's conjecture, is [Merkurjev1989].

theorem u_invariant_values.variants.even (n : ℕ) (hn : Even n) (hn₀ : n ≠ 0) :
    IsUInvariant n

Category research solved; AMS 11 Number theory, 12 Field theory and polynomials. Declared in FormalConjectures/Paper/KaplanskyUInvariant.lean, line 182.

`KaplanskyUInvariant.u_invariant_values.variants.nine`

Solved: stated here without proof.

Izhboldin's theorem [Izhboldin2001]: there is a field of \(u\)-invariant \(9\), the first example of an odd \(u\)-invariant greater than \(1\).

theorem u_invariant_values.variants.nine : IsUInvariant 9

Category research solved; AMS 11 Number theory, 12 Field theory and polynomials. Declared in FormalConjectures/Paper/KaplanskyUInvariant.lean, line 189.

`KaplanskyUInvariant.u_invariant_values.variants.two_pow_add_one`

Solved: stated here without proof.

Vishik's theorem [Vishik2009, Corollary 5.2]: for every \(r \ge 3\) there is a field of \(u\)-invariant \(2^r + 1\).

theorem u_invariant_values.variants.two_pow_add_one (r : ℕ) (hr : 3 ≤ r) :
    IsUInvariant (2 ^ r + 1)

Category research solved; AMS 11 Number theory, 12 Field theory and polynomials. Declared in FormalConjectures/Paper/KaplanskyUInvariant.lean, line 195.

`KaplanskyUInvariant.u_invariant_values.variants.karpenko`

Solved: stated here without proof.

Karpenko's theorem [Karpenko2026, Theorem 1.1]: if neither \(n + 1\) nor \(n + 3\) is a power of \(2\), then there is a field of \(u\)-invariant \(n\). This covers every positive integer except \(1\), \(3\), \(5\), \(7\) and the integers \(2^r - 1\), \(2^r - 3\) with \(r \ge 4\). As of September 2026 the result is a preprint and not yet peer-reviewed.

theorem u_invariant_values.variants.karpenko (n : ℕ) (h₁ : ∀ r, 2 ^ r ≠ n + 1)
    (h₃ : ∀ r, 2 ^ r ≠ n + 3) : IsUInvariant n

Category research solved; AMS 11 Number theory, 12 Field theory and polynomials. Declared in FormalConjectures/Paper/KaplanskyUInvariant.lean, line 206.

`KaplanskyUInvariant.u_invariant_values.variants.eleven`

Proved here.

The special case \(n = 11\) of u_invariant_values.variants.karpenko (neither \(12\) nor \(14\) is a power of \(2\)), the first odd value not of the form \(2^r + 1\) shown to be a \(u\)-invariant; it was announced in the preprint Fields of \(u\)-invariant 11 (21 April 2026) that [Karpenko2026] absorbs.

theorem u_invariant_values.variants.eleven : IsUInvariant 11

Category research solved; AMS 11 Number theory, 12 Field theory and polynomials. Declared in FormalConjectures/Paper/KaplanskyUInvariant.lean, line 217.

`KaplanskyUInvariant.u_invariant_values.variants.odd`

Open: stated without proof.

The expectation recorded in [MerkurjevParimala2025, §5.1]: every odd integer \(\ge 9\) is a \(u\)-invariant. By u_invariant_values.variants.karpenko this is open exactly for the integers \(2^r - 1\) and \(2^r - 3\) with \(r \ge 4\).

theorem u_invariant_values.variants.odd :
    ∀ n, Odd n → 9 ≤ n → IsUInvariant n

Category research open; AMS 11 Number theory, 12 Field theory and polynomials. Declared in FormalConjectures/Paper/KaplanskyUInvariant.lean, line 230.

`KaplanskyUInvariant.u_invariant_values.variants.thirteen`

Open: stated without proof.

The smallest open case of the form \(2^r - 3\): is there a field of \(u\)-invariant \(13\)?

theorem u_invariant_values.variants.thirteen : IsUInvariant 13

Category research open; AMS 11 Number theory, 12 Field theory and polynomials. Declared in FormalConjectures/Paper/KaplanskyUInvariant.lean, line 236.

`KaplanskyUInvariant.u_invariant_values.variants.fifteen`

Open: stated without proof.

The smallest open case of the form \(2^r - 1\): is there a field of \(u\)-invariant \(15\)?

theorem u_invariant_values.variants.fifteen : IsUInvariant 15

Category research open; AMS 11 Number theory, 12 Field theory and polynomials. Declared in FormalConjectures/Paper/KaplanskyUInvariant.lean, line 241.

Sources

TheoremKotzig's Conjecture #

Reference: A. Kotzig, cited in A. Rosa, On certain valuations of the vertices of a graph, Theory of Graphs (Internat. Sympos., Rome, 1966), Gordon and Breach, 1967, pp. 349–355.

Kotzig conjectured that for every \(n\), the complete graph \(K_{2n+1}\) decomposes into copies of any \(n\)-edge tree via cyclic shifts of a single embedding. This is strictly stronger than Ringel's conjecture; see Paper/RingelConjecture.lean. The large-\(n\) case is proved by Montgomery–Pokrovskiy–Sudakov; see Arxiv/2001.02665/RingelConjecture.lean.

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

`KotzigConjecture.kotzig_conjecture`

Open: stated without proof.

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

The \(2n+1\) copies are \(f_0, f_1, \dots, f_{2n}\) where \(f_i(v) = f_0(v) + i\) for all vertices \(v\) — each copy is obtained by adding \(i \pmod{2n+1}\) to every vertex of the base copy. This is strictly stronger than RingelConjecture.ringel_conjecture.

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

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

Sources

FormalConjectures/Paper/KotzigConjecture.lean at 2055e5ad

LeanKotzigConjecture.kotzig_conjecture

TheoremKurepa's conjecture #

Reference: On the left factorial function !N, by Đuro Kurepa Math. Balkanica 1, p. 147-153, 1971

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

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

`Kurepa.kurepa_conjecture`

Open: stated without proof.

Kurepa's conjecture

For all \(n\),

\[!n\not\equiv 0 \mod n\]

This appears as B44 "Sums of factorials." in Unsolved Problems in Number Theory by Richard K. Guy

theorem kurepa_conjecture (n : ℕ) (h_n : 2 < n) : (!n : ℕ) % n ≠ 0

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

`Kurepa.kurepa_conjecture.variants.prime`

Open: stated without proof.

This statement can be reduced to the prime case only.

theorem kurepa_conjecture.variants.prime (p : ℕ) (h_p : 2 < p) :
    p.Prime → (!p : ℕ) % p ≠ 0

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

`Kurepa.kurepa_conjecture.prime_reduction`

Textbook result, proved here.

Kurepa's conjecture for all integers greater than 2 is equivalent to the conjecture restricted to primes greater than 2.

theorem kurepa_conjecture.prime_reduction : (∀ n, 2 < n → (!n : ℕ) % n ≠ 0)
    ↔ (∀ p, 2 < p → p.Prime → (!p : ℕ) % p ≠ 0)

Category textbook; AMS 11 Number theory. Declared in FormalConjectures/Paper/Kurepa.lean, line 65.

`Kurepa.kurepa_conjecture.variants.gcd`

Open: stated without proof.

An equivalent formulation in terms of the gcd of \(n!\) and \(!n\).

theorem kurepa_conjecture.variants.gcd (n : ℕ) : 2 < n → (n !).gcd (! n) = 2

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

`Kurepa.kurepa_conjecture.gcd_reduction`

Textbook result, proved here.

Kurepa's conjecture for all integers greater than 2 is equivalent to the statement that \(\gcd(n!, !n) = 2\) for all integers greater than 2.

theorem kurepa_conjecture.gcd_reduction : (∀ n, 2 < n → (!n : ℕ) % n ≠ 0)
    ↔ (∀ n, 2 < n → (n)!.gcd (!n) = 2)

Category textbook; AMS 11 Number theory. Declared in FormalConjectures/Paper/Kurepa.lean, line 103.

Sources

LeanKurepa.kurepa_conjecture · Kurepa.kurepa_conjecture.variants.prime · Kurepa.kurepa_conjecture.prime_reduction · Kurepa.kurepa_conjecture.variants.gcd · Kurepa.kurepa_conjecture.gcd_reduction

TheoremConjectures about Latin Squares #

This file formalizes some conjectures and theorems around latin squares.

References: * [Wa2011] Wanless, Ian. "Transversals in Latin Squares: A Survey." Surveys in Combinatorics 2011, R. Chapman, Ed. Cambridge University Press, 2011, pp. 403–437. https://users.monash.edu.au/~iwanless/papers/transurveyBCC.pdf * https://en.wikipedia.org/wiki/Problems_in_Latin_squares

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

`LatinSquare.oddOrderLatinSquareTransversal`

Open: stated without proof.

Conjecture 3.2 in [Wa2011]: Each Latin square of odd order has at least one transversal.

theorem oddOrderLatinSquareTransversal :
    ∀ (n : ℕ), Odd n → ∀ (L : LatinSquare n), ∃ σ, IsTransversal L σ

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

`LatinSquare.oddOrderLeq9LatinSquareTransversal`

Solved: stated here without proof.

The conjecture is known to be true for \(n \leq 9\).

theorem oddOrderLeq9LatinSquareTransversal :
    ∀ n ≤ 9, Odd n → ∀ (L : LatinSquare n), ∃ σ, IsTransversal L σ

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

`LatinSquare.latinSquareOrder11Transversal`

Open: stated without proof.

The smallest odd number for which this conjecture is not known is 11.

theorem latinSquareOrder11Transversal :
    ∀ (L : LatinSquare 11), ∃ σ, IsTransversal L σ

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

`LatinSquare.latinSquareNearTransversal`

Open: stated without proof.

Conjecture 5.1 in [Wa2011]: Every latin square has a near-transversal

theorem latinSquareNearTransversal :
    ∀ (n : ℕ) (L : LatinSquare n), ∃ ρ σ, IsNearTransversal L ρ σ

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

`LatinSquare.z_even`

Textbook result, proved here.

The Cayley table of \(\mathbb{Z}_n\) for positive even \(n\) has no transversals.

theorem z_even (n : ℕ) : z (2 * (n + 1)) = 0

Category textbook; AMS 05 Combinatorics. Declared in FormalConjectures/Paper/LatinSquare.lean, line 118.

`LatinSquare.numTransversalsZn`

Open: stated without proof.

Conjecture 6.7 in [Wa2011]: There exist real constants \(0 < c_1 < c_2 < 1\) such that

\[ c_1^n n! \leq z_n \leq c_2^n n! \]

for all odd \(n \geq 3\).

theorem numTransversalsZn :
      ∃ᵉ (c₁ > (0 : ℝ)) (c₂ < (1 : ℝ)) (_ : c₁ < c₂),
      ∀ n ≥ 3, Odd n →
        (z n : ℝ) ∈ Set.Icc (c₁ ^ n * n.factorial) (c₂ ^ n * n.factorial)

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

`LatinSquare.growthRateZn`

Open: stated without proof.

Conjecture 6.9 in [Wa2011]:

\[ \lim_{\substack{n \to \infty \\ n \text{ odd}}} \frac{1}{n} \log(z_n / n!) = -1 \]

It is not even known if this limit exists. Note that \(z_n = 0\) for even \(n\) (see z_even), so the limit must be restricted to odd \(n\); here we parametrise odd \(n\) as \(2k + 1\).

theorem growthRateZn :
    Filter.Tendsto (fun k => (1 : ℝ) / (2 * k + 1) *
      Real.log (z (2 * k + 1) / (2 * k + 1).factorial)) Filter.atTop
      (nhds (-1))

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

`LatinSquare.maxTransversalsBound`

Solved: stated here without proof.

Theorem 7.2 in [Wa2011]: For all \(n \geq 5\),

\[ 15^{n/5} \leq T(n) \leq c^n \sqrt{n} \cdot n! \]

where \(c = \sqrt{\frac{3 - \sqrt{3}}{6}} \cdot e^{\sqrt{3}/6}\)

theorem maxTransversalsBound :
    let c := Real.sqrt ((3 - Real.sqrt 3) / 6) * Real.exp (Real.sqrt 3 / 6)
    ∀ n : ℕ, n ≥ 5 →
      (T n : ℝ) ∈ Set.Icc ((15 : ℝ) ^ ((n : ℝ) / 5)) (c ^ n * Real.sqrt n * n.factorial)

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

`LatinSquare.molsExistenceProblem`

Open: stated without proof.

MOLS existence problem: determine exactly which orders n admit a complete set of n - 1 mutually orthogonal latin squares.

Equivalently, this asks for which orders affine planes of order n exist. Complete sets are known for prime-power orders; the smallest currently unresolved order is 12.

theorem molsExistenceProblem : molsExistenceProblem.answer = {n : ℕ | HasCompleteMOLS n}

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

`LatinSquare.molsOrder12`

Open: stated without proof.

The smallest unresolved case of the MOLS existence problem: whether there are 11 mutually orthogonal latin squares of order 12.

theorem molsOrder12 : HasCompleteMOLS 12

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

Sources

LeanLatinSquare.oddOrderLatinSquareTransversal · LatinSquare.oddOrderLeq9LatinSquareTransversal · LatinSquare.latinSquareOrder11Transversal · LatinSquare.latinSquareNearTransversal · LatinSquare.z_even · LatinSquare.numTransversalsZn · LatinSquare.growthRateZn · LatinSquare.maxTransversalsBound · LatinSquare.molsExistenceProblem · LatinSquare.molsOrder12

TheoremLatin Tableau Conjecture #

The Latin Tableau Conjecture states that the graph associated to any (finite) Young diagram (i.e., whose vertices are the cells of the diagram, with edges between cells in the same row or column) is CDS-colorable, meaning that there exists a proper coloring of the vertices of the graph such that for all k > 0, the number of vertices with color < k equals the maximum size of the union of k independent sets of the graph.

References:

The Latin Tableau Conjecture

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

`LatinTableau.SimpleGraph.LatinTableauConjecture`

Open: stated without proof.

The Latin Tableau Conjecture: If G is the simple graph of a Young diagram, then G is CDS-colorable.

theorem LatinTableauConjecture (μ : YoungDiagram) :
     μ.toSimpleGraph.CDSColorable

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

Sources

LeanLatinTableau.SimpleGraph.LatinTableauConjecture

TheoremLennon–Pittel conjecture on random stable matchings #

References: - On the Likely Number of Stable Marriages by Craig Lennon, PhD dissertation, The Ohio State University (2007). - On the Likely Number of Solutions for the Stable Marriage Problem by Craig Lennon and Boris Pittel, Combinatorics, Probability and Computing 18 (2009), 371–421.

Let \(S_n\) be the number of stable matchings under uniformly random complete strict preferences.

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

`LennonPittel.lennon_pittel_conjecture`

Open: stated without proof.

The Lennon–Pittel conjecture states that for every positive nonincreasing sequence \(\varepsilon_n \to 0\), the probability that the number \(S_n\) of stable matchings is at least \(\varepsilon_n \mathbb{E}[S_n]\) tends to one.

theorem lennon_pittel_conjecture
    (ε : ℕ → ℝ) (hε_pos : ∀ n, 0 < ε n) (hε_antitone : Antitone ε)
    (hε_tendsto : Tendsto ε atTop (𝓝 0)) :
    Tendsto
      (fun n ↦
        (StableMarriage.uniformProfile n).toMeasure
          {p | (StableMarriage.numStableMatchings p : ℝ) ≥
            ε n * StableMarriage.expectedNumStableMatchings n})
      atTop (𝓝 1)

Category research open; AMS 05 Combinatorics, 60 Probability theory and stochastic processes. Declared in FormalConjectures/Paper/LennonPittelStableMatchings.lean, line 53.

Sources

LeanLennonPittel.lennon_pittel_conjecture

TheoremThe Manickam–Miklós–Singhi conjecture (1988)#

References: * [MM88] Manickam, N. and Miklós, D. (1988). "On the number of nonnegative partial sums of a nonnegative sum." Colloq. Math. Soc. János Bolyai 52, pp. 385--392. * [MS88] Manickam, N. and Singhi, N. M. (1988). "First distribution invariants and EKR theorems." J. Combin. Theory Ser. A 48, pp. 91--103. * [CSS14] Chowdhury, A., Sarkis, G. and Shahriari, S. (2014). "The Manickam–Miklós–Singhi conjectures for sets and vector spaces." J. Combin. Theory Ser. A 128, pp. 84--103. arXiv:1309.2212 * [Po15] Pokrovskiy, A. (2015). "A linear bound on the Manickam–Miklós–Singhi conjecture." J. Combin. Theory Ser. A 133, pp. 280--306. arXiv:1308.2176

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

`ManickamMiklosSinghiConjecture.manickam_miklos_singhi_conjecture`

Open: stated without proof.

The Manickam–Miklós–Singhi conjecture (1988).

If \(n \ge 4k\) and \(x_1, \dots, x_n\) are real numbers with \(x_1 + \dots + x_n = 0\), then at least \(\binom{n-1}{k-1}\) of the \(k\)-element subsets \(S \subseteq \{1, \dots, n\}\) have \(\sum_{i \in S} x_i \ge 0\). (The bound is attained by \(x = (n-1, -1, \dots, -1)\); the condition \(n \ge 4k\) cannot be weakened to \(n \ge 3k + 1\) in general.)

theorem manickam_miklos_singhi_conjecture :
    ∀ (n k : ℕ), 1 ≤ k → 4 * k ≤ n → ∀ x : Fin n → ℝ, ∑ i, x i = 0 →
      (n - 1).choose (k - 1) ≤ nonnegSubsetCount n k x

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

`ManickamMiklosSinghiConjecture.manickam_miklos_singhi_conjecture.variants.pokrovskiy`

Solved: stated here without proof.

Pokrovskiy (2015): the conjecture holds for \(n \ge C k\) with an absolute constant \(C\).

Pokrovskiy proved this with \(C = 10^{46}\), the first bound linear in \(k\).

Reference: [Po15].

theorem manickam_miklos_singhi_conjecture.variants.pokrovskiy :
    ∃ C : ℕ, ∀ (n k : ℕ), 1 ≤ k → C * k ≤ n → ∀ x : Fin n → ℝ, ∑ i, x i = 0 →
      (n - 1).choose (k - 1) ≤ nonnegSubsetCount n k x

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

`ManickamMiklosSinghiConjecture.manickam_miklos_singhi_conjecture.variants.quadratic`

Solved: stated here without proof.

Chowdhury–Sarkis–Shahriari (2014): the conjecture holds for \(n \ge 8k^2\).

Reference: [CSS14].

theorem manickam_miklos_singhi_conjecture.variants.quadratic (n k : ℕ) (hk : 1 ≤ k)
    (hn : 8 * k ^ 2 ≤ n) (x : Fin n → ℝ) (hx : ∑ i, x i = 0) :
    (n - 1).choose (k - 1) ≤ nonnegSubsetCount n k x

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

Sources

LeanManickamMiklosSinghiConjecture.manickam_miklos_singhi_conjecture · ManickamMiklosSinghiConjecture.manickam_miklos_singhi_conjecture.variants.pokrovskiy · ManickamMiklosSinghiConjecture.manickam_miklos_singhi_conjecture.variants.quadratic

TheoremMonochromatic quantum graphs (inherited vertex colorings)#

MonochromaticQuantumGraph.eqSystem4_no_solution_nnreal_ge4 MonochromaticQuantumGraph.eqSystem_no_solution_nnreal_even_ge6_ge3 MonochromaticQuantumGraph.eqSystem_no_solution_even_ge4_d_eq_n_explicit MonochromaticQuantumGraph.eqSystem4_no_solution_d4 MonochromaticQuantumGraph.eqSystem4_no_solution_ge4 MonochromaticQuantumGraph.eqSystem6_no_solution_d3 MonochromaticQuantumGraph.eqSystem6_no_solution_d4 MonochromaticQuantumGraph.eqSystem6_no_solution_d5 MonochromaticQuantumGraph.eqSystem6_no_solution_d6 MonochromaticQuantumGraph.eqSystem6_no_solution_ge3 MonochromaticQuantumGraph.eqSystem8_no_solution_d3 MonochromaticQuantumGraph.eqSystem8_no_solution_d10 MonochromaticQuantumGraph.eqSystem10_no_solution_d3 MonochromaticQuantumGraph.eqSystem10_no_solution_d4 MonochromaticQuantumGraph.eqSystem10_no_solution_d5 MonochromaticQuantumGraph.eqSystem10_no_solution_d6 MonochromaticQuantumGraph.eqSystem10_no_solution_d7 MonochromaticQuantumGraph.eqSystem10_no_solution_d8 MonochromaticQuantumGraph.eqSystem10_no_solution_d9 MonochromaticQuantumGraph.eqSystem10_no_solution_d10 MonochromaticQuantumGraph.eqSystem12_no_solution_d3 MonochromaticQuantumGraph.eqSystem14_no_solution_d3 MonochromaticQuantumGraph.eqSystem16_no_solution_d3 MonochromaticQuantumGraph.eqSystem_no_solution_ge6_ge3 MonochromaticQuantumGraph.eqSystem4_no_solution_ge4_real MonochromaticQuantumGraph.eqSystem6_no_solution_d3_real MonochromaticQuantumGraph.eqSystem6_no_solution_d5_real MonochromaticQuantumGraph.eqSystem6_no_solution_ge3_real MonochromaticQuantumGraph.eqSystem8_no_solution_d3_real MonochromaticQuantumGraph.eqSystem10_no_solution_d3_real MonochromaticQuantumGraph.eqSystem_no_solution_ge6_ge3_real MonochromaticQuantumGraph.eqSystem4_no_solution_ge4_int MonochromaticQuantumGraph.eqSystem6_no_solution_d3_int MonochromaticQuantumGraph.eqSystem6_no_solution_d5_int MonochromaticQuantumGraph.eqSystem6_no_solution_ge3_int MonochromaticQuantumGraph.eqSystem8_no_solution_d3_int MonochromaticQuantumGraph.eqSystem10_no_solution_d3_int MonochromaticQuantumGraph.eqSystem_no_solution_ge6_ge3_int MonochromaticQuantumGraph.eqSystem4_no_solution_ge4_trinary_int MonochromaticQuantumGraph.eqSystem6_no_solution_d3_trinary_int MonochromaticQuantumGraph.eqSystem6_no_solution_d5_trinary_int MonochromaticQuantumGraph.eqSystem6_no_solution_ge3_trinary_int MonochromaticQuantumGraph.eqSystem8_no_solution_d3_trinary_int MonochromaticQuantumGraph.eqSystem10_no_solution_d3_trinary_int MonochromaticQuantumGraph.eqSystem_no_solution_ge6_ge3_trinary_int

This file studies the existence of monochromatic quantum graphs: edge-coloured, edge-weighted complete graphs whose perfect matchings induce vertex colourings, with the property that

every non-monochromatic inherited vertex colouring has total weight 0, while

each of the D monochromatic colourings has total weight 1.

In the quantum-optics motivation, such a construction corresponds to generating high-dimensional multipartite GHZ-type states using probabilistic pair sources and linear optics (without additional resources), where interference patterns can be expressed as weighted sums over perfect matchings.

Main questions (informal)

For N = 4 and D ≥ 4, does there exist such a graph/weighting?

For even N ≥ 6 and D ≥ 3, does there exist such a graph/weighting?

Formalisation sketch

A quantum graph with N vertices and D colours can be encoded by a weight function W : EdgeN N D α → α (for a coefficient domain α).

For each assignment of vertex indices ι : V N → Fin D, we define a perfect-matching sum pmSumN N D W ι (a sum over perfect matchings, where each matching contributes the product of the corresponding edge weights determined by ι). The equation system EqSystemN N D W requires

pmSumN N D W ι = 1 iff ι is constant (all entries equal), and 0 otherwise.

The open conjectures in this file ask for non-existence/existence of such W over various coefficient domains (e.g. ℂ, ℝ, ℤ, and restricted integer weights).

References

[Krenn2017] M. Krenn, X. Gu, A. Zeilinger, "Quantum Experiments and Graphs: Multiparty States as Coherent Superpositions of Perfect Matchings", Physical Review Letters 119(24), 240403 (2017).

[MO2018] Vertex coloring inherited from perfect matchings (motivated by quantum physics), MathOverflow question 311325.

[Gu2019] X. Gu, M. Erhard, A. Zeilinger, M. Krenn, "Quantum experiments and graphs II: Quantum interference, computation, and state generation", PNAS 116(10), 4147–4155 (2019).

[Krenn2019] Questions on the Structure of Perfect Matchings inspired by Quantum Physics by M. Krenn, X. Gu, U. Soltész, Proc. 2nd Croatian Combinatorial Days, 57–70 (2019).

[Chandran2022] Edge-coloured graphs with only monochromatic perfect matchings and their connection to quantum physics by N. Chandran, S. Gajjala (2022).

[Chandran2024] Krenn–Gu conjecture for sparse graphs by N. Chandran, S. Gajjala, S. Illickan, M. Krenn, MFCS 2024.

[Ki26] A solver-free Lean 4 proof of the sharp bound \(D \le N - 2\) for monochromatic quantum graph equation systems over integral domains, commit 6c534038.

[Ki26b] A solver-free Lean 4 proof that the monochromatic quantum graph equation system has no solution for \(N = 10\) and \(D = 8\) over integral domains, commit a9309005.

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

The file states 45 research or textbook statements: 16 open and 29 solved. It also has 3 test statements, counted here but not shown.

`MonochromaticQuantumGraph.eqSystem4_no_solution_nnreal_ge4`

Solved: stated here without proof.

Bogdanov: for \(N = 4\) and all \(D \geq 4\), no solution exists over \(\mathbb{R}_{\geq 0}\).

theorem eqSystem4_no_solution_nnreal_ge4 :
    ∀ D : Nat, D ≥ 4 →
      ¬ ∃ W : WeightsN 4 D ℝ≥0, EqSystemN 4 D W

Category research solved; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 346.

`MonochromaticQuantumGraph.eqSystem_no_solution_nnreal_even_ge6_ge3`

Solved: stated here without proof.

Bogdanov: for all even \(N \geq 6\) and \(D \geq 3\), no solution exists over \(\mathbb{R}_{\geq 0}\).

theorem eqSystem_no_solution_nnreal_even_ge6_ge3 :
    ∀ N D : Nat,
      N ≥ 6 → Even N → D ≥ 3 →
        ¬ ∃ W : WeightsN N D ℝ≥0, EqSystemN N D W

Category research solved; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 353.

`MonochromaticQuantumGraph.eqSystem_no_solution_even_ge4_d_eq_n_explicit`

Solved: stated here; a Lean proof is at https://github.com/google-deepmind/formal-conjectures/blob/af88acbf9da0f26e3e934743a819e986e02f6875/FormalConjectures/Paper/MonochromaticQuantumGraph.lean#L1006.

For all even \(N \geq 4\) and \(D = N\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{C}\)?

The DeepMind prover agent has found a formal proof for this statement.

theorem eqSystem_no_solution_even_ge4_d_eq_n_explicit :
    ∀ N : Nat, N ≥ 4 → Even N →
      ¬ ∃ W : WeightsN N N ℂ, EqSystemN N N W

Category research solved; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 383.

`MonochromaticQuantumGraph.eqSystem4_no_solution_d4`

Solved: stated here; a Lean proof is at https://github.com/google-deepmind/formal-conjectures/blob/af88acbf9da0f26e3e934743a819e986e02f6875/FormalConjectures/Paper/MonochromaticQuantumGraph.lean#L1021.

For \(N = 4\) and \(D = 4\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{C}\)?

This is the \(D = N\) case, proved using eqSystem_no_solution_even_ge4_d_eq_n_explicit.

theorem eqSystem4_no_solution_d4 :
    ¬ ∃ W : WeightsN 4 4 ℂ, EqSystemN 4 4 W

Category research solved; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 395.

`MonochromaticQuantumGraph.eqSystem4_no_solution_ge4`

Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/4854c7233c58a7dce45fdd58b1826abf2c9c1a0f/FormalConjectures/Paper/MonochromaticQuantumGraph.lean#L549.

For \(N = 4\) and all \(D \geq 4\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{C}\)?

The DeepMind prover agent has found a formal proof of this statement.

theorem eqSystem4_no_solution_ge4 :
    ∀ D : Nat, D ≥ 4 →
      ¬ ∃ W : WeightsN 4 D ℂ, EqSystemN 4 D W

Category research solved; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 408.

`MonochromaticQuantumGraph.eqSystem6_no_solution_d3`

Solved: stated here; a Lean proof is at https://github.com/algal/krenn-gu-6x3-certificate/blob/c04696e515e0c02be140353fb52ea60c62e827b1/KrennGuCertificate/Unrestricted.lean#L201-L222.

For \(N = 6\) and \(D = 3\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{C}\)?

A complete Lean 4 proof is available in the linked external certificate repository.

theorem eqSystem6_no_solution_d3 :
    ¬ ∃ W : WeightsN 6 3 ℂ, EqSystemN 6 3 W

Category research solved; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 422.

`MonochromaticQuantumGraph.eqSystem6_no_solution_d4`

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/monochromatic-quantum-graph-n6-d4-lean/blob/7d30141a19714986d6f9e632314fd880c9a1e86e/lean/QuantumCR/FormalConjecturesWrapper.lean#L30-L37.

For \(N = 6\) and \(D = 4\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{C}\)?

theorem eqSystem6_no_solution_d4 :
    ¬ ∃ W : WeightsN 6 4 ℂ, EqSystemN 6 4 W

Category research solved; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 433.

`MonochromaticQuantumGraph.eqSystem6_no_solution_d5`

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/monochromatic-quantum-graph-sharp-bound-lean/blob/6c5340384479dbb36129b2e0084449be2458cce2/lean/QuantumCR/FormalConjecturesWrappers.lean#L55-L62.

For \(N = 6\) and \(D = 5\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{C}\)?

The sharp bound \(D \le N - 2\) over an integral domain [Ki26] settles this: here \(D = N - 1\).

theorem eqSystem6_no_solution_d5 :
    ¬ ∃ W : WeightsN 6 5 ℂ, EqSystemN 6 5 W

Category research solved; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 445.

`MonochromaticQuantumGraph.eqSystem6_no_solution_d6`

Solved: stated here; a Lean proof is at https://github.com/google-deepmind/formal-conjectures/blob/af88acbf9da0f26e3e934743a819e986e02f6875/FormalConjectures/Paper/MonochromaticQuantumGraph.lean#L1074.

For \(N = 6\) and \(D = 6\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{C}\)?

This follows from eqSystem_no_solution_even_ge4_d_eq_n_explicit.

theorem eqSystem6_no_solution_d6 :
    ¬ ∃ W : WeightsN 6 6 ℂ, EqSystemN 6 6 W

Category research solved; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 457.

`MonochromaticQuantumGraph.eqSystem6_no_solution_ge3`

Open: stated without proof.

For \(N = 6\) and all \(D \geq 3\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{C}\)?

theorem eqSystem6_no_solution_ge3 :
    ∀ D : Nat, D ≥ 3 →
      ¬ ∃ W : WeightsN 6 D ℂ, EqSystemN 6 D W

Category research open; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 464.

`MonochromaticQuantumGraph.eqSystem8_no_solution_d3`

Open: stated without proof.

For \(N = 8\) and \(D = 3\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{C}\)?

theorem eqSystem8_no_solution_d3 :
    ¬ ∃ W : WeightsN 8 3 ℂ, EqSystemN 8 3 W

Category research open; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 472.

`MonochromaticQuantumGraph.eqSystem8_no_solution_d10`

Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/2cc6df2e95835d759caedb15e36b70025b2eae2c/FormalConjectures/Paper/MonochromaticQuantumGraph.lean#L853.

For \(N = 8\) and \(D = 10\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{C}\)?

The DeepMind prover agent has found a formal proof of this statement.

theorem eqSystem8_no_solution_d10 :
    ¬ ∃ W : WeightsN 8 10 ℂ, EqSystemN 8 10 W

Category research solved; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 484.

`MonochromaticQuantumGraph.eqSystem10_no_solution_d3`

Open: stated without proof.

For \(N = 10\) and \(D = 3\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{C}\)?

theorem eqSystem10_no_solution_d3 :
    ¬ ∃ W : WeightsN 10 3 ℂ, EqSystemN 10 3 W

Category research open; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 491.

`MonochromaticQuantumGraph.eqSystem10_no_solution_d4`

Open: stated without proof.

For \(N = 10\) and \(D = 4\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{C}\)?

theorem eqSystem10_no_solution_d4 :
    ¬ ∃ W : WeightsN 10 4 ℂ, EqSystemN 10 4 W

Category research open; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 498.

`MonochromaticQuantumGraph.eqSystem10_no_solution_d5`

Open: stated without proof.

For \(N = 10\) and \(D = 5\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{C}\)?

theorem eqSystem10_no_solution_d5 :
    ¬ ∃ W : WeightsN 10 5 ℂ, EqSystemN 10 5 W

Category research open; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 505.

`MonochromaticQuantumGraph.eqSystem10_no_solution_d6`

Open: stated without proof.

For \(N = 10\) and \(D = 6\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{C}\)?

theorem eqSystem10_no_solution_d6 :
    ¬ ∃ W : WeightsN 10 6 ℂ, EqSystemN 10 6 W

Category research open; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 512.

`MonochromaticQuantumGraph.eqSystem10_no_solution_d7`

Open: stated without proof.

For \(N = 10\) and \(D = 7\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{C}\)?

theorem eqSystem10_no_solution_d7 :
    ¬ ∃ W : WeightsN 10 7 ℂ, EqSystemN 10 7 W

Category research open; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 519.

`MonochromaticQuantumGraph.eqSystem10_no_solution_d8`

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/monochromatic-quantum-graph-n10-d8-lean/blob/a9309005c7a27a2615f8e7eebef7a1db017809ab/lean/QuantumGraphTenEightFC.lean#L5466-L5473.

For \(N = 10\) and \(D = 8\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{C}\)?

The sharp bound \(D \le N - 2\) of [Ki26] does not cover this equality case \(D = N - 2\); it is settled over an integral domain in [Ki26b].

theorem eqSystem10_no_solution_d8 :
    ¬ ∃ W : WeightsN 10 8 ℂ, EqSystemN 10 8 W

Category research solved; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 532.

`MonochromaticQuantumGraph.eqSystem10_no_solution_d9`

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/monochromatic-quantum-graph-sharp-bound-lean/blob/6c5340384479dbb36129b2e0084449be2458cce2/lean/QuantumCR/FormalConjecturesWrappers.lean#L73-L80.

For \(N = 10\) and \(D = 9\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{C}\)?

The sharp bound \(D \le N - 2\) over an integral domain [Ki26] settles this: here \(D = N - 1\).

theorem eqSystem10_no_solution_d9 :
    ¬ ∃ W : WeightsN 10 9 ℂ, EqSystemN 10 9 W

Category research solved; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 543.

`MonochromaticQuantumGraph.eqSystem10_no_solution_d10`

Solved: stated here; a Lean proof is at https://github.com/google-deepmind/formal-conjectures/blob/af88acbf9da0f26e3e934743a819e986e02f6875/FormalConjectures/Paper/MonochromaticQuantumGraph.lean#L1167.

For \(N = 10\) and \(D = 10\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{C}\)?

This follows from the \(D = N\) case, see eqSystem_no_solution_even_ge4_d_eq_n_explicit.

theorem eqSystem10_no_solution_d10 :
    ¬ ∃ W : WeightsN 10 10 ℂ, EqSystemN 10 10 W

Category research solved; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 554.

`MonochromaticQuantumGraph.eqSystem12_no_solution_d3`

Open: stated without proof.

For \(N = 12\) and \(D = 3\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{C}\)?

theorem eqSystem12_no_solution_d3 :
    ¬ ∃ W : WeightsN 12 3 ℂ, EqSystemN 12 3 W

Category research open; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 561.

`MonochromaticQuantumGraph.eqSystem14_no_solution_d3`

Open: stated without proof.

For \(N = 14\) and \(D = 3\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{C}\)?

theorem eqSystem14_no_solution_d3 :
    ¬ ∃ W : WeightsN 14 3 ℂ, EqSystemN 14 3 W

Category research open; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 568.

`MonochromaticQuantumGraph.eqSystem16_no_solution_d3`

Open: stated without proof.

For \(N = 16\) and \(D = 3\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{C}\)?

theorem eqSystem16_no_solution_d3 :
    ¬ ∃ W : WeightsN 16 3 ℂ, EqSystemN 16 3 W

Category research open; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 575.

`MonochromaticQuantumGraph.eqSystem_no_solution_ge6_ge3`

Open: stated without proof.

For all even \(N \geq 6\) and \(D \geq 3\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{C}\)?

theorem eqSystem_no_solution_ge6_ge3 :
    ∀ N D : Nat, N ≥ 6 → Even N → D ≥ 3 →
      ¬ ∃ W : WeightsN N D ℂ, EqSystemN N D W

Category research open; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 584.

`MonochromaticQuantumGraph.eqSystem4_no_solution_ge4_real`

Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/4854c7233c58a7dce45fdd58b1826abf2c9c1a0f/FormalConjectures/Paper/MonochromaticQuantumGraph.lean#L738.

For \(N = 4\) and all \(D \geq 4\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{R}\)?

This follows from the solution of the complex version of the problem (see eqSystem4_no_solution_ge4)

theorem eqSystem4_no_solution_ge4_real :
    ∀ D : Nat, D ≥ 4 →
      ¬ ∃ W : WeightsN 4 D ℝ, EqSystemN 4 D W

Category research solved; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 601.

`MonochromaticQuantumGraph.eqSystem6_no_solution_d3_real`

Open: stated without proof.

For \(N = 6\) and \(D = 3\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{R}\)?

theorem eqSystem6_no_solution_d3_real :
    ¬ ∃ W : WeightsN 6 3 ℝ, EqSystemN 6 3 W

Category research open; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 609.

`MonochromaticQuantumGraph.eqSystem6_no_solution_d5_real`

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/monochromatic-quantum-graph-sharp-bound-lean/blob/6c5340384479dbb36129b2e0084449be2458cce2/lean/QuantumCR/FormalConjecturesWrappers.lean#L64-L71.

For \(N = 6\) and \(D = 5\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{R}\)?

The sharp bound \(D \le N - 2\) over an integral domain [Ki26] settles this: here \(D = N - 1\).

theorem eqSystem6_no_solution_d5_real :
    ¬ ∃ W : WeightsN 6 5 ℝ, EqSystemN 6 5 W

Category research solved; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 620.

`MonochromaticQuantumGraph.eqSystem6_no_solution_ge3_real`

Open: stated without proof.

For \(N = 6\) and all \(D \geq 3\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{R}\)?

theorem eqSystem6_no_solution_ge3_real :
    ∀ D : Nat, D ≥ 3 →
      ¬ ∃ W : WeightsN 6 D ℝ, EqSystemN 6 D W

Category research open; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 627.

`MonochromaticQuantumGraph.eqSystem8_no_solution_d3_real`

Open: stated without proof.

For \(N = 8\) and \(D = 3\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{R}\)?

theorem eqSystem8_no_solution_d3_real :
    ¬ ∃ W : WeightsN 8 3 ℝ, EqSystemN 8 3 W

Category research open; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 635.

`MonochromaticQuantumGraph.eqSystem10_no_solution_d3_real`

Open: stated without proof.

For \(N = 10\) and \(D = 3\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{R}\)?

theorem eqSystem10_no_solution_d3_real :
    ¬ ∃ W : WeightsN 10 3 ℝ, EqSystemN 10 3 W

Category research open; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 644.

`MonochromaticQuantumGraph.eqSystem_no_solution_ge6_ge3_real`

Open: stated without proof.

For all even \(N \geq 6\) and \(D \geq 3\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{R}\)?

theorem eqSystem_no_solution_ge6_ge3_real :
    ∀ N D : Nat, N ≥ 6 → Even N → D ≥ 3 →
      ¬ ∃ W : WeightsN N D ℝ, EqSystemN N D W

Category research open; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 651.

`MonochromaticQuantumGraph.eqSystem4_no_solution_ge4_int`

Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/4854c7233c58a7dce45fdd58b1826abf2c9c1a0f/FormalConjectures/Paper/MonochromaticQuantumGraph.lean#L836.

For \(N = 4\) and all \(D \geq 4\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{Z}\)?

This follows from the solution of the complex version of the problem (see eqSystem4_no_solution_ge4).

theorem eqSystem4_no_solution_ge4_int :
    ∀ D : Nat, D ≥ 4 →
      ¬ ∃ W : WeightsN 4 D ℤ, EqSystemN 4 D W

Category research solved; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 667.

`MonochromaticQuantumGraph.eqSystem6_no_solution_d3_int`

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/monochromatic-quantum-graphs-lean/blob/d3ed1892ef181f5f5f5d61d9b5817f05b53a6675/lean/QuantumLean/FormalConjecturesWrappers.lean#L32-L39.

For \(N = 6\) and \(D = 3\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{Z}\)?

theorem eqSystem6_no_solution_d3_int :
    ¬ ∃ W : WeightsN 6 3 ℤ, EqSystemN 6 3 W

Category research solved; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 678.

`MonochromaticQuantumGraph.eqSystem6_no_solution_d5_int`

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/monochromatic-quantum-graphs-lean/blob/d3ed1892ef181f5f5f5d61d9b5817f05b53a6675/lean/QuantumLean/FormalConjecturesWrappers.lean#L41-L48.

For \(N = 6\) and \(D = 5\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{Z}\)?

theorem eqSystem6_no_solution_d5_int :
    ¬ ∃ W : WeightsN 6 5 ℤ, EqSystemN 6 5 W

Category research solved; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 688.

`MonochromaticQuantumGraph.eqSystem6_no_solution_ge3_int`

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/monochromatic-quantum-graphs-lean/blob/d3ed1892ef181f5f5f5d61d9b5817f05b53a6675/lean/QuantumLean/FormalConjecturesWrappers.lean#L50-L58.

For \(N = 6\) and all \(D \geq 3\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{Z}\)?

theorem eqSystem6_no_solution_ge3_int :
    ∀ D : Nat, D ≥ 3 →
      ¬ ∃ W : WeightsN 6 D ℤ, EqSystemN 6 D W

Category research solved; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 698.

`MonochromaticQuantumGraph.eqSystem8_no_solution_d3_int`

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/monochromatic-quantum-graphs-lean/blob/d3ed1892ef181f5f5f5d61d9b5817f05b53a6675/lean/QuantumLean/FormalConjecturesWrappers.lean#L60-L67.

For \(N = 8\) and \(D = 3\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{Z}\)?

theorem eqSystem8_no_solution_d3_int :
    ¬ ∃ W : WeightsN 8 3 ℤ, EqSystemN 8 3 W

Category research solved; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 709.

`MonochromaticQuantumGraph.eqSystem10_no_solution_d3_int`

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/monochromatic-quantum-graphs-lean/blob/d3ed1892ef181f5f5f5d61d9b5817f05b53a6675/lean/QuantumLean/FormalConjecturesWrappers.lean#L69-L76.

For \(N = 10\) and \(D = 3\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{Z}\)?

theorem eqSystem10_no_solution_d3_int :
    ¬ ∃ W : WeightsN 10 3 ℤ, EqSystemN 10 3 W

Category research solved; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 720.

`MonochromaticQuantumGraph.eqSystem_no_solution_ge6_ge3_int`

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/monochromatic-quantum-graphs-lean/blob/d3ed1892ef181f5f5f5d61d9b5817f05b53a6675/lean/QuantumLean/FormalConjecturesWrappers.lean#L78-L86.

For all even \(N \geq 6\) and \(D \geq 3\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{Z}\)?

theorem eqSystem_no_solution_ge6_ge3_int :
    ∀ N D : Nat, N ≥ 6 → Even N → D ≥ 3 →
      ¬ ∃ W : WeightsN N D ℤ, EqSystemN N D W

Category research solved; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 730.

`MonochromaticQuantumGraph.eqSystem4_no_solution_ge4_trinary_int`

Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/4854c7233c58a7dce45fdd58b1826abf2c9c1a0f/FormalConjectures/Paper/MonochromaticQuantumGraph.lean#L936.

For \(N = 4\) and all \(D \geq 4\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{Z}\) with weights in \(\{-1, 0, 1\}\)?

This follows from the complex version, see eqSystem4_no_solution_ge4.

theorem eqSystem4_no_solution_ge4_trinary_int :
    ∀ D : Nat, D ≥ 4 →
      ¬ ∃ W : WeightsN 4 D ℤ,
          (∀ e, W e = (-1 : ℤ) ∨ W e = 0 ∨ W e = 1) ∧
            EqSystemN 4 D W

Category research solved; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 746.

`MonochromaticQuantumGraph.eqSystem6_no_solution_d3_trinary_int`

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/monochromatic-quantum-graphs-lean/blob/d3ed1892ef181f5f5f5d61d9b5817f05b53a6675/lean/QuantumLean/FormalConjecturesWrappers.lean#L88-L97.

For \(N = 6\) and \(D = 3\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{Z}\) with weights in \(\{-1, 0, 1\}\)?

theorem eqSystem6_no_solution_d3_trinary_int :
    ¬ ∃ W : WeightsN 6 3 ℤ,
        (∀ e, W e = (-1 : ℤ) ∨ W e = 0 ∨ W e = 1) ∧
          EqSystemN 6 3 W

Category research solved; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 759.

`MonochromaticQuantumGraph.eqSystem6_no_solution_d5_trinary_int`

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/monochromatic-quantum-graphs-lean/blob/d3ed1892ef181f5f5f5d61d9b5817f05b53a6675/lean/QuantumLean/FormalConjecturesWrappers.lean#L99-L108.

For \(N = 6\) and \(D = 5\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{Z}\) with weights in \(\{-1, 0, 1\}\)?

theorem eqSystem6_no_solution_d5_trinary_int :
    ¬ ∃ W : WeightsN 6 5 ℤ,
        (∀ e, W e = (-1 : ℤ) ∨ W e = 0 ∨ W e = 1) ∧
          EqSystemN 6 5 W

Category research solved; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 771.

`MonochromaticQuantumGraph.eqSystem6_no_solution_ge3_trinary_int`

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/monochromatic-quantum-graphs-lean/blob/d3ed1892ef181f5f5f5d61d9b5817f05b53a6675/lean/QuantumLean/FormalConjecturesWrappers.lean#L110-L120.

For \(N = 6\) and all \(D \geq 3\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{Z}\) with weights in \(\{-1, 0, 1\}\)?

theorem eqSystem6_no_solution_ge3_trinary_int :
    ∀ D : Nat, D ≥ 3 →
      ¬ ∃ W : WeightsN 6 D ℤ,
          (∀ e, W e = (-1 : ℤ) ∨ W e = 0 ∨ W e = 1) ∧
            EqSystemN 6 D W

Category research solved; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 783.

`MonochromaticQuantumGraph.eqSystem8_no_solution_d3_trinary_int`

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/monochromatic-quantum-graphs-lean/blob/d3ed1892ef181f5f5f5d61d9b5817f05b53a6675/lean/QuantumLean/FormalConjecturesWrappers.lean#L122-L131.

For \(N = 8\) and \(D = 3\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{Z}\) with weights in \(\{-1, 0, 1\}\)?

theorem eqSystem8_no_solution_d3_trinary_int :
    ¬ ∃ W : WeightsN 8 3 ℤ,
        (∀ e, W e = (-1 : ℤ) ∨ W e = 0 ∨ W e = 1) ∧
          EqSystemN 8 3 W

Category research solved; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 796.

`MonochromaticQuantumGraph.eqSystem10_no_solution_d3_trinary_int`

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/monochromatic-quantum-graphs-lean/blob/d3ed1892ef181f5f5f5d61d9b5817f05b53a6675/lean/QuantumLean/FormalConjecturesWrappers.lean#L133-L142.

For \(N = 10\) and \(D = 3\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{Z}\) with weights in \(\{-1, 0, 1\}\)?

theorem eqSystem10_no_solution_d3_trinary_int :
    ¬ ∃ W : WeightsN 10 3 ℤ,
        (∀ e, W e = (-1 : ℤ) ∨ W e = 0 ∨ W e = 1) ∧
          EqSystemN 10 3 W

Category research solved; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 809.

`MonochromaticQuantumGraph.eqSystem_no_solution_ge6_ge3_trinary_int`

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/monochromatic-quantum-graphs-lean/blob/d3ed1892ef181f5f5f5d61d9b5817f05b53a6675/lean/QuantumLean/FormalConjecturesWrappers.lean#L144-L154.

For all even \(N \geq 6\) and \(D \geq 3\), does there exist no solution to the monochromatic quantum graph equation system over \(\mathbb{Z}\) with weights in \(\{-1, 0, 1\}\)?

theorem eqSystem_no_solution_ge6_ge3_trinary_int :
    ∀ N D : Nat, N ≥ 6 → Even N → D ≥ 3 →
      ¬ ∃ W : WeightsN N D ℤ,
          (∀ e, W e = (-1 : ℤ) ∨ W e = 0 ∨ W e = 1) ∧
            EqSystemN N D W

Category research solved; AMS 05 Combinatorics, 14 Algebraic geometry, 81 Quantum theory. Declared in FormalConjectures/Paper/MonochromaticQuantumGraph.lean, line 821.

Sources

TheoremEnergy-critical NLS in three dimensions.#

This file states an a priori estimate for the energy-critical nonlinear Schrödinger equation on \(ℝ^3\). By 'soft' arguments, this bound implies global well-posedness in the energy space, scattering, asymptotic completeness, and uniform regularity (all of which are less elementary to state). This is remarked on p. 770 and p. 793 in the referenced article which first proved the a priori bound.

The main theorem is: - NLS_apriori: a bound on the space-time \(L^10\) norm in terms of the initial energy for local smooth solutions to the NLS equation.

References

Colliander, Keel, Staffilani, Takaoka, Tao, Annals of Mathematics 167 (2008) proves the a priori estimate, and thereby, global well-posedness.

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

`NLSCritical.NLS_apriori`

Solved: stated here without proof.

The \(L^10_{t,x}\) a priori estimate for local schwartz solutions.

theorem NLS_apriori :
    ∃ f : ℝ → ℝ, ∀ l > 0, ∀ s : LocalSchwartzSolution l,
    L10_local l s.u ≤ f (energy (s.u 0))

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

Sources

LeanNLSCritical.NLS_apriori

TheoremThe 1-2-3 conjecture (Karoński–Łuczak–Thomason 2004; proved by Keusch 2024)#

References: * [KLT04] Karoński, M., Łuczak, T. and Thomason, A. (2004). "Edge weights and vertex colours." J. Combin. Theory Ser. B 91, pp. 151--157. * [ABDMRT07] Addario-Berry, L., Dalal, K., McDiarmid, C., Reed, B. A. and Thomason, A. (2007). "Vertex-colouring edge-weightings." Combinatorica 27, pp. 1--12. * [KKP10] Kalkowski, M., Karoński, M. and Pfender, F. (2010). "Vertex-coloring edge-weightings: towards the 1-2-3-conjecture." J. Combin. Theory Ser. B 100, pp. 347--349. * [Ke24] Keusch, R. (2024). "A solution to the 1-2-3 conjecture." J. Combin. Theory Ser. B 166, pp. 183--202. arXiv:2303.02611

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

`OneTwoThreeConjecture.one_two_three_conjecture`

Solved: stated here without proof.

The 1-2-3 conjecture (Karoński–Łuczak–Thomason 2004), proved by Keusch (2024).

Every finite simple graph with no isolated edge admits an edge weighting with weights in \(\{1, 2, 3\}\) such that adjacent vertices have different weighted degrees.

theorem one_two_three_conjecture :
    ∀ {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj],
      NoIsolatedEdge G →
      ∃ w : Sym2 V → ℕ, (∀ e ∈ G.edgeFinset, 1 ≤ w e ∧ w e ≤ 3) ∧
        IsVertexColouringWeighting G w

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

`OneTwoThreeConjecture.one_two_three_conjecture.variants.one_to_five`

Solved: stated here without proof.

Kalkowski–Karoński–Pfender (2010): weights in \(\{1, \dots, 5\}\) suffice.

Reference: [KKP10].

theorem one_two_three_conjecture.variants.one_to_five
    {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj]
    (hG : NoIsolatedEdge G) :
    ∃ w : Sym2 V → ℕ, (∀ e ∈ G.edgeFinset, 1 ≤ w e ∧ w e ≤ 5) ∧
      IsVertexColouringWeighting G w

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

`OneTwoThreeConjecture.one_two_three_conjecture.variants.one_to_thirty`

Solved: stated here without proof.

Addario-Berry–Dalal–McDiarmid–Reed–Thomason (2007): weights in \(\{1, \dots, 30\}\) suffice.

Reference: [ABDMRT07]; see also the introduction of [KKP10].

theorem one_two_three_conjecture.variants.one_to_thirty
    {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj]
    (hG : NoIsolatedEdge G) :
    ∃ w : Sym2 V → ℕ, (∀ e ∈ G.edgeFinset, 1 ≤ w e ∧ w e ≤ 30) ∧
      IsVertexColouringWeighting G w

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

`OneTwoThreeConjecture.one_two_three_conjecture.variants.isolated_edge_necessary`

Proved here.

The hypothesis "no isolated edge" is necessary.

A single edge K₂ has no vertex-colouring edge weighting at all: both endpoints receive the weight of the unique edge as their weighted degree.

theorem one_two_three_conjecture.variants.isolated_edge_necessary :
    ¬ ∃ w : Sym2 (Fin 2) → ℕ, IsVertexColouringWeighting (completeGraph (Fin 2)) w

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

`OneTwoThreeConjecture.one_two_three_conjecture.variants.two_weights_insufficient`

Proved here.

Weights \(\{1, 2\}\) do not suffice: the triangle.

In K₃ the three vertex sums are a + b, a + c, b + c for the three edge weights a, b, c, and they are pairwise distinct only if a, b, c are, which is impossible with two available weights. Hence the constant 3 in the conjecture cannot be lowered to 2.

theorem one_two_three_conjecture.variants.two_weights_insufficient :
    ¬ ∃ w : Sym2 (Fin 3) → ℕ, (∀ e ∈ (completeGraph (Fin 3)).edgeFinset, 1 ≤ w e ∧ w e ≤ 2) ∧
      IsVertexColouringWeighting (completeGraph (Fin 3)) w

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

Sources

LeanOneTwoThreeConjecture.one_two_three_conjecture · OneTwoThreeConjecture.one_two_three_conjecture.variants.one_to_five · OneTwoThreeConjecture.one_two_three_conjecture.variants.one_to_thirty · OneTwoThreeConjecture.one_two_three_conjecture.variants.isolated_edge_necessary · OneTwoThreeConjecture.one_two_three_conjecture.variants.two_weights_insufficient

TheoremParities of partition numbers #

There are several conjectures on parities of partition numbers. The most famous conjecture is the Parkin-Shanks conjecture, which states that the natural density of n where the partition number p(n) is even (resp. odd) exists and equals 1/2.

There are several related (weaker) results toward the conjecture. Kolberg showed that p(n) takes each parity infinitely often. Subbarao conjectured that every arithmetic progression r (mod t) contains infinitely many n with p(n) even and infinitely many n with p(n) odd; the even case was proved by Ono and the odd case by Radu. Quantitative lower bounds for the number of n ≤ X with p(n) even (resp. odd) have also been studied. The best known bounds are ≫ √X log log X for even values (Bellaïche–Nicolas) and ≫ √X for odd values (Zheng, in an appendix to Ono–Swaminathan). Ono–Swaminathan also proved that both parities occur infinitely often along the quadratic progressions (D m² + 1) / 24, and Ono conjectured the same for every nonconstant integer-valued polynomial that is eventually positive.

References: * On the distribution of parity in the partition function, T. R. Parkin, D. Shanks, Math. Comp. 21 (1967), 466–480. * Note on the parity of the partition function, O. Kolberg, Math. Scand. 7 (1959), 377–378. * Some remarks on the partition function, M. V. Subbarao, Amer. Math. Monthly 73 (1966), 851–854. * Parity of the partition function in arithmetic progressions, K. Ono, J. Reine Angew. Math. 472 (1996), 1–16. * Distribution of parity of the partition function in arithmetic progressions, S. Ahlgren, Indag. Math. (N.S.) 10 (1999), 173–181. * Parity of the partition function, K. Ono, Adv. Math. 225 (2010), 349–366. * A proof of Subbarao's conjecture, C.-S. Radu, J. Reine Angew. Math. 672 (2012), 161–175. * Parité des coefficients de formes modulaires, J. Bellaïche, J.-L. Nicolas, Ramanujan J. 40 (2016), 1–44. * Nonzero coefficients of half-integral weight modular forms mod ℓ, J. Bellaïche, B. Green, K. Soundararajan, Res. Math. Sci. 5 (2018), Paper No. 6. * Parity of the partition function in quadratic progressions (with an appendix by Q.-Y. Zheng), K. Ono, A. Swaminathan, arXiv:2509.09553. * [Cox] D. A. Cox, Primes of the Form \(x^2 + ny^2\), 2nd ed., Wiley, 2013.

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

The file states 16 research or textbook statements: 2 open, 13 solved and 1 textbook result.

`PartitionParity.kolberg`

Solved: stated here without proof.

p(n) is even for infinitely many n and odd for infinitely many n. (Kolberg)

theorem kolberg :
    {n : ℕ | Even (partitionNumber n)}.Infinite ∧ {n : ℕ | Odd (partitionNumber n)}.Infinite

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

`PartitionParity.parkin_shanks`

Open: stated without proof.

The natural density of n where the partition number p(n) is even (resp. odd) exists and equals 1/2.

theorem parkin_shanks :
    {n : ℕ | Even (partitionNumber n)}.HasDensity (1 / 2) ∧
    {n : ℕ | Odd (partitionNumber n)}.HasDensity (1 / 2)

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

`PartitionParity.subbarao.even`

Solved: stated here without proof.

Every arithmetic progression contains infinitely many n where p(n) is even. Conjectured by Subbarao and proved by Ono.

theorem subbarao.even : ∀ r t, 0 < t →
    {n : ℕ | n ≡ r [MOD t] ∧ Even (partitionNumber n)}.Infinite

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

`PartitionParity.subbarao.odd`

Solved: stated here without proof.

Every arithmetic progression contains infinitely many n where p(n) is odd. Conjectured by Subbarao; Ono proved it for every progression containing at least one n with p(n) odd, and Radu showed that every progression contains such an n.

theorem subbarao.odd : ∀ r t, 0 < t →
    {n : ℕ | n ≡ r [MOD t] ∧ Odd (partitionNumber n)}.Infinite

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

`PartitionParity.ahlgren.even`

Solved: stated here without proof.

For every arithmetic progression r (mod t), the number of n ≤ X with n ≡ r (mod t) and p(n) even is ≫ √X. (Ahlgren)

theorem ahlgren.even : ∀ r t, 0 < t →
    (fun X : ℝ ↦ √X) =O[atTop]
      fun X : ℝ ↦ ({n : ℕ | n ≤ X ∧ n ≡ r [MOD t] ∧ Even (partitionNumber n)}.ncard : ℝ)

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

`PartitionParity.ahlgren.odd`

Solved: stated here without proof.

For every arithmetic progression r (mod t), the number of n ≤ X with n ≡ r (mod t) and p(n) odd is ≫ √X / log X. Ahlgren proved this for every progression containing at least one n with p(n) odd; by Radu's theorem every progression does.

theorem ahlgren.odd : ∀ r t, 0 < t →
    (fun X : ℝ ↦ √X / X.log) =O[atTop]
      fun X : ℝ ↦ ({n : ℕ | n ≤ X ∧ n ≡ r [MOD t] ∧ Odd (partitionNumber n)}.ncard : ℝ)

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

`PartitionParity.bellaiche_nicolas.even`

Solved: stated here without proof.

The number of n ≤ X with p(n) even is ≫ √X log log X. (Bellaïche–Nicolas)

theorem bellaiche_nicolas.even :
    (fun X : ℝ ↦ √X * X.log.log) =O[atTop]
      fun X : ℝ ↦ ({n : ℕ | n ≤ X ∧ Even (partitionNumber n)}.ncard : ℝ)

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

`PartitionParity.bellaiche_nicolas.even_explicit`

Solved: stated here without proof.

The number of n ≤ x with p(n) even is at least 0.069 √x log log x for every x > 1. (Bellaïche–Nicolas)

theorem bellaiche_nicolas.even_explicit : ∀ x : ℝ, 1 < x →
    0.069 * √x * x.log.log ≤ ({n : ℕ | n ≤ x ∧ Even (partitionNumber n)}.ncard : ℝ)

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

`PartitionParity.bellaiche_nicolas.odd_explicit`

Solved: stated here without proof.

The number of n ≤ x with p(n) odd is at least 0.037 √x / (log x)^(7/8) for every x ≥ 2. (Bellaïche–Nicolas)

theorem bellaiche_nicolas.odd_explicit : ∀ x : ℝ, 2 ≤ x →
    0.037 * √x / (x.log) ^ (7 / 8 : ℝ) ≤ ({n : ℕ | n ≤ x ∧ Odd (partitionNumber n)}.ncard : ℝ)

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

`PartitionParity.bellaiche_green_soundararajan.odd`

Solved: stated here without proof.

The number of n ≤ X with p(n) odd is ≫ √X / log log X. (Bellaïche–Green–Soundararajan)

theorem bellaiche_green_soundararajan.odd :
    (fun X : ℝ ↦ √X / X.log.log) =O[atTop]
      fun X : ℝ ↦ ({n : ℕ | n ≤ X ∧ Odd (partitionNumber n)}.ncard : ℝ)

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

`PartitionParity.ono_swaminathan.quadratic`

Solved: stated here without proof.

For square-free D > 1 with D ≡ 23 (mod 24), both parities occur infinitely often among p((D m² + 1) / 24) as m ranges over the positive integers coprime to 6. Note that 24 ∣ D m² + 1 for such m. Conjectured by Ono and proved by Ono–Swaminathan.

theorem ono_swaminathan.quadratic : ∀ D : ℕ, 1 < D → Squarefree D → D % 24 = 23 →
    {m : ℕ | m.Coprime 6 ∧ Even (partitionNumber ((D * m ^ 2 + 1) / 24))}.Infinite ∧
    {m : ℕ | m.Coprime 6 ∧ Odd (partitionNumber ((D * m ^ 2 + 1) / 24))}.Infinite

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

`PartitionParity.ono_swaminathan.odd_bound`

Solved: stated here without proof.

The odd half of Theorem 1 of Ono–Swaminathan, with its effective bound: for square-free D > 1 with D ≡ 23 (mod 24) there is an m coprime to 6 with m ≤ 12 h(-D) + 2 such that p((D m² + 1) / 24) is odd, where h(-D) is the class number of ℚ(√-D). Here ℚ(√-D) is AdjoinRoot (X ^ 2 + D), a number field since X ^ 2 + D is irreducible over ℚ for D > 0.

theorem ono_swaminathan.odd_bound (D : ℕ) (hD : 1 < D) (hsq : Squarefree D) (h23 : D % 24 = 23) :
    haveI : Fact (Irreducible (X ^ 2 + C (D : ℚ))) :=
      ⟨irreducible_X_sq_add_C_of_pos (Nat.cast_pos.2 (by lia))⟩
    ∃ m : ℕ, m.Coprime 6 ∧
      m ≤ 12 * NumberField.classNumber (AdjoinRoot (X ^ 2 + C (D : ℚ))) + 2 ∧
      Odd (partitionNumber ((D * m ^ 2 + 1) / 24))

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

`PartitionParity.classNumber_eq_ncard_reducedForms`

Textbook result, stated without proof.

For square-free D ≡ 3 (mod 4), the discriminant -D is fundamental and the class number of ℚ(√-D) equals the number of reduced primitive positive-definite binary quadratic forms of discriminant -D [Cox, Theorem 2.8]. This identification is used in Zheng's appendix to Ono–Swaminathan.

theorem classNumber_eq_ncard_reducedForms (D : ℕ) (hsq : Squarefree D) (h3 : D % 4 = 3) :
    haveI : Fact (Irreducible (X ^ 2 + C (D : ℚ))) :=
      ⟨irreducible_X_sq_add_C_of_pos (Nat.cast_pos.2 (by lia))⟩
    NumberField.classNumber (AdjoinRoot (X ^ 2 + C (D : ℚ))) =
      {⟨a, b, c⟩ : ℤ × ℤ × ℤ | IsReducedForm D a b c}.ncard

Category textbook; AMS 11 Number theory. Declared in FormalConjectures/Paper/PartitionParity.lean, line 174.

`PartitionParity.zheng.liminf`

Solved: stated here; a Lean proof assuming ono_swaminathan.odd_bound, classNumber_eq_ncard_reducedForms is at https://github.com/AxiomMath/PartitionZheng/blob/9bfb4326c4ea1e00016a842d7cc145e5c4e0684a/Solution/Basic.lean#L17.

Zheng's explicit lower bound: liminf_{X → ∞} N_odd(X) / √X ≥ 243 / (64 √6 π⁵), where N_odd(X) is the number of n ≤ X with p(n) odd [Ono-Swaminathan, Appendix A, Corollary 2].

theorem zheng.liminf :
    ((243 / (64 * √6 * π ^ 5) : ℝ) : EReal) ≤
      liminf (fun X : ℝ ↦
        ((({n : ℕ | n ≤ X ∧ Odd (partitionNumber n)}.ncard : ℝ) / √X : ℝ) : EReal)) atTop

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

`PartitionParity.zheng.odd`

Solved: stated here without proof.

The number of n ≤ X with p(n) odd is ≫ √X.

theorem zheng.odd :
    (fun X : ℝ ↦ √X) =O[atTop]
      fun X : ℝ ↦ ({n : ℕ | n ≤ X ∧ Odd (partitionNumber n)}.ncard : ℝ)

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

`PartitionParity.ono.polynomial`

Open: stated without proof.

Ono's conjecture, as stated in Section 1 of Ono–Swaminathan: if g is a nonconstant integer-valued polynomial that is eventually positive, then p(g(n)) is even for infinitely many n and odd for infinitely many n.

theorem ono.polynomial (g : ℚ[X]) (hg : 0 < g.natDegree)
    (hint : ∀ n : ℕ, ∃ k : ℤ, g.eval (n : ℚ) = k)
    (hpos : ∀ᶠ n : ℕ in atTop, 0 < g.eval (n : ℚ)) :
    {n : ℕ | Even (partitionNumber ⌊g.eval (n : ℚ)⌋₊)}.Infinite ∧
    {n : ℕ | Odd (partitionNumber ⌊g.eval (n : ℚ)⌋₊)}.Infinite

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

Sources

TheoremPfister's problem on the Pythagoras number of \(\mathbb{R}(X_1, \dots, X_n)\)#

The Pythagoras number \(p(K)\) of a field \(K\) is the least \(p\) such that every sum of squares in \(K\) is a sum of \(p\) squares, i.e. the least element of pythagorasBounds K.

Artin's solution of Hilbert's 17th problem shows that a positive semidefinite rational function in \(\mathbb{R}(X_1, \dots, X_n)\) is a sum of squares, and Pfister showed that \(2^n\) squares suffice ([Pfister1967, Theorem 1]; for the field, Corollary 1 of Theorem 2 in [Pfister1971]). Since sums of squares are positive semidefinite, \(p(\mathbb{R}(X_1, \dots, X_n)) \le 2^n\) [Pfister1995, p. 95].

Problem 1 of [Pfister1971, §4] asks for the true value of \(p(\mathbb{R}(X_1, \dots, X_n))\). The question is often posed as: is \(p(\mathbb{R}(X_1, \dots, X_n)) = 2^n\), i.e. is Pfister's bound optimal? See e.g. [Benoist2017, Question 0.2].

Problem 1 itself quotes the lower bound \(n + 1 \le p(\mathbb{R}(X_1, \dots, X_n))\) from Cassels' theorem [Cassels1964]. For \(n \ge 2\) the best known bounds are \(n + 2 \le p(\mathbb{R}(X_1, \dots, X_n)) \le 2^n\) [Pfister1995, p. 97], where the lower bound follows from the Cassels–Ellison–Pfister theorem [CEP1971]. The bounds agree for \(n = 2\), so the value is known for \(n \le 2\) and open for every \(n \ge 3\). The survey [MerkurjevParimala2025, §5.2] records the question as open even for \(\mathbb{R}(X_1, X_2, X_3)\) (Question 5.7).

References: - [Pfister1971] A. Pfister, Sums of squares in real function fields, pp. 297–300 in Actes du Congrès International des Mathématiciens, Tome 1 (Nice, 1970), Gauthier-Villars, 1971, IMU scan. - [Pfister1967] A. Pfister, Zur Darstellung definiter Funktionen als Summe von Quadraten, Invent. Math. 4 (1967), 229–237, doi:10.1007/BF01425382. - [Cassels1964] J. W. S. Cassels, On the representation of rational functions as sums of squares, Acta Arith. 9 (1964), 79–82, doi:10.4064/aa-9-1-79-82. - [Pfister1995] A. Pfister, Quadratic forms with applications to algebraic geometry and topology, London Math. Soc. Lecture Note Ser. 217, Cambridge University Press, 1995. - [CEP1971] J. W. S. Cassels, W. J. Ellison, A. Pfister, On sums of squares and on elliptic curves over function fields, J. Number Theory 3 (1971), 125–149, doi:10.1016/0022-314X(71)90030-8. - [Benoist2017] O. Benoist, On Hilbert's 17th problem in low degree, Algebra Number Theory 11 (2017), 929–959, doi:10.2140/ant.2017.11.929, arXiv:1602.07330. - [MerkurjevParimala2025] A. Merkurjev, R. Parimala, Quadratic forms beyond arithmetic, Notices Amer. Math. Soc. 72 (2025), no. 7, 711–718, doi:10.1090/noti3192.

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

`PfisterPythagorasNumber.pfister_problem`

Open: stated without proof.

Pfister's problem (Problem 1 of [Pfister1971, §4]): what is the true value of \(p(\mathbb{R}(X_1, \dots, X_n))\), as a function of \(n\)? It is \(1\), \(2\), \(4\) for \(n = 0, 1, 2\) (pfister_problem.variants.zero, pfister_problem.variants.one, pfister_problem.variants.two) and open for every \(n \ge 3\), where only the bounds \(n + 2 \le p(\mathbb{R}(X_1, \dots, X_n)) \le 2^n\) are known.

theorem pfister_problem :
    ∀ n, IsLeast (pythagorasBounds (MvRatFunc (Fin n) ℝ)) (pfister_problem.answer n)

Category research open; AMS 11 Number theory, 12 Field theory and polynomials, 14 Algebraic geometry. Declared in FormalConjectures/Paper/PfisterPythagorasNumber.lean, line 90.

`PfisterPythagorasNumber.pfister_problem.variants.eq_two_pow`

Open: stated without proof.

Pfister's problem in its common yes/no form (e.g. Question 0.2 of [Benoist2017]): is \(p(\mathbb{R}(X_1, \dots, X_n)) = 2^n\) for every \(n\), i.e. is Pfister's bound optimal? This holds for \(n \le 2\) and is open for every \(n \ge 3\).

theorem pfister_problem.variants.eq_two_pow :
    ∀ n : ℕ, IsLeast (pythagorasBounds (MvRatFunc (Fin n) ℝ)) (2 ^ n)

Category research open; AMS 11 Number theory, 12 Field theory and polynomials, 14 Algebraic geometry. Declared in FormalConjectures/Paper/PfisterPythagorasNumber.lean, line 100.

`PfisterPythagorasNumber.pfister_problem.variants.upper_bound`

Solved: stated here; a Lean proof is at https://github.com/anatoliiohorodnyk/lean-fc-proofs/blob/a25a41b3e51f6987edeafcc1602e80e6d30e6f05/Proofs/T_PfisterPythagorasNumber_pfister_problem_variants_upper_bound.lean#L1006.

Pfister's theorem: every sum of squares in \(\mathbb{R}(X_1, \dots, X_n)\) is a sum of \(2^n\) squares [Pfister1995, p. 95]; this is Corollary 1 of Theorem 2 in [Pfister1971]. For positive semidefinite polynomials it is [Pfister1967, Theorem 1], the quantitative refinement of Artin's theorem Hilbert17.hilbert_17th_problem in FormalConjectures/HilbertProblems/17.lean.

theorem pfister_problem.variants.upper_bound (n : ℕ) :
    2 ^ n ∈ pythagorasBounds (MvRatFunc (Fin n) ℝ)

Category research solved; AMS 11 Number theory, 12 Field theory and polynomials, 14 Algebraic geometry. Declared in FormalConjectures/Paper/PfisterPythagorasNumber.lean, line 112.

`PfisterPythagorasNumber.pfister_problem.variants.cassels`

Solved: stated here; a Lean proof is at https://github.com/anatoliiohorodnyk/lean-fc-proofs/blob/a25a41b3e51f6987edeafcc1602e80e6d30e6f05/Proofs/T_PfisterPythagorasNumber_pfister_problem_variants_cassels.lean#L434.

Cassels' theorem [Cassels1964], as quoted in Problem 1 of [Pfister1971, §4]: \(1 + X_1^2 + \dots + X_n^2\) is not a sum of \(n\) squares in \(\mathbb{R}(X_1, \dots, X_n)\).

theorem pfister_problem.variants.cassels (n : ℕ) :
    ¬IsSumSqOfLength n (algebraMap (MvPolynomial (Fin n) ℝ) (MvRatFunc (Fin n) ℝ)
      (1 + ∑ i, MvPolynomial.X i * MvPolynomial.X i))

Category research solved; AMS 11 Number theory, 12 Field theory and polynomials, 14 Algebraic geometry. Declared in FormalConjectures/Paper/PfisterPythagorasNumber.lean, line 122.

`PfisterPythagorasNumber.pfister_problem.variants.add_one_le`

Proved here.

The lower bound \(n + 1 \le p(\mathbb{R}(X_1, \dots, X_n))\) quoted in Problem 1 of [Pfister1971, §4]: \(1 + X_1^2 + \dots + X_n^2\) is a sum of \(n + 1\) squares but, by Cassels' theorem pfister_problem.variants.cassels, not of \(n\) squares. It is superseded by pfister_problem.variants.lower_bound for \(n \ge 2\).

theorem pfister_problem.variants.add_one_le (n : ℕ) {p : ℕ}
    (hp : p ∈ pythagorasBounds (MvRatFunc (Fin n) ℝ)) : n + 1 ≤ p

Category research solved; AMS 11 Number theory, 12 Field theory and polynomials, 14 Algebraic geometry. Declared in FormalConjectures/Paper/PfisterPythagorasNumber.lean, line 134.

`PfisterPythagorasNumber.pfister_problem.variants.lower_bound`

Solved: stated here without proof.

The lower bound \(n + 2 \le p(\mathbb{R}(X_1, \dots, X_n))\) for \(n \ge 2\) [Pfister1995, p. 97], a consequence of the Cassels–Ellison–Pfister theorem [CEP1971]. The hypothesis \(n \ge 2\) is needed: \(p(\mathbb{R}(X)) = 2 < 3\).

theorem pfister_problem.variants.lower_bound (n : ℕ) (hn : 2 ≤ n) {p : ℕ}
    (hp : p ∈ pythagorasBounds (MvRatFunc (Fin n) ℝ)) : n + 2 ≤ p

Category research solved; AMS 11 Number theory, 12 Field theory and polynomials, 14 Algebraic geometry. Declared in FormalConjectures/Paper/PfisterPythagorasNumber.lean, line 149.

`PfisterPythagorasNumber.pfister_problem.variants.zero`

Textbook result, proved here.

\(p(\mathbb{R}(X_1, \dots, X_n)) = 1\) for \(n = 0\), i.e. \(p(\mathbb{R}) = 1\): here the bounds \(n + 1\) and \(2^n\) of pfister_problem.variants.add_one_le and pfister_problem.variants.upper_bound agree. Compare isLeast_pythagorasBounds_real, the same value for ℝ itself.

theorem pfister_problem.variants.zero : IsLeast (pythagorasBounds (MvRatFunc (Fin 0) ℝ)) 1

Category textbook; AMS 11 Number theory, 12 Field theory and polynomials, 14 Algebraic geometry. Declared in FormalConjectures/Paper/PfisterPythagorasNumber.lean, line 159.

`PfisterPythagorasNumber.pfister_problem.variants.one`

Textbook result, proved here.

\(p(\mathbb{R}(X)) = 2\) [Pfister1995, p. 96]: Pfister's bound gives \(p \le 2\), and Cassels' theorem pfister_problem.variants.cassels gives \(p \ge 2\) through pfister_problem.variants.add_one_le, since \(1 + X^2\) is a sum of two squares that is not a square in \(\mathbb{R}(X)\).

theorem pfister_problem.variants.one : IsLeast (pythagorasBounds (MvRatFunc (Fin 1) ℝ)) 2

Category textbook; AMS 11 Number theory, 12 Field theory and polynomials, 14 Algebraic geometry. Declared in FormalConjectures/Paper/PfisterPythagorasNumber.lean, line 170.

`PfisterPythagorasNumber.pfister_problem.variants.two`

Proved here.

\(p(\mathbb{R}(X_1, X_2)) = 4\) [CEP1971], as recorded in [Pfister1971, §4] and [Pfister1995, p. 96]: the bounds \(n + 2\) and \(2^n\) agree when \(n = 2\).

theorem pfister_problem.variants.two : IsLeast (pythagorasBounds (MvRatFunc (Fin 2) ℝ)) 4

Category research solved; AMS 11 Number theory, 12 Field theory and polynomials, 14 Algebraic geometry. Declared in FormalConjectures/Paper/PfisterPythagorasNumber.lean, line 179.

Sources

TheoremPrime Tuples Conjecture #

Reference: [FLC07] Friedlander, J. B. and Luca, F. and Stoiciu, M., On the irrationality of a divisor function series. Integers (2007).

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

`PrimeTuplesConjecture.prime_tuples_conjecture`

Open: stated without proof.

For any k ≥ 2, let a₁,...,aₖ and b₁,...,bₖ be integers with aᵢ > 0. Suppose that for every prime p there exists an integer n such that p ∤ ∏ i, (aᵢ n + bᵢ). Then there exist infinitely many n such that aᵢ n + bᵢ is prime for all i.

theorem prime_tuples_conjecture {k : ℕ} (hk : 2 ≤ k) (a : Fin k → ℕ+) (b : Fin k → ℕ)
    (hab : ∀ p, p.Prime → ∃ n, ¬ p ∣ ∏ i, (a i * n + b i)) :
    Set.Infinite {n | ∀ i : Fin k, (a i * n + b i).Prime}

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

Sources

FormalConjectures/Paper/PrimeTuples.lean at 2055e5ad

LeanPrimeTuplesConjecture.prime_tuples_conjecture

TheoremPudlák's conjectures on incompleteness in the finite domain #

References: * [CR79] Cook, S. A. and Reckhow, R. A. (1979). "The relative efficiency of propositional proof systems." J. Symbolic Logic 44, pp. 36--50. * [HH88] Hartmanis, J. and Hemachandra, L. A. (1988). "Complexity classes without machines: on complete languages for UP." Theoret. Comput. Sci. 58, pp. 129--142. * [KP89] Krajíček, J. and Pudlák, P. (1989). "Propositional proof systems, the consistency of first order theories and the complexity of computations." J. Symbolic Logic 54, pp. 1063--1079. * [MP91] Megiddo, N. and Papadimitriou, C. H. (1991). "On total functions, existence theorems and computational complexity." Theoret. Comput. Sci. 81, pp. 317--324. * [Pa94] Papadimitriou, C. H. (1994). "On the complexity of the parity argument and other inefficient proofs of existence." J. Comput. System Sci. 48, pp. 498--532. * [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. * [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/PudlakFiniteDomainConjectures.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: 4 open, 2 solved and 1 textbook result. It also has 4 API statements, counted here but not shown.

`PudlakFiniteDomain.sat_no_p_optimal_proof_system`

Open: stated without proof.

SAT has no p-optimal proof system (Pudlák's conjecture SAT [Pu17]).

No proof system for SAT p-simulates every other proof system for SAT. Since the existence of a p-optimal proof system depends only on the polynomial-time many-one degree of the language [KMT03], the conjecture is stated here for an arbitrary NP-complete language. Equivalently [Pu17], for every consistent polynomial-time axiomatized theory T ⊇ S¹₂ there is a proof system for SAT whose soundness T cannot prove.

theorem sat_no_p_optimal_proof_system (L : DecisionProblem) (hL : IsCompleteFor NP L) :
    ¬∃ P : List Bool → List Bool, IsPOptimalProofSystem L P

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

`PudlakFiniteDomain.tfnp_no_complete_problem`

Open: stated without proof.

TFNP has no complete problem (Megiddo–Papadimitriou [MP91]; Pudlák's conjecture TFNP [Pu17]).

No total NP search problem is complete under polynomial-time many-one reductions of search problems. Equivalently [Pu17], for every consistent polynomial-time axiomatized theory T ⊇ S¹₂ some total NP search problem is not polynomially reducible to any total NP search problem provably total in T.

theorem tfnp_no_complete_problem : ¬∃ T : TFNPProblem, T.IsComplete

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

`PudlakFiniteDomain.up_no_complete_language`

Open: stated without proof.

UP has no complete language (Hartmanis–Hemachandra [HH88]; Pudlák's conjecture UP [Pu17]).

No language accepted by an unambiguous polynomial-time verifier is complete for UP under polynomial-time many-one reductions.

theorem up_no_complete_language : ¬∃ L : DecisionProblem, IsCompleteFor UP L

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

`PudlakFiniteDomain.np_inter_conp_no_complete_language`

Open: stated without proof.

NP ∩ coNP has no complete language (Pudlák's conjecture NP ∩ coNP [Pu17]).

No language in NP ∩ coNP is complete for that class under polynomial-time many-one reductions.

theorem np_inter_conp_no_complete_language :
    ¬∃ L : DecisionProblem, IsCompleteFor (NP ∩ coNP) L

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

`PudlakFiniteDomain.tfnp_no_complete_problem.variants.exists_of_NP_eq_coNP`

Solved: stated here without proof.

If NP = coNP then TFNP has a complete problem [MP91, Pu17].

Under NP = coNP the search problem "given a CNF, find a satisfying assignment or a short proof of unsatisfiability" is total and complete.

theorem tfnp_no_complete_problem.variants.exists_of_NP_eq_coNP (h : NP = coNP) :
    ∃ T : TFNPProblem, T.IsComplete

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

`PudlakFiniteDomain.tfnp_no_complete_problem.variants.NP_ne_coNP`

Proved here.

The conjecture implies NP ≠ coNP [Pu17].

theorem tfnp_no_complete_problem.variants.NP_ne_coNP
    (h : ¬∃ T : TFNPProblem, T.IsComplete) : NP ≠ coNP

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

`PudlakFiniteDomain.sat_no_p_optimal_proof_system.variants.exists_of_P_eq_NP`

Textbook result, stated without proof.

If P = NP then every NP-complete language has a p-optimal proof system.

The map sending π to itself when π ∈ L and to a fixed element of L otherwise is then polynomial-time, and every proof system Q for L is p-simulated by it via Q itself.

theorem sat_no_p_optimal_proof_system.variants.exists_of_P_eq_NP (h : P = NP)
    (L : DecisionProblem) (hL : IsCompleteFor NP L) (hne : ∃ y, L y = true) :
    ∃ P : List Bool → List Bool, IsPOptimalProofSystem L P

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

Sources

LeanPudlakFiniteDomain.sat_no_p_optimal_proof_system · PudlakFiniteDomain.tfnp_no_complete_problem · PudlakFiniteDomain.up_no_complete_language · PudlakFiniteDomain.np_inter_conp_no_complete_language · PudlakFiniteDomain.tfnp_no_complete_problem.variants.exists_of_NP_eq_coNP · PudlakFiniteDomain.tfnp_no_complete_problem.variants.NP_ne_coNP · PudlakFiniteDomain.sat_no_p_optimal_proof_system.variants.exists_of_P_eq_NP

TheoremReed's omega, delta, and chi conjecture #

References: - B. Reed, ω Δ and χ, J. Graph Theory 27 (1998) 177-212. - openproblemgarden - mathoverflow/37923 asked by user Andrew D. King

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

`ReedOmegaDeltaChi.reed_omega_delta_chi_conjecture`

Open: stated without proof.

For a graph \(G\), we define \(\Delta(G)\) to be the maximum degree, \(\omega(G)\) to be the size of the largest clique subgraph, and \(\chi(G)\) to be the chromatic number. Reed's omega, delta, and chi conjecture states that

\[\chi(G) \leq \lceil \frac{1}{2}(\omega(G) + \Delta(G) + 1) \rceil.\]

theorem reed_omega_delta_chi_conjecture :
  ∀ {V : Type} (G : SimpleGraph V),
    let χ := G.chromaticNumber
    let ω := G.ecliqueNum
    let Δ := G.emaxDegree
    2 * χ ≤ ω + Δ + 2

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

`ReedOmegaDeltaChi.reed_omega_delta_chi_conjecture_for_finite_graphs`

Open: stated without proof.

For a finite graph \(G\), we define \(\Delta(G)\) to be the maximum degree, \(\omega(G)\) to be the size of the largest clique subgraph, and \(\chi(G)\) to be the chromatic number. Reed's omega, delta, and chi conjecture states that

\[\chi(G) \leq \lceil \frac{1}{2}(\omega(G) + \Delta(G) + 1) \rceil.\]

theorem reed_omega_delta_chi_conjecture_for_finite_graphs :
  ∀ {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj],
    let χ := G.chromaticNumber
    let ω := G.cliqueNum
    let Δ := G.maxDegree
    2 * χ ≤ ω + Δ + 2

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

`ReedOmegaDeltaChi.reed_conjecture_Δ_6_ω_2`

Open: stated without proof.

The simplest open case is when \(\Delta(G) = 6\) and \(\omega(G) = 2\).

theorem reed_conjecture_Δ_6_ω_2 :
  ∀ {V : Type} (G : SimpleGraph V), G.emaxDegree = 6 ∧ G.cliqueNum = 2 → G.chromaticNumber ≤ 5

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

Sources

LeanReedOmegaDeltaChi.reed_omega_delta_chi_conjecture · ReedOmegaDeltaChi.reed_omega_delta_chi_conjecture_for_finite_graphs · ReedOmegaDeltaChi.reed_conjecture_Δ_6_ω_2

TheoremEquivalents to the Riemann Hypothesis #

This file contains formal statements that are known to be equivalent to the Riemann Hypothesis, following the survey [Co26], §4. The statement of the Riemann Hypothesis itself is in FormalConjectures.Millennium.RiemannHypothesis.

References: * [Co26] A. Connes, The Riemann Hypothesis: Past, Present and a Letter Through Time, 2026.

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

`RiemannHypothesis.robin_criterion`

Solved: stated here without proof.

Robin's Criterion. The Riemann Hypothesis is equivalent to

\[ \sigma(n) < e ^ {\gamma} n\log\log n \]

for all \(n > 5040\), where \(\gamma\) is the Euler-Mascheroni constant and \(\sigma(n)\) is the sum of divisors.

theorem robin_criterion :
    RiemannHypothesis ↔ ∀ n > 5040, σ 1 n < (exp eulerMascheroniConstant) * n * log (log n)

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

`RiemannHypothesis.robin_criterion_rhs`

Open: stated without proof.

The statement that Robin's criterion holds.

theorem robin_criterion_rhs {n : ℕ} (hn : n > 5040) :
    σ 1 n < exp eulerMascheroniConstant * n * log (log n)

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

`RiemannHypothesis.lagarias_criterion`

Solved: stated here without proof.

Lagarias' Criterion. A refinement of Robin's criterion: the Riemann Hypothesis is equivalent to

\[ \sigma(n) < H_n + e^{H_n}\log H_n \]

for all \(n \geq 2\), where \(H_n = 1 + 1/2 + \cdots + 1/n\) is the \(n\)th harmonic number.

Note that [Co26] states this for all \(n \geq 1\), but at \(n = 1\) both sides equal \(1\); Lagarias' original formulation is the non-strict inequality for all \(n \geq 1\), with equality only at \(n = 1\).

theorem lagarias_criterion : RiemannHypothesis ↔
    ∀ n > 1, σ 1 n < harmonic n + exp (harmonic n) * log (harmonic n)

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

`RiemannHypothesis.lagarias_criterion_rhs`

Open: stated without proof.

The statement that Lagarias' criterion holds.

theorem lagarias_criterion_rhs {n : ℕ} (hn : 1 < n) :
    σ 1 n < harmonic n + exp (harmonic n) * log (harmonic n)

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

`RiemannHypothesis.li_criterion`

Solved: stated here without proof.

Li's Criterion. The Riemann Hypothesis is equivalent to the positivity of

\[ \lambda_n := \sum_{\rho}\left(1 - \left(1 - \frac{1}{\rho}\right)^n\right) \]

for each \(n > 0\).

theorem li_criterion : RiemannHypothesis ↔ ∀ n > 0, 0 < lambda n

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

`RiemannHypothesis.li_criterion_rhs`

Open: stated without proof.

The statement that Li's criterion holds.

theorem li_criterion_rhs {n : ℕ} (hn : 0 < n) : 0 < lambda n

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

`RiemannHypothesis.beurling_nyman_criterion`

Solved: stated here without proof.

Beurling-Nyman Criterion. The Riemann Hypothesis is equivalent to the statement that the set of finite linear combination \(\sum_{\nu = 1}^n c_{\nu}\rho_{\theta_{\nu}}\) is dense in \(L^2(0, 1)\), when ranging over \(0 < \theta_{\nu}\leq 1\) and \(\sum_{\nu = 1}^n c_{\nu}\theta_{\nu} = 0\).

theorem beurling_nyman_criterion : RiemannHypothesis ↔
    Dense { fractScalarInvSumL2 n c θ | (n) (c) (θ)
      (hθ : ∀ ν, θ ν ∈ Set.Ioc 0 1) (h : ∑ ν, c ν * θ ν = 0) }

Category research solved; AMS 11 Number theory, 28 Measure and integration. Declared in FormalConjectures/Paper/RiemannHypothesisEquivalents.lean, line 136.

`RiemannHypothesis.beurling_nyman_criterion_rhs`

Open: stated without proof.

The statement that the Beurling-Nyman criterion holds.

theorem beurling_nyman_criterion_rhs :
    Dense { fractScalarInvSumL2 n c θ | (n) (c) (θ)
      (hθ : ∀ ν, θ ν ∈ Set.Ioc 0 1) (h : ∑ ν, c ν * θ ν = 0) }

Category research open; AMS 11 Number theory, 28 Measure and integration. Declared in FormalConjectures/Paper/RiemannHypothesisEquivalents.lean, line 143.

`RiemannHypothesis.weil_positivity_criterion`

Solved: stated here without proof.

Weil's Positivity Criterion. The Riemann Hypothesis is equivalent to the non-positivity of Weil factor sums on the convolution of test functions. In [Co26] this is expressed as

\[ \sum_v W_v(g\star g^*) \leq 0 \]

for all compactly-supported smooth functions \(g : \mathbb{R}_+^{\times} \to \mathbb{C}\) such that the Mellin transform of \(g\) vanishes at \(\pm i / 2\), where \(g^*(x) := \bar{g}(x^{-1})\) and \(W_v\) are the multiplicative Weil factors defined in [Co26]. We formalise this as the corresponding additive statement (via \(x = e^u\)), since convolution in mathlib is additive, and restrict to real-valued test functions \(g\), which suffices for the equivalence.

theorem weil_positivity_criterion :
    RiemannHypothesis ↔ ∀ g : C_c(ℝ, ℝ), ContDiff ℝ ∞ g → IsTestFunction g →
      weilArchimedean (g ⋆ fun x ↦ g (-x)) +
        ∑' p : Nat.Primes, weilNonArchimedean p (g ⋆ fun x ↦ g (-x)) ≤ 0

Category research solved; AMS 11 Number theory, 46 Functional analysis. Declared in FormalConjectures/Paper/RiemannHypothesisEquivalents.lean, line 173.

`RiemannHypothesis.weil_positivity_criterion_rhs`

Open: stated without proof.

The statement that the Weil criterion holds.

theorem weil_positivity_criterion_rhs {g : C_c(ℝ, ℝ)} (hg : ContDiff ℝ ∞ g)
    (h : IsTestFunction g) :
    weilArchimedean (g ⋆ fun x ↦ g (-x)) +
      ∑' p : Nat.Primes, weilNonArchimedean p (g ⋆ fun x ↦ g (-x)) ≤ 0

Category research open; AMS 11 Number theory, 46 Functional analysis. Declared in FormalConjectures/Paper/RiemannHypothesisEquivalents.lean, line 181.

Sources

LeanRiemannHypothesis.robin_criterion · RiemannHypothesis.robin_criterion_rhs · RiemannHypothesis.lagarias_criterion · RiemannHypothesis.lagarias_criterion_rhs · RiemannHypothesis.li_criterion · RiemannHypothesis.li_criterion_rhs · RiemannHypothesis.beurling_nyman_criterion · RiemannHypothesis.beurling_nyman_criterion_rhs · RiemannHypothesis.weil_positivity_criterion · RiemannHypothesis.weil_positivity_criterion_rhs

TheoremMoments of the Riemann zeta function on the critical line #

The moments \(\frac{1}{T}\int_0^T |\zeta(1/2 + it)|^{2k}\,dt\) are conjectured to be asymptotic to \(c_k (\log T)^{k^2}\) for some constants \(c_k\). This is a theorem for \(k = 1\) (Hardy–Littlewood, \(c_1 = 1\)) and \(k = 2\) (Ingham, \(c_2 = 1/(2\pi^2)\)), and these are the only proven cases. Conrey–Ghosh and Conrey–Gonek conjectured \(c_3 = 42 a_3 / 9!\) and \(c_4 = 24024 a_4 / 16!\), with \(a_k\) the arithmetic factor \(a_k = \prod_p (1 - 1/p)^{k^2} \sum_{m \ge 0} \binom{m+k-1}{m}^2 p^{-m}\); Keating–Snaith conjectured \(c_k = a_k f_k\) with \(f_k = \prod_{j=0}^{k-1} j!/(j+k)!\) from random matrix theory, recovering \(g_k = (k^2)!\,f_k = 1, 2, 42, 24024\).

The statements and constants below are taken from §3.4.5 of [Co26].

References: - [Co26] A. Connes, The Riemann Hypothesis: Past, Present and a Letter Through Time, arXiv:2602.04022, §3.4.5. - [In26] A. E. Ingham, Mean-value theorems in the theory of the Riemann zeta-function, Proc. London Math. Soc. 27 (1926), 273–300. - [CG98] J. B. Conrey, A. Ghosh, A conjecture for the sixth power moment of the Riemann zeta-function, Internat. Math. Res. Notices 1998, no. 15, 775–780. - [CGo01] J. B. Conrey, S. Gonek, High moments of the Riemann zeta-function, Duke Math. J. 107 (2001), no. 3, 577–604. - [KS00] J. P. Keating, N. C. Snaith, Random matrix theory and \(\zeta(1/2+it)\), Commun. Math. Phys. 214 (2000), no. 1, 57–89.

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

`RiemannZetaMoments.moment_isEquiv`

Open: stated without proof.

The asymptotic behaviour of the \(k\)th moment of the Riemann zeta function is conjectured to be

\[ \frac{1}{T}\int_0^T |\zeta(1/2 + it)|^{2k}dt \sim c_k \log(T)^{k^2}, \]

for some constant \(c_k\).

theorem moment_isEquiv (k : ℕ) : ∃ c > (0 : ℝ),
    moment k ~[atTop] fun T ↦ c * T.log ^ (k ^ 2)

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

`RiemannZetaMoments.moment_isEquiv₁`

Solved: stated here without proof.

The asymptotic behaviour of the first moment of the Riemann zeta function was proved by Hardy and Littlewood, where \(c_1 = 1\) [Co26, §3.4.5].

theorem moment_isEquiv₁ : moment 1 ~[atTop] fun T ↦ T.log

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

`RiemannZetaMoments.moment_isEquiv₂`

Solved: stated here without proof.

The asymptotic behaviour of the second moment of the Riemann zeta function was proved by Ingham [In26], where \(c_2 = 1/(2\pi^2)\).

theorem moment_isEquiv₂ : moment 2 ~[atTop] fun T ↦ (1 / (2 * π ^ 2)) * T.log ^ 4

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

`RiemannZetaMoments.moment_isEquiv₃`

Open: stated without proof.

The constant in the asymptotic formula for the 3rd zeta moment is conjectured to be \(42a_3/9!\) [CG98].

theorem moment_isEquiv₃ : moment 3 ~[atTop] fun T ↦ 42 * arithmeticFactor 3 / 9 ! * T.log ^ 9

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

`RiemannZetaMoments.moment_isEquiv₄`

Open: stated without proof.

The constant in the asymptotic formula for the 4th zeta moment is conjectured to be \(24024a_4/16!\) [CGo01].

theorem moment_isEquiv₄ :
    moment 4 ~[atTop] fun T ↦ 24024 * arithmeticFactor 4 / 16 ! * T.log ^ 16

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

`RiemannZetaMoments.moment_isEquivₖ`

Open: stated without proof.

The Keating–Snaith conjecture [KS00] for the \(k\)th moment of the Riemann zeta function, provides the value of \(c_k\) in the asymptotic formula [Co26, §3.4.5].

theorem moment_isEquivₖ (k : ℕ) : moment k ~[atTop]
    fun T ↦ (arithmeticFactor k * ∏ j ∈ Finset.range k, (j ! : ℝ) / (j + k) !) *
      T.log ^ (k ^ 2)

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

Sources

LeanRiemannZetaMoments.moment_isEquiv · RiemannZetaMoments.moment_isEquiv₁ · RiemannZetaMoments.moment_isEquiv₂ · RiemannZetaMoments.moment_isEquiv₃ · RiemannZetaMoments.moment_isEquiv₄ · RiemannZetaMoments.moment_isEquivₖ

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

The Hall ratio conjecture… to Moments of the Riemann zeta…

TheoremThe Hall ratio conjecture (Harris 2019) — disproved#

HallRatioConjecture.hall_ratio_conjecture

HallRatioConjecture.hall_ratio_conjecture.variants.hallRatio_le_fractionalChromaticNumber

HallRatioConjecture.hall_ratio_conjecture.variants.unbounded

Sources

TheoremHartshorne's conjecture on Vector Bundles#

AlgebraicGeometry.Scheme.harthshorne_conjecture

Sources

TheoremConjectures around homogeneous topological spaces#

Homogeneous.homogeneousSpace_exists_inj_tendsto

Homogeneous.homogeneousSpace_exists_surjective

Homogeneous.firstCountableTopology_of_countablyMonolithicSpace

Homogeneous.countablyMonolithicSpace_card_lt

Homogeneous.monolithicSpace_exists_nhds_generated_countable

Sources

TheoremKaplansky's problem on the values of the \(u\)-invariant#

KaplanskyUInvariant.u_invariant_values

KaplanskyUInvariant.u_invariant_values.variants.kaplansky_conjecture

KaplanskyUInvariant.u_invariant_values.variants.not_three

KaplanskyUInvariant.u_invariant_values.variants.not_five

KaplanskyUInvariant.u_invariant_values.variants.not_seven

KaplanskyUInvariant.u_invariant_values.variants.two_pow

KaplanskyUInvariant.u_invariant_values.variants.even

KaplanskyUInvariant.u_invariant_values.variants.nine

KaplanskyUInvariant.u_invariant_values.variants.two_pow_add_one

KaplanskyUInvariant.u_invariant_values.variants.karpenko

KaplanskyUInvariant.u_invariant_values.variants.eleven

KaplanskyUInvariant.u_invariant_values.variants.odd

KaplanskyUInvariant.u_invariant_values.variants.thirteen

KaplanskyUInvariant.u_invariant_values.variants.fifteen

Sources

TheoremKotzig's Conjecture#

KotzigConjecture.kotzig_conjecture

Sources

TheoremKurepa's conjecture#

Kurepa.kurepa_conjecture

Kurepa's conjecture

Kurepa.kurepa_conjecture.variants.prime

Kurepa.kurepa_conjecture.prime_reduction

Kurepa.kurepa_conjecture.variants.gcd

Kurepa.kurepa_conjecture.gcd_reduction

Sources

TheoremConjectures about Latin Squares#

LatinSquare.oddOrderLatinSquareTransversal

LatinSquare.oddOrderLeq9LatinSquareTransversal

LatinSquare.latinSquareOrder11Transversal

LatinSquare.latinSquareNearTransversal

LatinSquare.z_even

LatinSquare.numTransversalsZn

LatinSquare.growthRateZn

LatinSquare.maxTransversalsBound

LatinSquare.molsExistenceProblem

LatinSquare.molsOrder12

Sources

TheoremLatin Tableau Conjecture#

LatinTableau.SimpleGraph.LatinTableauConjecture

Sources

TheoremLennon–Pittel conjecture on random stable matchings#

LennonPittel.lennon_pittel_conjecture

Sources

TheoremThe Manickam–Miklós–Singhi conjecture (1988)#

ManickamMiklosSinghiConjecture.manickam_miklos_singhi_conjecture

ManickamMiklosSinghiConjecture.manickam_miklos_singhi_conjecture.variants.pokrovskiy

ManickamMiklosSinghiConjecture.manickam_miklos_singhi_conjecture.variants.quadratic

Sources

TheoremMonochromatic quantum graphs (inherited vertex colorings)#

Main questions (informal)

Formalisation sketch

References

MonochromaticQuantumGraph.eqSystem4_no_solution_nnreal_ge4

MonochromaticQuantumGraph.eqSystem_no_solution_nnreal_even_ge6_ge3

MonochromaticQuantumGraph.eqSystem_no_solution_even_ge4_d_eq_n_explicit

MonochromaticQuantumGraph.eqSystem4_no_solution_d4

MonochromaticQuantumGraph.eqSystem4_no_solution_ge4

MonochromaticQuantumGraph.eqSystem6_no_solution_d3

MonochromaticQuantumGraph.eqSystem6_no_solution_d4

MonochromaticQuantumGraph.eqSystem6_no_solution_d5

MonochromaticQuantumGraph.eqSystem6_no_solution_d6

MonochromaticQuantumGraph.eqSystem6_no_solution_ge3

TheoremThe Hall ratio conjecture (Harris 2019) — disproved #

`HallRatioConjecture.hall_ratio_conjecture`

`HallRatioConjecture.hall_ratio_conjecture.variants.hallRatio_le_fractionalChromaticNumber`

`HallRatioConjecture.hall_ratio_conjecture.variants.unbounded`

TheoremHartshorne's conjecture on Vector Bundles #

`AlgebraicGeometry.Scheme.harthshorne_conjecture`

TheoremConjectures around homogeneous topological spaces #

`Homogeneous.homogeneousSpace_exists_inj_tendsto`

`Homogeneous.homogeneousSpace_exists_surjective`

`Homogeneous.firstCountableTopology_of_countablyMonolithicSpace`

`Homogeneous.countablyMonolithicSpace_card_lt`

`Homogeneous.monolithicSpace_exists_nhds_generated_countable`

TheoremKaplansky's problem on the values of the \(u\)-invariant #

`KaplanskyUInvariant.u_invariant_values`

`KaplanskyUInvariant.u_invariant_values.variants.kaplansky_conjecture`

`KaplanskyUInvariant.u_invariant_values.variants.not_three`

`KaplanskyUInvariant.u_invariant_values.variants.not_five`

`KaplanskyUInvariant.u_invariant_values.variants.not_seven`

`KaplanskyUInvariant.u_invariant_values.variants.two_pow`

`KaplanskyUInvariant.u_invariant_values.variants.even`

`KaplanskyUInvariant.u_invariant_values.variants.nine`

`KaplanskyUInvariant.u_invariant_values.variants.two_pow_add_one`

`KaplanskyUInvariant.u_invariant_values.variants.karpenko`

`KaplanskyUInvariant.u_invariant_values.variants.eleven`

`KaplanskyUInvariant.u_invariant_values.variants.odd`

`KaplanskyUInvariant.u_invariant_values.variants.thirteen`

`KaplanskyUInvariant.u_invariant_values.variants.fifteen`

TheoremKotzig's Conjecture #

`KotzigConjecture.kotzig_conjecture`

TheoremKurepa's conjecture #

`Kurepa.kurepa_conjecture`

`Kurepa.kurepa_conjecture.variants.prime`

`Kurepa.kurepa_conjecture.prime_reduction`

`Kurepa.kurepa_conjecture.variants.gcd`

`Kurepa.kurepa_conjecture.gcd_reduction`

TheoremConjectures about Latin Squares #

`LatinSquare.oddOrderLatinSquareTransversal`

`LatinSquare.oddOrderLeq9LatinSquareTransversal`

`LatinSquare.latinSquareOrder11Transversal`

`LatinSquare.latinSquareNearTransversal`

`LatinSquare.z_even`

`LatinSquare.numTransversalsZn`

`LatinSquare.growthRateZn`

`LatinSquare.maxTransversalsBound`

`LatinSquare.molsExistenceProblem`

`LatinSquare.molsOrder12`

TheoremLatin Tableau Conjecture #

`LatinTableau.SimpleGraph.LatinTableauConjecture`

TheoremLennon–Pittel conjecture on random stable matchings #

`LennonPittel.lennon_pittel_conjecture`

`ManickamMiklosSinghiConjecture.manickam_miklos_singhi_conjecture`

`ManickamMiklosSinghiConjecture.manickam_miklos_singhi_conjecture.variants.pokrovskiy`

`ManickamMiklosSinghiConjecture.manickam_miklos_singhi_conjecture.variants.quadratic`

`MonochromaticQuantumGraph.eqSystem4_no_solution_nnreal_ge4`

`MonochromaticQuantumGraph.eqSystem_no_solution_nnreal_even_ge6_ge3`

`MonochromaticQuantumGraph.eqSystem_no_solution_even_ge4_d_eq_n_explicit`

`MonochromaticQuantumGraph.eqSystem4_no_solution_d4`

`MonochromaticQuantumGraph.eqSystem4_no_solution_ge4`

`MonochromaticQuantumGraph.eqSystem6_no_solution_d3`

`MonochromaticQuantumGraph.eqSystem6_no_solution_d4`

`MonochromaticQuantumGraph.eqSystem6_no_solution_d5`

`MonochromaticQuantumGraph.eqSystem6_no_solution_d6`

`MonochromaticQuantumGraph.eqSystem6_no_solution_ge3`

`MonochromaticQuantumGraph.eqSystem8_no_solution_d3`

`MonochromaticQuantumGraph.eqSystem8_no_solution_d10`

`MonochromaticQuantumGraph.eqSystem10_no_solution_d3`

`MonochromaticQuantumGraph.eqSystem10_no_solution_d4`

`MonochromaticQuantumGraph.eqSystem10_no_solution_d5`

`MonochromaticQuantumGraph.eqSystem10_no_solution_d6`

`MonochromaticQuantumGraph.eqSystem10_no_solution_d7`

`MonochromaticQuantumGraph.eqSystem10_no_solution_d8`

`MonochromaticQuantumGraph.eqSystem10_no_solution_d9`

`MonochromaticQuantumGraph.eqSystem10_no_solution_d10`

`MonochromaticQuantumGraph.eqSystem12_no_solution_d3`

`MonochromaticQuantumGraph.eqSystem14_no_solution_d3`

`MonochromaticQuantumGraph.eqSystem16_no_solution_d3`

`MonochromaticQuantumGraph.eqSystem_no_solution_ge6_ge3`

`MonochromaticQuantumGraph.eqSystem4_no_solution_ge4_real`

`MonochromaticQuantumGraph.eqSystem6_no_solution_d3_real`

`MonochromaticQuantumGraph.eqSystem6_no_solution_d5_real`