Existence of global Leray–Hopf weak solutions for the unforced two-dimensional incompressible Navier–Stokes equations on bounded open domains with no-slip boundary conditions has not been formalized in a proof assistant.

The Galerkin construction is formalized in Lean 4, building divergence-free graph spaces (velocity–gradient closures), a bounded skew trilinear convection form, and compact spectral coordinates. A spectral compactness argument in space–time is developed instead of the Aubin–Lions–Simon lemma, combining Arzelà–Ascoli on finite projections with operator-norm approximation after a compact embedding. Finite-dimensional variational Galerkin solutions are extended to the full interval via an exact energy identity, and Ladyzhenskaya estimates control the transport term. Mathlib's closed-subspace and Lp theory provide the underlying Hilbert-space structure.

For every initial datum in the solenoidal L2 velocity space, a weakly continuous velocity path is obtained that satisfies the weak equation locally in time and obeys the energy inequality at every time. Finite-horizon solutions with continuous forcing in the dual energy space are also formalized for rectangles. The abstract Hilbert-space results apply to evolution equations with a compact energy-to-velocity embedding and a skew trilinear nonlinearity.