Real and complex analysis
16 families · 10 verified by lean
This page gathers the 16 result families that the openai/math repository catalogues under Real and complex analysis. Each claim comes from a manuscript; 10 of them have a Lean formalization checked by software, and the other 6 are still to be verified. Open any card to read a plain-language explainer, the original statement and its sources.
Koebe’s circle-domain conjecture
Resolves the existence part of Koebe's circle-domain conjecture: every domain in the Riemann sphere is conformally equivalent to a domain whose complementary components are round disks or points. It also proves that circle domains with conformally removable boundary are rigid, meaning every conformal equivalence to another circle domain is Möbius, establishing this direction of the He–Schramm conjecture.
Brennan's conjecture and the integral-means spectrum
Proves Brennan's conjecture: for every conformal bijection ϕ from a simply connected plane domain onto the disk, is area-integrable for . The sharp universal integral-means identity is for t ≤ −2. A strict bound for bounded univalent functions disproves Kraetzer's prediction at that parameter.
The Falconer distance conjecture
Resolves the Falconer distance conjecture in every dimension d ≥ 2: every compact set with Hausdorff dimension greater than determines a set of Euclidean distances of positive Lebesgue measure.
Kakeya in three and four dimensions
Resolves the Kakeya maximal conjecture in three dimensions and the Hausdorff-dimension conjecture in four. In three dimensions, the radius-δ tube maximal operator maps to with norm for every ε > 0. In four dimensions, every set containing a unit segment in every direction has Hausdorff dimension four.
The Fourier-convergence conjecture
Proves that the ordinary symmetric Fourier partial sums of every complex-valued function in converge almost everywhere along the full sequence. This resolves the classical sufficiency conjecture at the scale.
Real ultraflat Littlewood polynomials and unbounded binary merit factors
Constructs polynomials with N consecutive coefficients in whose modulus is uniformly on the entire unit circle, for every sufficiently large integer length N. Thus real Littlewood polynomials are ultraflat, including at the real endpoints. Their binary merit factors tend to infinity, disproving Turyn's bounded-merit-factor conjecture.
Fourier restriction for positively curved surfaces
Proves the diagonal Fourier extension conjecture for positively curved surfaces in three dimensions. For every compact smooth positively curved surface , including surfaces with boundary, the extension operator is bounded from to for every p > 3.
The three-dimensional Bochner–Riesz conjecture
Resolves the three-dimensional Bochner–Riesz conjecture in its strict range: the Bochner–Riesz multipliers of order δ are bounded on for every whenever .
Local smoothing in three dimensions
Resolves Sogge's local smoothing conjecture for the Euclidean wave equation in three spatial dimensions. The estimate holds throughout the full strict range , with Sobolev regularity above . In particular, the critical L3 estimate holds with every positive Sobolev loss.
The exact Sobolev endpoint for Schrödinger convergence
Proves almost-everywhere convergence as for every and every dimension n ≥ 2. This attains the sharp Sobolev equality case of Carleson's Schrödinger convergence problem, including the planar endpoint H1/3.
Riesz transforms and rectifiability in higher codimension
Resolves the remaining higher-codimension Riesz-transform rectifiability problem: for d ≥ 4 and , an n-Ahlfors–David regular Radon measure on ℝd is uniformly n-rectifiable whenever its n-dimensional Riesz transform is uniformly L2-bounded over all positive hard truncations. The rectifiability bounds depend only on dimension, regularity and operator bounds.
Annular variation and dyadic absolute bounds for the triangular Hilbert transform
Proves maximal and annular r-variation bounds, for every r > 2, from complex to . The maximal estimate controls both hard truncation endpoints and gives almost-everywhere and norm convergence. Pairing with a third input settles the triangular Hilbert transform estimate at the symmetric point.
Hilbert transforms along Lipschitz directions
Proves a uniform strong L2 bound for the planar Hilbert transform along any Lipschitz unit vector field, at integration lengths bounded by an absolute multiple of its reciprocal Lipschitz constant. The estimate is uniform over inner truncations and yields an L2-bounded principal-value operator, establishing Stein's weak-type conjecture at this short scale.
The geometric case of the Erdős similarity conjecture
For every fixed , constructs compact subsets of with measure arbitrarily close to one containing no translated and nontrivially dilated copy of , with dilations of either sign. This resolves the geometric-progression case of the Erdős similarity conjecture for every ratio.
Endpoint Sobolev regularity of centered disk averages
Resolves the planar centered-disk case of the Hajłasz–Onninen maximal-function regularity problem. For every real , the centered disk maximal function satisfies with an absolute constant. It belongs locally to and has a globally integrable weak gradient.
An L3 bound for the trilinear Hilbert transform
Proves that the principal-value trilinear Hilbert transform with shifts , , is bounded from to . This resolves the L3 exponent case of the standard conjecture for slopes 1, 2, 3.