AI results
This page collects results obtained with the help of AI.
- Normality of smooth lattice three-polytopesA complete proof that every smooth three-dimensional lattice polytope is normal.
- Fourteen points in three-spaceA proof that every finite subscheme of A3 of degree at most 14 is smoothable; equivalently, the Hilbert schemes of 12, 13 and 14 points in A3 are irreducible. The whole result, degree at most 14, is formally verified in Lean. Degrees 15 to 19 are treated in the sequel below.
- Nineteen points in three-spaceA proof that every finite subscheme of A3 of degree at most 19 is smoothable; equivalently, the Hilbert schemes of at most 19 points in A3 are irreducible. Sequel to Fourteen points in three-space. Compared with that case, the new ingredient is linkage: a finite scheme lying in a complete intersection of less than twice its length is smoothable if all shorter schemes are. Degrees up to 16 are formally verified in Lean. The computations cited in the paper are in the accompanying archive; its script
VERIFY.shreruns all of them in a few minutes. Degree 20 is treated in the sequel below. - Twenty points in three-spaceA proof that every finite subscheme of A3 of degree at most 20 is smoothable; equivalently, the Hilbert scheme of 20 points in A3 is irreducible, so a reducible Hilbert scheme of points in A3 needs at least 21 points. Sequel to Nineteen points in three-space. In degree 20, linkage needs a complete intersection of local length at most 39; the new tools bound such lengths by a computation on the blow-up of the origin, by a weighted Bézout theorem, and by prescribing three equations of the scheme through the free tails of its inverse system. The computations cited in the paper are in the accompanying archive; its script
run_all.shchecks every file against the listed checksums and reruns the computations in about twenty minutes with four parallel processes. - The exponent of matrix multiplication is less than 2.37116A proof that the exponent of matrix multiplication satisfies ω ≤ 2.371159796228 < 2.37116. The bound 2.371177 of Dupont et al. comes from a feasible point of an optimisation problem that encodes the analysis of Alman, Duan, Vassilevska Williams, Xu, Xu and Zhou; the paper gives a better point of the same problem and proves its feasibility by computation, with two independently written programs. The archive contains the point and both programs; its script
verify.shchecks the feasibility of the point in about seven minutes. - Fast multiplication of large matrices: implementationsPrograms for multiplying large matrices (single precision, multicore CPUs) in three variants: accurate (error at or below that of the vendor library, still faster than it), safe, and fast (much faster, somewhat larger error). The ideas of what to implement are mine; there is no new theory, and everything used is publicly known.