OpenAI claims the planar hot spots conjecture (Lean)

Your AI and this story

Key facts

• Claim (abstract, verbatim): ‘We prove the strict hot spots conjecture for smooth bounded simply connected planar domains. More precisely, every nonzero eigenfunction for the first positive Neumann eigenvalue has nonvanishing gradient in the interior, so all its global maxima and minima lie on the boundary. This holds even when the eigenvalue is multiple.’
• Context (paper §1): Burdzy and Werner’s 1999 counterexample with two holes and Burdzy’s 2005 one-hole example show that topology matters; ‘The simply connected planar conjecture is stated explicitly in [Bur05, Conjecture 1.2(ii)].’ Earlier positive cases: convex domains with two axes of symmetry (Jerison–Nadirashvili), lip domains (Atar–Burdzy 2004), all triangles (Judge–Mondal), nearly circular convex domains (Miyamoto)
• Method (paper §1): the starting point is ‘Rohleder’s variational principle for tangent vector fields’. Scalar boundary multipliers are constructed ‘through a reciprocal Green-kernel theorem’, using McCullough and Quiggin’s characterization of complete Nevanlinna–Pick kernels and Schoenberg’s squared-distance embedding. An interior critical point ‘would thus produce too many eigenfunction gradients’
• Lean: comparator challenge HotSpots.lean (OAI.StrictHotSpots.main_theorem) covers nonempty bounded open simply connected planar sets with smooth boundary. It defines the first positive Neumann value as the infimum of mean-zero Rayleigh quotients and takes eigenfunctions in weak form; smoothness of the eigenfunction up to the boundary is a hypothesis, which MathVet lists among definitions to check. Accepted in the oai-math-revised comparator run of 25–26 Oct; MathVet verdict ‘full’, with a sandboxed comparator pass
• Follow-ups that use the theorem as an unchecked input: Burdzy (arXiv 2610.12622, 8 Oct; ‘The paper was generated by ChatGPT with prompts from the listed author’) obtains non-strict hot spots on every bounded simply connected planar domain with compact Neumann resolvent and a simple eigenvalue, and writes: ‘We take this assertion as an input and do not assess or reproduce its proof.’ Rodrigo Bañuelos (2610.32920, 23 Oct) proves the same for domains of finite area and adds examples with cusps and unbounded domains; his Section 1 ‘was generated entirely by ChatGPT (6.1 Sol) in response to a few human prompts’. Jizhou Guo (GitHub preprint, 10 Oct) deduces boundary extrema for every convex planar domain, polygons included
• Criticism (Burdzy’s human commentary, 2610.12622): ‘The OpenAI model that generated [3] missed the theorem presented in this note’, and ‘It is highly surprising that [3] did not cite the spectacular paper of de Dios Pont [2], which shows that the hot spots conjecture fails for convex domains in high dimensions’
• Specialists cite it without assessing it. Atar and Burdzy (2610.19908, 14 Oct, a starlike 3D counterexample): ‘More recently, OpenAI [18] presented a proof for smooth simply connected planar domains.’ Deng, Jiang and Yang (2610.18546, 13 Oct, no AI statement) prove that on every bounded convex planar domain the maximum modulus is attained only on the boundary, and write that OpenAI ‘stated a theorem’. Deng, Gui, Jiang, Yang, Yao and Zou (2604.19003v4) note that OpenAI’s ‘setting, however, excludes polygonal domains with corners’
• Reactions: on Proofs and Prompts (8 Oct), in a reaction signed ‘Mitchell Taylor’ (the page lists no affiliations): ‘In particular, I am happy to see that the hot spots conjecture is true for simply connected subsets of the plane’. AIM (Matthew Colbrook’s tracker) marks problem 003, hot spots on smooth convex planar domains, SOLVED, after what it calls an AI statement-level comparison, not an audit of the proof