In 1974 C. D. Aliprantis posed open questions about topological completions of locally solid vector lattices. They ask whether properties known in the metrizable case (σ-Lebesgue, property (B, i), approximation by upper elements, regularity versus order density) hold without metrizability.

The authors construct Hausdorff locally convex-solid vector lattices that serve as counterexamples, built from spaces such as C(A_∞), c × ℝ^{A'} and c_0 × ℝ^{PS}. Each counterexample is formalized in Lean 4 using version v0.1.0 of banlat, a Banach lattice library that depends on Mathlib. The main theorem in each section links to its Lean declaration. Per the AI disclosure, GPT models generated most of the counterexamples and helped formalize them.

All five questions are answered in the negative. Without metrizability, neither the σ-Lebesgue property nor property (B, i) need pass to the completion, and a positive element of the completion need not be the limit of a decreasing sequence of upper elements. The generalized (A, 0) property need not make the canonical image regular, and regularity of that image need not imply order density. All five counterexamples are machine-checked in Lean.