Question about the Lean formalization of the recent Navier–Stokes blow-up result: is compact support of the force postulated rather than proved?