A counterexample to Liu's conjecture on Fano indices in dimension four

Introduction

We work over $\mathbb{C}$. For a well-formed weighted projective space $\mathbb{P}(a_0,\ldots,a_n)$ with canonical singularities, the Fano index is $q=a_0+\cdots+a_n$. The index of a Calabi–Yau variety $S$ (a normal projective variety with $K_S\sim_{\mathbb{Q}}0$) is the least $m\ge1$ with $mK_S\sim0$, and the index of a log canonical singularity $P\in Y$ is the least $m\ge1$ such that $mK_Y$ is Cartier at $P$. Following [7 Definition 4.1], let

• $I_{n,\mathrm{wps}}$ be the set of Fano indices of $n$-dimensional well-formed weighted projective spaces with canonical singularities, together with $\{1,\ldots,n\}$;

• $I_{n,\mathrm{term}}$ be the set of indices of $n$-dimensional terminal Calabi–Yau varieties;

• $I_{n,\mathrm{loc}}$ be the set of indices of $n$-dimensional log canonical singularities.

Liu proves the conjecture for $n\le3$ [7 Proposition 4.3] and computes $I_{4,\mathrm{wps}}$ by an exhaustive search [7 Theorem 4.4], [8].

The two memberships come from a symmetry of order 1389 of one Calabi–Yau threefold, the hypersurface $X_{78}$ of $\mathbb{P}(1,1,11,26,39)$ (§ 2–§ 4). The nonmembership is a finite statement about the 1,301,769,806 partitions of 1389 into five parts (§ 5). It is proved in the Lean 4 kernel from a certificate of witnesses, together with the polynomial identities of § 2 (§ 6). Figure 1 shows the plan of the proof.

Image not extracted

Remark 1.3. Read literally, $I_{4,\mathrm{loc}}$ contains every positive integer: for $m\ge2$ the group $\mu_m$ acting on $\mathbb{C}^4$ with weights $(1,1,1,m-2)$ is free in codimension one, so $\mathbb{C}^4/\mu_m$ is klt, and $\mathrm{d}x_1\wedge\cdots\wedge\mathrm{d}x_4$ has weight $m+1\equiv1\pmod m$, so its index is $m$ (by the argument in the proof of Proposition 4.2). Since $3487\notin I_{4,\mathrm{wps}}$ by [7 Theorem 4.4], the literal reading fails at once, and the intended reading of $I_{n,\mathrm{loc}}$ concerns log canonical singularities that are not klt. The singularity of Proposition 4.2 is log canonical and not klt, so Theorem 1.2 holds for both readings.

The threefold

Let $w=(w_0,\ldots,w_4)=(1,1,11,26,39)$ and

Proof. (1) and (2) are direct. For (3), let $x$ be a common zero; then $x_3=x_4=0$. With $\partial_i=\partial F/\partial x_i$,

since $x_0\partial_0=77x_0^{77}x_1+x_2^7x_0$, $x_1\partial_1=x_0^{77}x_1+67x_1^{67}x_2$ and $x_2\partial_2=x_1^{67}x_2+7x_2^7x_0$. Hence $x_2^7x_0=0$. If $x_2=0$, then $\partial_1=x_0^{77}$ and $\partial_2=x_1^{67}+7x_2^6x_0$ give $x_0=x_1=0$. If $x_0=0$, then $\partial_0=x_2^7$ gives $x_2=0$ and $\partial_2$ gives $x_1=0$. □

Let $C = \{F = 0\} \subset\mathbb{A}^{5}$ and $X = \{F = 0\} \subset\mathbb{P} = \mathbb{P}(1,1,11,26,39)$. By Lemma 2.1, $X$ is a quasi-smooth hypersurface of degree $78$; $\mathbb{P}$ and $X$ are well formed [4 6.10]. Hence $X$ has cyclic quotient singularities and $\omega_X \cong\mathcal{O}_X(78-\sum w_i) = \mathcal{O}_X$ [4 6.14]. Quotient singularities are klt [6 5.20], and the discrepancies of a klt variety with Cartier canonical divisor are integers, so $X$ is a canonical Calabi–Yau threefold with $K_X \sim0$.

Fix a primitive $1389$th root of unity $\zeta$ and put $g = \operatorname{diag}(\zeta,\zeta^{1312},\zeta^{992},1,1)$.

Proof. (1) The monomials $x_0^{77}x_1$, $x_1^{67}x_2$, and $x_2^{7}x_0$ acquire the factors

(2) $1389 = 3\cdot463$ and $2305 = 5\cdot461$ are coprime. (3) The integers $1$, $1312 = 2^{5}\cdot41$ and $992 = 2^{5}\cdot31$ are prime to $1389$, so $\zeta^k$, $\zeta^{1312k}$ and $\zeta^{992k}$ differ from $1$. □

