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 eight ofthem passes through the ninth. We prove three versions. The first assumes that the eight pointsimpose independent conditions on cubics; we prove the exact criterion for this, in both directions:no five of the points are collinear and the eight do not lie on a conic. The second assumes that thetwo cubics have no common line or conic component. The third is the textbook form, in whichthe two cubics have exactly nine common zeros. None of the three assumes an algebraicallyclosed field. The first two hold over every field. The third holds over every infinite field, and afinite field K exactly when |K| /∈ {4, 5, 7}: we prove it for every other finite field, and it is falseover F4, F5 and F7, for which we give explicit counterexamples, checked by computer but notformalised. The line lemma behind all three (a cubic vanishing on a line contains it) needs afield with at least three elements, and we formalise a counterexample over F2. As applicationswe derive Pascal’s and Pappus’s theorems from Cayley–Bacharach under their natural incidenceand distinctness hypotheses, for fields with more than ten elements. We also prove that a conicis a line pair if and only if its Gram determinant vanishes, over an algebraically closed field ofcharacteristic different from two. The development has about 3,600 lines and uses no sorry andno axioms beyond Lean’s standard three. The mathematics is classical. We found no earlierformalisation of the theorem in the sources we searched (Section 8).