Gao and Leung asked whether the uo-adherence of a sublattice of a Banach lattice must be order closed. Fremlin's problem asks whether a Banach lattice with a weakly Fatou norm must admit an equivalent lattice norm with the Fatou property.

For the first question, a C(K) space built from Solovay's complete Boolean algebra contains a separable norm-closed sublattice whose only order-closed sublattice extension is C(K) itself. For the second, finite-height trees and cylinder-set characteristic functions give spaces X_n that are weakly Fatou with constant 2, where iterated order adherence of the unit ball reaches norm 2^n. Their c_0-sum is the counterexample. All results are verified in Lean 4 using the banlat library on Mathlib, with large language models assisting the formalization.

The paper gives a negative answer to the Gao-Leung question and a self-contained counterexample showing that a weakly Fatou norm need not be equivalent to any Fatou norm. Each stated result links to a corresponding Lean declaration.