The Pompeiu problem

Read formalization.yaml

authors

Jaume de Dios Pont, OpenAI Codex

method

agent — GPT-5

review

agent-reviewed (OpenAI Codex mathematical referee agent, OpenAI Codex Lean/API referee agent, OpenAI Codex OriginSeries and interface-sign referee agents)

axioms

Classical.choice, Quot.sound, propext

sorry

3 unproved goals declared

results

5 main results named, with an alignment table

sources

Modular proof draft for a planar Schiffer counterexample

divergences

This is not a line-by-line translation of a pre-existing published proof: the large-N proof manuscript, its corrected density/landing argument, and the Lean formalization were co-developed. The manuscript often uses anisotropic Holder spaces and states C2,alpha boundary regularity plus interior smoothness; the public Lean comparator currently claims the classical counterexample at C2 regularity and does not claim C2,alpha or C-infinity interior regularity. The construction-native SchifferCandidate separately records star-convexity and simple connectedness, while the plain comparator states star-shapedness, which implies contractibility but does not repeat the simple-connectedness field. The comparator normalizes the positive eigenvalue to 1 by dilation and strengthens the Neumann boundary condition to vanishing of the full Frechet derivative. The formal proof uses weighted l1 Fourier sequences, continuous radial jets, quantitative parametric contraction, and reusable Lyapunov--Schmidt splitting rather than a black-box Nash--Moser theorem. It proves tip and interface regularity directly from integer-order Bessel power series and one-sided Cartesian jets, without invoking general ell

checked by

nobody independent of its authors yet