The matrix $g$ commutes with the $\mathbb{C}^{*}$-action $t\cdot x = (t^{w_0}x_0,\ldots,t^{w_4}x_4)$, so $G = \langle g\rangle\cong\mu_{1389}$ acts on $C$, on $\mathbb{P}$ and on $X$. Let $\sigma$ be the Poincaré residue of $dx_0\wedge\cdots\wedge dx_4/F$ along $C$; it generates $\omega_C$, and $g^{*}\sigma= \det(g)\,\sigma$ by Lemma 2.2(1).

Proof. Let $\xi= \sum w_i x_i \partial/\partial x_i$ and let $\rho\colon C\setminus\{0\}\to X$ be the quotient map. The $3$-form $\iota_{\xi}\sigma$ is $\mathbb{C}^{*}$-invariant, since $\sigma$ has weight $\sum w_i-78=0$, and $\iota_{\xi}\iota_{\xi}\sigma=0$. Let $X^\circ\subset X$ be the open set over which $\rho$ is a principal $\mathbb{C}^{*}$-bundle; its complement has codimension at least $2$ because $X$ is well formed. On $X^\circ$ there is a nowhere vanishing $3$-form $\tau$ with $\rho^{*}\tau=\iota_{\xi}\sigma$. As $\omega_X$ is reflexive, $\tau$ is a nowhere vanishing section of $\omega_X\cong\mathcal{O}_X$, so it spans $H^0(X,\omega_X)$. Since $g$ commutes with $\xi$ and with $\rho$, $g^{*}\tau=\det(g)\,\tau$. □

A terminal Calabi–Yau fourfold of index 1389

A log canonical singularity of index 1389

Proof. By Lemma 2.1(3), $C$ is a hypersurface whose only singular point is $0$, so $C$ is Gorenstein and, by Serre’s criterion, normal; its local ring at $0$ is a domain, so $C$ is irreducible and no coordinate $x_j$ divides $F$.

Let $B \to\mathbb{A}^{5}$ be the weighted blow-up of $0$ with weights $w$. It is covered by the charts $U_i = \mathbb{A}^{5}/\mu_{w_i}$, where $\varphi_i: \mathbb{A}^{5}_{y} \to\mathbb{A}^{5}_{x}$ is $x_i = y_i^{w_i}$, $x_j = y_j y_i^{w_j}$ ($j \ne i$), and $\epsilon\in\mu_{w_i}$ acts by $y_i \mapsto\epsilon y_i$, $y_j \mapsto\epsilon^{-w_j}y_j$. Quasi-homogeneity gives $F \circ\varphi_i = y_i^{78}F_i$, where $F_i$ is $F$ with $x_i$ replaced by $1$ and $x_j$ by $y_j$; it does not involve $y_i$. Let $S_i = \{F_i = 0\}$ in the coordinates $y_j$, $j \ne i$. If $F_i$ and its derivatives vanish at $u$ (with $u_i = 1$), the Euler identity $78F = \sum w_jx_j\partial_jF$ gives $\partial_iF(u) = 0$, contradicting Lemma 2.1(3); so $S_i$ is smooth. The strict transform $W$ of $C$ is covered by $W_i = V_i/\mu_{w_i}$ with $V_i = \mathbb{A}^{1}_{y_i} \times S_i$, and the exceptional divisor $E_W = W \cap\pi^{-1}(0)$ is covered by $D_i/\mu_{w_i}$ with $D_i = \{0\} \times S_i$.

The action of $\mu_{w_i}$ on $V_i$ is free in codimension one. A non-identity $\epsilon$ fixes no point with $y_i \ne0$. Its fixed points in $D_i$ satisfy $y_j = 0$ for some $j \ne i$ with $\epsilon^{w_j} \ne1$, which exists because the $w_j$ with $j \ne i$ are coprime; and $\{y_j = 0\}$ contains no component of $S_i$ because $x_j \nmid F$. Hence $q_i: V_i \to W_i$ is étale in codimension one, $q_i^*K_{W_i} = K_{V_i}$ and $q_i^*E_W = D_i$. The pair $(V_i,D_i)$ is a smooth variety with a smooth divisor, hence log canonical, so $(W,E_W)$ is log canonical by [6 5.20].

The Jacobian of $\varphi_i$ is $w_i y_i^{\sum w_j-1}$, so

and the pullback of $\sigma$ to $V_i$ is $w_i y_i^{-1}$ times a generator of $\omega_{V_i}$. Thus the pullback of $\sigma$ to $W$ is a rational section of $\omega_W$ with divisor $-E_W$, that is, $K_W + E_W = \psi^*K_C$ for $\psi: W \to C$. By [6 Lemma 2.30], every divisor over $C$ has the same discrepancy for $C$ as for $(W,E_W)$. So $C$ is log canonical, and $E_W$ has discrepancy $-1$, so $C$ is not klt. □

Image not extracted

