The "extension" (or "analytic") form of the theorem of Hahn-Banach has a natural and yet elegant proof. In just any textbook I have ever seen, it is proved first; the "separation" (or "geometric") version of Hahn-Banach's theorem is proved as a kind of corollary of the former.
Question: Are the two theorems actually equivalent? If so, is any direct proof of the analytic version known that is instead based on the geometric one?
Yes, the two theorems are equivalent in the sense that one can easily be deduced from the other and both have direct proofs from scratch.
A standard textbook starting with a direct proof of the geometric version is Schaefer's Topological Vector Spaces, Chapter II, Section 3.
The statement Schaefer proves is:
Let $F$ be a subspace of a topological vector space $E$ and let $U$ be a nonempty open convex subset, disjoint from $F$. Then there is a closed hyperplane $H$ containing $F$ and disjoint from $U$.
The usual reductions via translation and taking the difference of the convex sets then yield the separation theorems of an open convex set from a point and of an open convex set from a compact convex set.
The proof starts by a simple geometric observation: Let $U$ be an open and convex subset of a Hausdorff topological vector space of dimension $\geq 2$. If $U$ does not contain $0$, then there is a one-dimensional subspace disjoint from $U$. This is easily reduced to the two-dimensional case, where it is rather clear.
To establish the above statement, a straightforward application of Zorn's lemma shows that there is a maximal (hence closed) subspace $M$ containing $F$ and disjoint from $U$. Since $U$ is non-empty, $E/M$ has dimension at least $1$. If the dimension of $E/M$ is $1$, then $M$ is a hyperplane and we're done. Suppose towards a contradiction that the dimension is at least $2$. The image of $U$ in $E/M$ does not contain $0$ and is open since the canonical projection $\pi \colon E \to E/M$ is open. Since $M$ is closed, $E/M$ is Hausdorff. Therefore there is a one-dimensional subspace $L$ of $E/M$ not meeting the image of $U$. The pre-image of $L$ contains $M$, is strictly larger and does not meet $U$, contradicting the maximality of $M$.
In order to get the analytic form, identify a linear functional on a subspace with its graph in $E \times \mathbb{R}$. Endow $E \times \mathbb{R}$ with the product topology induced by the sublinear functional $p$ and the usual topology on $\mathbb{R}$. The set $U = \lbrace (x,t) \mid p(x) \lt t\rbrace$ is an open convex cone in $E \times \mathbb{R}$, not containing $(0,0)$. A linear functional $f$ is dominated by $p$ iff $\operatorname{graph}(f)$ is disjoint from $U$. A maximal closed hyperplane $M$ containing $\operatorname{graph}(f)$ and disjoint from $U$ is then seen to be the graph of a linear functional $F$ which is obviously an extension of $f$ and dominated by $p$.
The separating version is ubiquitous in economics, and in my experience, most textbooks in mathematical economics prove it directly (though sometimes only in the finite dimensional case).
