The critical dimension for the one-phase Bernoulli problem

Claims seven is the critical dimension for one-phase Bernoulli minimizers, so free boundaries are smooth through six.

1 paper September 24, 2026 Explained by AI

The one-phase Bernoulli problem models a fluid region whose edge, the free boundary, is not fixed in advance. Minimizers can have corner-like singular points, which first appear in some critical dimension. De Silva and Jerison found a singular example in dimension seven, and Jerison and Savin ruled them out up to dimension four. This paper claims to rule them out in dimensions five and six, so seven is the critical dimension. Lean, a computer proof checker, has a formal statement only of the dimension-seven existence part.

First step

1981

Hans Wilhelm Alt and Luis Caffarelli, existence and regularity for the one-phase problem

Significance

Major

It claims the exact critical dimension for a central free-boundary problem, closing the gap between five and seven.

Trust

Formal proof listed

Field

Partial differential equations

1 paper

The explanation

Take the interval from −1 to 1. A nonnegative function u must equal 0 at −1 and 1 at 1. Its energy is the integral of its squared slope, plus the length where u is positive. Try u = 0 up to some point, then a straight ramp of length ℓ up to 1 at x = 1. The slope is 1/ℓ, so the energy is ℓ × (1/ℓ)² + ℓ = 1/ℓ + ℓ. With ℓ = 0.5 it is 2.5. With ℓ = 1 it is 2. With ℓ = 2 it is 2.5 again. The best choice is ℓ = 1, where the slope is exactly 1. The point where u becomes positive is the free boundary. Its position is not given; minimizing chooses it.

In space, the one-phase Bernoulli energy is the same: squared gradient plus the volume where u is positiveSource 1. The simplest minimizers are flat, u = (x · e)₊, a single ramp in one directionSource 2. Weiss's dimension reduction links singular points of minimizers to nonflat cones, minimizers that scale like u(rx) = r u(x)Source 3. So the key number is d*, the first dimension with a nonflat minimizing cone. Jerison and Savin showed d* ≥ 5. De Silva and Jerison built a nonflat minimizer in dimension seven, so d* ≤ 7Source 4.

The paper claims d* = 7. Every nonzero one-homogeneous global minimizer in dimensions one to six is flatSource 5. It follows that free boundaries of minimizers are smooth up to dimension six. In dimension n ≥ 7, the singular set has dimension at most n − 7, and this is sharpSource 6.

The obstacle is a stability test. Jerison and Savin explained why a simple power of the Hessian, the matrix of second derivatives, fails in dimensions four to sixSource 7. The paper builds a test function and a vector field together from the normalized HessianSource 8. A suspected cone in dimension five or six is reduced to a domain on the five-dimensional sphereSource 9. The needed inequalities are then checked by weighted sums of squares with exact rational boundsSource 10. Coefficient tables are listed in an appendix.

How sure is this? Lean, a computer proof checker, has a formal statement of only one part. That part says a nonflat minimizer exists in dimension seven, as De Silva and Jerison showed. The new flatness result in dimensions five and six is not in the Lean scope. It remains a claim. No specialist review is published.

What it doesn't show. This does not cover the two-phase problem or nonminimizing stable solutions. The Lean scope leaves out the new flatness result in dimensions up to six and the regularity consequences.

Where it came from

This result comes from an unreleased OpenAI model, published in the openai/math release on 6 October 2026.

Hype check

Major if the flatness proof holds: it would fix the critical dimension at seven. Lean covers only the dimension-seven existence part, which was already known. No specialist review is published.

Words used

Free boundary: The edge of the region where the solution is positive; its position is part of the unknown.
One-phase Bernoulli energy: The integral of squared gradient plus the volume where the function is positive.
Global minimizer: A function whose energy cannot be lowered by changing it inside any ball.
One-homogeneous: Scaling like u(rx) = r u(x), so the function is a cone.
Flat solution: A single ramp, u = (x · e)₊, whose free boundary is a plane.
Singular set: Free-boundary points where no zoom-in looks like a flat solution.
Hessian: The matrix of second derivatives of a function.

The original paper

The critical dimension for one-phase Bernoulli minimizers (PDF, opens in a new tab)
September 24, 2026

Lean notes

All quoted lines (10)

For a nonnegative function $v\in H^1(B)$ , where $B\subset\R^d$ is a ball, the one-phase Bernoulli energy is $J(v;B)=\int_B\bigl(|\nabla v|^2+\mathbf 1_{\{v>0\}}\bigr)\,dx.$
The critical dimension for one-phase Bernoulli minimizers Back to text
The nonzero flat solutions are $u(x)=(x\cdot e)_+,\qquad |e|=1.$
The critical dimension for one-phase Bernoulli minimizers Back to text
Weiss's monotonicity formula and dimension reduction connect the singularities of general minimizers to homogeneous global minimizers; see also.
The critical dimension for one-phase Bernoulli minimizers Back to text
In the other direction, De Silva and Jerison constructed a nonflat homogeneous global minimizer in dimension seven, proving $d_*\leq7$ .
The critical dimension for one-phase Bernoulli minimizers Back to text
Every nonzero one-homogeneous global minimizer of (…) in $\R^d$ , $1\leq d\leq6$ , is flat.
The critical dimension for one-phase Bernoulli minimizers Back to text
In dimension $n\ge7$ , its singular set has Hausdorff dimension at most $n-7$ , and this bound is sharp.
The critical dimension for one-phase Bernoulli minimizers Back to text
Jerison and Savin explain why this unweighted choice does not give a uniform instability criterion in dimensions four through six: the interior and boundary estimates impose different restrictions on the power, and their sharp configurations need not agree.
The critical dimension for one-phase Bernoulli minimizers Back to text
Our proof uses the normalized shape of the Hessian to construct both a scalar test and a separate vector field whose divergence controls the test's energy.
The critical dimension for one-phase Bernoulli minimizers Back to text
Thus both possible dimensions lead to a domain $\Omega\subset S^5$ with a smooth regular boundary and, possibly, these two tips (Section …).
The critical dimension for one-phase Bernoulli minimizers Back to text
We prove them by weighted sums of tensor squares and exact rational remainder bounds, with all coefficients and contraction conventions supplied in Appendix ….
The critical dimension for one-phase Bernoulli minimizers Back to text

Other sources

openai/math, Lean scope note for family 367 The linked formalization proves the existence side: in dimension seven there is a nonzero one-homogeneous global minimizer that is not a half-space solution.
openai/math release notes (2026): model provenance and review status manuscripts and supporting proof artifacts produced by an internal OpenAI model

366The planar Mumford–Shah regularity conjecture and local weak- L 4 gradient boundsPartial differential equations
365Joint metric and connection recovery from one boundary patchPartial differential equations
363Nonuniqueness with local conservation for the hard-sphere Boltzmann equationPartial differential equations
362Global smoothness for relativistic Vlasov–MaxwellPartial differential equations
368The three-dimensional Ball–Evans approximation problemPartial differential equations

Browse Partial differential equations Open since the 1980s Lean-checked results