The Hyperplane Separation Theorem (HST) is usually [proved][1] 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 for all $(l,m)\in\succsim$, we have $A\cdot l\geq A\cdot m$.


The constructive proof can be [found here][2]. I think that a very simple constructive proof also exists for HST.


  [1]: https://www.princeton.edu/~aaa/Public/Teaching/ORF523/S16/ORF523_S16_Lec5_gh.pdf
  [2]: https://en.wikipedia.org/wiki/Von_Neumann%E2%80%93Morgenstern_utility_theorem#Proof_sketch