Proof. By Lemma 2.2(3), the fixed locus of $g^k$ on $C$ for $0<k<1389$ lies in the curve $\{x_0=x_1=x_2=0,\ x_3^3+x_4^3=0\}$. So $p:C\to Y$ is étale in codimension one, $K_C=p^*K_Y$, and $Y$ is log canonical and not klt by Lemma 4.1 and [6 5.20].

For $m\geq1$, the sections of $\mathcal{O}_Y(mK_Y)$ near $P$ are the $G$-invariant sections of $\omega_C^{\otimes m}$, that is, $f\sigma^m$ with $g^*f=\det(g)^{-m}f$. If $1389\mid m$, then $\sigma^m$ is invariant and generates. Conversely, if $mK_Y$ is Cartier at $P$ with generator $f\sigma^m$, then $f(0)\neq0$, and $g(0)=0$ gives $f(0)=\det(g)^{-m}f(0)$, so $1389\mid m$ by Lemma 2.2(2). □

Weighted projective spaces of Fano index 1389

For $a=(a_0,\ldots,a_4)\in\mathbb{Z}_{>0}^5$ with $q=\sum a_i$ and $k\in\mathbb{Z}$, put

By Kasprzyk's criterion [5 Proposition 2.5], a well-formed $\mathbb{P}(a)$ has canonical singularities if and only if $\operatorname{age}_a(k)\in\{1,2,3\}$ for every $k\in\{2,\ldots,q-2\}$.

Image not extracted

Proof. Order the weights so that $a_0\geq a_1\geq\cdots\geq a_4$. Then $2a_1+a_2+a_3+a_4\leq a_0+\cdots+a_4=1389$. Proposition 5.2 gives $k\in\{2,\ldots,1387\}$, and Lemma 5.1 gives $\operatorname{age}_a(1389-k)=4$ with $1389-k\in\{2,\ldots,1387\}$. Kasprzyk’s criterion excludes canonical singularities, and $1389>4$. □

Proof of Theorem 1.2. Combine Propositions 3.1 and 4.2 with Theorem 5.3. □

Remark 5.4. Since $\varphi(1389)=924\leq984$, the number 1389 lies in the set $\{m:\varphi(m)\leq984\}$ that contains $I_{4,\mathrm{wps}}$ by [7 Theorem 4.4]; it is one of the elements of the set $J_4$ of [7 Section 4]. Theorem 5.3 agrees with the list [8]. The neighbouring index 1383 lies in $I_{4,\mathrm{wps}}$: $\mathbb{P}(674,461,195,35,18)$ is well formed and passes Kasprzyk’s criterion.

Formal verification

The finite and algebraic parts of the proof are formalized in Lean 4 with its mathematical library [9, 2]. In the formalization the set $I_{4,\mathrm{wps}}$ is defined as the union of $\{1,2,3,4\}$ with the sums $\sum a_i$ over the well-formed $a\in\mathbb{Z}_{\geq0}^5$ that satisfy Kasprzyk’s criterion. The formal statements are Lemma 2.1, Lemma 2.2, Proposition 5.2, the first part of Theorem 5.3, and the statement $1389\notin I_{4,\mathrm{wps}}$. The kernel checks every proof, and each of these theorems depends only on the axioms of propositional extensionality, choice and quotient soundness.

The certificate of Proposition 5.2 is split into 4,022 statements, each asserting that the checker accepts one list of boxes. Each statement is closed by evaluating the checker in the kernel, so no compiled code is trusted; checking all of them takes about 15 minutes on four cores. The steps that rest on the literature, namely Kasprzyk’s criterion, the results of [4] and [3], and the singularity theory of § 2–§ 4, are proved in the text and not formalized, since the library does not yet contain weighted projective spaces or discrepancies.

Independently of the formalization, programs in C, C++, Julia and Python enumerate all 1,301,769,806 partitions of 1389 into five parts, test Kasprzyk’s criterion on the 874,763,737 well-formed ones, and find no canonical one. The same enumeration for $q = 1383$ finds $\mathbb{P}(674, 461, 195, 35, 18)$.

Acknowledgements

The authors used the generative AI tool Claude (Anthropic), through Claude Code, to assist with the proofs, the Lean formalization, the computations and the preparation of this article. The authors reviewed and edited the content and take full responsibility for it.

Competing interests

None.

Funding

None.

Data availability

Deep Bhattacharjee computed the Lean formalization and the Julia, C, C++ shell and Python computations with the help of AI assistance (Claude, Anthropic). The Lean formalization of the finite and algebraic parts of the proof, together with the certificate generator and the search programs, is archived at Zenodo [1], doi:10.5281/zenodo.23387505. The paper is available at https://github.com/creelie/fuzzy-guacamole/blob/main/preprintLiuFanoIndexConjecture/LiuFanoIndexConjecture.pdf.

Formerly, Electro-Gravitational Space Propulsion Laboratory (EGSPL), Bhubaneswar, Odisha 751030, India

Email address: [email protected]

Email address: [email protected]

Formerly, National Taiwan University, Taipei 106319, Taiwan

Email address: [email protected]