{"id":"arxiv/2609.33033","url":"https://arxiv.org/abs/2609.33033","tags":["math.AP"],"score":0,"title":"Formalization of the Galerkin Construction for the Two-Dimensional Navier--Stokes Equations in Lean","domain":"math.AP","source":"arxiv","authors":["Weinan Wang"],"reviews":0,"subject":"math.AP","summary":"We formalize in Lean 4 the Galerkin construction of global Leray--Hopf weak solutions for the unforced two-dimensional Navier--Stokes equations on arbitrary bounded open domains with no-slip boundary conditions. For every initial datum in the solenoidal \\(L^2\\) velocity space, the solution has a weakly continuous velocity path, satisfies the weak equation locally in time, and obeys the energy inequality at every time. For rectangles, we also formalize finite-horizon solutions with continuous forcing in the dual energy space. The development includes divergence-free graph spaces, compact…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-09-27","reactions":{}}