Browse › Partial differential equations › 367 The critical dimension for the one-phase Bernoulli problem
The critical dimension for one-phase Bernoulli minimizers
Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion
Edit NOTES.md · Existing issues · Source on GitHub
Abstract
We prove that seven is the critical dimension for the one-phase Bernoulli problem: every nonzero one-homogeneous global minimizer in dimensions at most six is flat, while a nonflat one-homogeneous global minimizer exists in dimension seven. It follows that the interior free boundary of a local minimizer is smooth in dimensions at most six. In dimension n ≥ 7, its singular set has Hausdorff dimension at most $n-7$, and this bound is sharp. In dimension seven, the singular set is locally finite.
If the PDF does not display here, open it directly: Open PDF.
Notes
No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.
Automatically collected notes (unreviewed)
work in progress
Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-21) and not checked by a person. May be wrong or incomplete. Report an error.
Formalization
- OpenAI, The critical dimension for the one-phase Bernoulli problem — Lean scope note (OpenAI Math Release Lean docs, 2026-10-06). The release's own Lean development covers only the existence half of Theorem 1.1 (a nonflat one-homogeneous global minimizer in $\mathbb R^7$); flatness for $d\le6$ and the regularity and singular-set consequences are explicitly outside its scope. [family-level]
- William M. Feldman, one-phase-critical-dim: Lean 4 / Mathlib proof that one-homogeneous minimizers of the one-phase Bernoulli problem are flat in dimensions at most six (GitHub repository; Palomar entry PALOMAR-2026-10-14-000010 v1, 2026-10-14). Independent formalization of the flatness half ($1\le d\le6$) of Theorem 1.1 following the paper's certificate method, with new certificates for $d=3,4$; the README reports no
sorry, says the code was written by AI coding agents under the author's direction, and notes that no machine-checked bridge yet links it to the release'sGlobalMinimizerand that the singular-set corollary is not formalized. [AI-generated per source]
Related prior literature mentioned by others
- D. Kriventsov and G. S. Weiss, Rectifiability, finite Hausdorff measure, and compactness for non-minimizing Bernoulli free boundaries (arXiv:2306.10131, 2023). Cited in the README of the independent Lean formalization above as part of the background used there; not in the paper's bibliography.
- F. Abedin, W. M. Feldman and K. Stinson, Variational properties of Perron's extremal solutions in the Bernoulli one-phase problem (arXiv:2609.14981, 2026-09-14). Cited in the README of the independent Lean formalization above, one of whose pinned dependency libraries is a Perron/variational Bernoulli package by the same author.
Possibly relevant literature (found by the agent, not checked)
- N. Edelen and M. Engelstein, Quantitative stratification for some free-boundary problems (arXiv:1702.04325, Trans. Amer. Math. Soc. 2019). Proves rectifiability and measure bounds for the singular set of Alt–Caffarelli minimizers, which bears on the singular-set statements of Corollary 1.2 (dimension bound $n-7$, local finiteness for $n=7$).
- Giorgio Tortone and Bozhidar Velichkov, Vectorial Bernoulli Problems and Free Boundary Systems (La Matematica 5, article 16, 4 February 2026). Its Theorem 1.1 summarizes the dependence of one-phase singular-set bounds on the critical dimension, providing background for Corollary 1.2 and its specialization to critical dimension seven.
- C. Hines, J. Kolesar and P. McGrath, New Homogeneous Solutions for the One-Phase Free Boundary Problem (arXiv:2509.09409, 2025-09-11). Constructs new nonflat one-homogeneous solutions (including an infinite family in dimension four); Theorem 1.1 would imply none of these is a global minimizer in dimensions at most six.
Digests and expositions
- Expository note in the one-phase-critical-dim repository, The critical dimension of the one-phase Bernoulli problem: an expository account (Typst source with compiled
note.pdf, October 2026). Explains the structure of the flatness proof for $d\le6$ (reduction to smooth links, suspension from dimension five to six, stability inequality, finite algebraic certificate); the README says the expository notes were only partly reviewed by the author. [AI-generated per source] - Latent Seminar, The critical dimension of the one-phase Bernoulli problem (6 October 2026). Outlines the spherical Hessian, stability, exact tensor certificate and cutoff arguments, and states that it does not independently verify the complete proof or run the certificate engines. [family-level]
Elsewhere
- Palomar: Flatness of one-homogeneous one-phase Bernoulli minimizers in dimensions at most six (Lean formalization (formalizes))
- VibeMathed: Problem record
- Emergent Mind: family 367
Independent sites; their content is not reviewed here.
Cite
@misc{OAI:The-critical-dimension-for-one-phase-Bernoulli-minimizers-September-24-2026,
author = {{OpenAI}},
title = {{The critical dimension for one-phase Bernoulli minimizers}},
howpublished = {OpenAI Math Release preprint
\href{https://github.com/openai/math/blob/main/preprints/The-critical-dimension-for-one-phase-Bernoulli-minimizers-September-24-2026/The-critical-dimension-for-one-phase-Bernoulli-minimizers-September-24-2026.pdf}{OAI:The-critical-dimension-for-one-phase-Bernoulli-minimizers-September-24-2026}},
year = {2026}
}From OpenAI's README for this paper:
Verification
Use Python 3.10 or later on a little-endian POSIX system, with NumPy installed in that interpreter. From this paper directory, run the complete exact finite-certificate reproduction:
python3 -B verification/checks/reproduce.py
Success ends with PASS both full interior engines and all supporting checks.
For a bounded check of the pinned inputs and typeset tables without executing
the arithmetic engines, run:
python3 -B verification/checks/reproduce.py --verify-inputs-only
The existing integrity guard tests and deterministic appendix check are:
python3 -B verification/checks/test_reproduce.py
python3 -B verification/checks/generate_tables.py
The finite checks verify the supplied exact arithmetic and coefficient comparisons. They do not certify equivalence between mathematical formulas and code, or the analytic proof. The supported reproduction commands above use temporary copies and leave the supplied verification inputs unchanged.
Lean formalization
OpenAI provides Lean files for this family: lean/docs/367.md. The Lean statements have not been checked by people against the paper's claims.
Family 367: The critical dimension for the one-phase Bernoulli problem
Establishes seven as the first dimension admitting a nonflat, one-homogeneous global minimizer of the one-phase Bernoulli energy. Consequently, minimizing free boundaries are smooth through dimension six, and their singular sets have dimension at most $n-7$ in higher dimensions.
This is the only paper in this family.