# AI provenance: A counterexample to Liu's conjecture on Fano indices in dimension four

Authors: Deep Bhattacharjee (corresponding author, ORCID 0000-0003-0466-750X)
and Ushashi Bhattacharya (ORCID 0009-0002-2254-3914).

- Paper: https://github.com/creelie/fuzzy-guacamole/blob/main/preprintLiuFanoIndexConjecture/LiuFanoIndexConjecture.pdf
- Lean formalisation and code: doi:10.5281/zenodo.23387505 (release v2.0.0; all versions doi:10.5281/zenodo.23319498)
- Repository: https://github.com/creelie/fuzzy-guacamole

## Result

H. Liu (On Fano indices of weighted projective spaces, arXiv:2608.03434,
Conjecture 4.2) conjectured that in every dimension n ≥ 2 three sets of
integers coincide: the Fano indices of n-dimensional well-formed weighted
projective spaces with canonical singularities (together with 1, ..., n), the
indices of n-dimensional terminal Calabi–Yau varieties, and the indices of
n-dimensional log canonical singularities. Liu proved this for n ≤ 3. The
paper shows that it fails for n = 4: 1389 is the index of a terminal
Calabi–Yau fourfold and of a four-dimensional log canonical singularity that
is not klt, but it is not the Fano index of any canonical weighted projective
space of dimension four.

The proof has four steps:

- Lemmas 2.1 to 2.3: F = x0^77 x1 + x1^67 x2 + x2^7 x0 + x3^3 + x4^2 defines a
  quasi-smooth Calabi–Yau threefold X of degree 78 in P(1,1,11,26,39), and
  g = diag(ζ, ζ^1312, ζ^992, 1, 1), with ζ a primitive 1389th root of unity,
  preserves F, has determinant of order 1389 and multiplies the 3-form of X
  by its determinant.
- Proposition 3.1: (Z × E)/μ_1389, with Z → X a G-equivariant terminalization
  (Esser–Totaro–Wang) and E an elliptic curve with a point of order 1389, is a
  terminal Calabi–Yau fourfold of index 1389.
- Lemma 4.1 and Proposition 4.2: the cone {F = 0} in C^5 is log canonical and
  not klt (by a weighted blow-up), and its quotient by μ_1389 is a log
  canonical, non-klt singularity of index 1389.
- Lemma 5.1, Proposition 5.2 and Theorem 5.3: every a in Z_{>0}^5 with sum 1389
  has age_a(k) = 4 for some k in {2, ..., 1387}, so by Kasprzyk's criterion no
  well-formed P(a) of Fano index 1389 has canonical singularities.

## Who did what

Deep Bhattacharjee chose the problem, directed the work, set the format and
the target journal (Proceedings of the American Mathematical Society), and ran
the computations. Claude (Anthropic), used through Claude Code under his
direction, produced the following:

- the proofs;
- the Lean 4 formalisation and the certificate generator;
- the search programs in C, C++, Julia, Python and shell;
- the figures;
- the LaTeX text of the paper.

No other AI system took part.

## How the result is checked

- **Lean 4.34.1 with Mathlib.** The theorem `LiuIndex.not_mem_Iwps4` states
  1389 ∉ I_{4,wps}, with Kasprzyk's criterion as the definition of a canonical
  weighted projective space; `LiuIndex.exists_age_four` gives the witness k for
  every a with sum 1389. They rest on a certificate of 368,253 boxes of 8^4
  points, split into 4,022 statements, each proved by `decide +kernel`, so the
  kernel evaluates the checker; `native_decide` is not used, and a soundness
  theorem proves that a passing box has the required witnesses. Lean also
  proves Lemma 2.1 (weighted homogeneity, quasi-smoothness, well-formedness)
  and Lemma 2.2 (invariance of F, the order of det g, the fixed points of the
  powers of g). Every theorem depends only on the standard axioms propext,
  Classical.choice and Quot.sound. There is no `sorry`, `admit` or added
  axiom.
- **Independent programs.** Exhaustive searches in C, C++, Julia and Python
  run over 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 search at q = 1383 finds the canonical
  P(674, 461, 195, 35, 18), a control that the search can find one.
- **Workflows.** Every pull request regenerates the certificate and compares
  it with the committed files, builds the Lean project, checks the axioms,
  runs the four searches and builds the paper; the release workflow repeats
  the Lean check and the C and C++ searches before publishing.

## What is not claimed

- The paper refutes Liu's conjecture in dimension four. It says nothing new
  about dimensions two and three (proved by Liu) or about dimensions five and
  higher.
- Lean checks the finite part (1389 ∉ I_{4,wps}) and the algebra of F and g.
  Kasprzyk's criterion, the facts on weighted hypersurfaces (Iano-Fletcher),
  the equivariant terminalization (Esser–Totaro–Wang) and the singularity
  theory of Sections 2 to 4 are proved by hand in the paper or taken from the
  cited literature, because Mathlib has no weighted projective spaces,
  discrepancies or terminalizations.
- On 15 October 2026 the authors checked that Conjecture 4.2 still stands in
  version 3 of arXiv:2608.03434 and searched arXiv and the web; they found no
  earlier counterexample in dimension four. Liu's own list of the Fano indices
  of canonical weighted projective fourspaces (Zenodo 10.5281/zenodo.21806548)
  does not contain 1389, in agreement with the paper.