Hyperplane anti-Bertini embeddings over finite fields
Yutong Zhang, Yaoran Yang
math.AG
Jun 22, 2026 · v1
TL;DR
Authors developed Lean 4 formalizations of selected proof components, with GPT-based assistance via the CSSC framework, released in a public repository.
Abstract
Baker asked, as recorded by Poonen, whether a fixed smooth quasiprojective variety over a finite field must have a smooth rational hyperplane section after every sufficiently high-dimensional linearly nondegenerate embedding. Poonen predicted a negative answer for every positive-dimensional variety. We prove this predicted negative answer for each prescribed variety: if $X$ is nonempty, smooth, quasiprojective, and of pure positive dimension over $\F_q$, then for every sufficiently large $N$ there is a locally closed embedding $X\hookrightarrow\PP^N_{\F_q}$ whose components remain linearly nondegenerate after arbitrary scalar extension, but whose every $\F_q$-rational hyperplane section is singular. The construction assigns one closed point of $X$ to each rational hyperplane and forces the pulled-back linear form to have zero first-order jet at that point.
Problem
Baker asked whether a fixed smooth quasiprojective variety over a finite field must have a smooth rational hyperplane section after every sufficiently high-dimensional nondegenerate embedding. Poonen predicted a negative answer for every positive-dimensional variety.
Approach
For a prescribed variety X, the construction assigns one closed point of X to each F_q-rational hyperplane. It then builds coordinates in two blocks: a shielded block and an anti-code block built from first-order local codes. These force the pulled-back linear form to have zero first-order jet at the assigned point while keeping the map an embedding. Selected proof components were formalized in Lean 4 with AI assistance.
Results
For every sufficiently large N there is a locally closed embedding of X into P^N that is componentwise linearly nondegenerate after any scalar extension, yet every rational hyperplane section is singular. This answers Baker's question negatively for every prescribed positive-dimensional X.
