The Cayley–Bacharach theorem for plane cubics, formalised in Lean 4, with finite-field thresholds

We formalise the Cayley–Bacharach theorem for plane cubics in Lean 4 with Mathlib: underhypotheses made precise below, if two cubics meet in nine points, every cubic through eightof them passes through the ninth. We prove three versions. The first assumes that the eightpoints impose independent conditions on cubics; we prove the exact criterion for this, in bothdirections: no five of the points are collinear and the eight do not lie on a conic. The secondassumes that the two cubics have no common line or conic component. The third is the textbookform, in which the two cubics have exactly nine common zeros. None of the three assumes analgebraically closed field. The first two hold over every field. The third holds over every infinitefield and every finite field with at least eight elements. It is false over F4, F5 and F7; we giveexplicit counterexamples, checked by computer but not formalised. The line lemma behind allthree (a cubic vanishing on a line contains it) needs a field with at least three elements, and weformalise a counterexample over F2. As applications we derive Pascal’s and Pappus’s theoremsfrom Cayley–Bacharach under their natural incidence and distinctness hypotheses, for fieldswith more than ten elements. We also prove that a conic is a line pair if and only if its Gramdeterminant vanishes, over an algebraically closed field of characteristic different from two. Thedevelopment has about 3,600 lines and uses no sorry and no axioms beyond Lean’s standardthree. The mathematics is classical. We found no earlier formalisation of the theorem in thesources we searched (Section 8).