Papers With

← All papers
First page of Self-similar solutions for the gSQG patch equations

Self-similar solutions for the gSQG patch equations

Javier Gómez-Serrano, Marcus Pasquariello

math.AP Oct 23, 2026 · v2
formalization autoformalization mathlib analysis
Read PDF arXiv abstract Code
TL;DR
Main theorem on self-similar gSQG patch solutions is formally verified in Lean 4 with Mathlib, autoformalized by LLMs via a 553-node blueprint.
Abstract
The inviscid generalized surface quasi-geostrophic (gSQG) equations are a family of active scalar equations parametrized by a scalar $α$ that includes the two-dimensional Euler equations ($α= 0)$ and the SQG equation $(α= 1)$. We prove that, for every $α\in (\frac{7}{4}, 2)$ and every $T > 0$, there exists a self-similar patch solution whose boundary is a smooth, unbounded graph for $0 \leq t < T$ and develops a corner singularity at time $T$. The proof has been formally verified in Lean 4.
Problem

The question is whether the generalized surface quasi-geostrophic (gSQG) patch equations admit self-similar solutions whose smooth graph boundary develops a corner singularity in finite time. The target range is α in (7/4, 2).

Approach

The front equation is rewritten in self-similar variables. An approximate solution is built from the linearized equation using stationary-phase analysis. A fixed-point argument then closes the construction, relying on a conjugated linear inverse and nonlinear estimates in weighted spaces. The full proof was formalized in Lean 4 with Mathlib, autoformalized by LLMs (GPT-6 for the blueprint, Opus 5.5 for execution) over 4 refinement passes.

Results

For every α in (7/4, 2) and every T > 0, a self-similar patch solution exists with a smooth unbounded graph boundary that forms a corner at time T. The Lean blueprint has 553 nodes, all formally proved, and the code is in a public repository.