The Hyperplane Separation Theorem (HST) is usually proved through the existence of a unique minimum-norm vector in a nonempty closed convex set. I think this is an existential proof which applies to infinite dimensional spaces.
However, to actually apply the result in a real world problem, one might need to find the actual numeric value of the minimum-norm vector through construction. Furthermore, constructivism is appreciated in mathematical economics and operation research mathematics.
Do we have a simple constructive proof for HST over $\mathbb R^n$ or a linear space?
Theorem: Let $C,D$ be two closed convex sets of a $\mathbb R^n$ that do not intersect. Then there exists a non-zero real vector $a$ such that $a\cdot c\geq a\cdot d$ for any $c\in C$ and any $d\in D$.
As an example for constructive proof I will refer to a simple proof of a very similar theorem, the von-Neumann–Morgenstern utility theorem:
vNM Theroem: Let $\succsim \subset X\times X\subset\mathbb R^n\times\mathbb R^n$. Let $\succsim$ be complete, transitive, continuous.
Let $\succsim$ also be convex: $(p,q)\in\succsim$ and $(l,m)\in\succsim$ implies $\alpha(p,q)+(1-\alpha)(l,m)\in\succsim$ for any $\alpha \in(0,1)$.
Then, there exists a real vector $A$ such that: $(l,m)\in\succsim \iff A\cdot l\geq A\cdot m$.
A simple constructive proof can be found here. I think that a very simple constructive proof also exists for HST.
