# Affine Bernstein rigidity through dimension nine and a smooth dimension-ten counterexample

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [The affine Bernstein theorem in dimensions three through nine](../../preprints/The-affine-Bernstein-theorem-in-dimensions-three-through-nine-September-24-2026/main.pdf)

## Scope

The formalization proves the Euclidean-complete affine Bernstein theorem for graph dimensions $3\le n\le9$. If a smooth function on a nonempty open convex domain has positive-definite Hessian, satisfies the affine maximal equation, and its graph is complete in the induced Euclidean metric, then the domain is all of $\mathbb R^n$ and the function is a positive-definite quadratic polynomial plus an affine term. Its graph is therefore an elliptic paraboloid.

The paper's extension to immersed hypersurfaces without an initial graph assumption is outside this selected statement.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Affine Bernstein classification for complete graphs in dimensions three through nine | [AffineBernstein.lean](../ComparatorChallenges/AffineBernstein.lean) |