First, let me explain what I mean by "synthetic" in the title, which is a proof that reasons purely axiomatically and does not explicitly invoke local coordinate charts (either via concrete expansions or Penrose-style abstract tensor notation). For example in Euclidean geometry, one can either prove statements using Euclid's postulates or via vector arithmetic/Cartesian geometry. Euclidean proofs tend to be shorter and more elegant, but the arithmetical proofs tend to be easier to discover.

To better illustrate in the context of geodesic flow, this I shall now sketch out a basic non-synthetic (arithmetical) derivation for the geodesic equation. Given a compact, path-connected Riemannian manifold (M, g) and a pair of designated points A, B, find a path $\gamma : [0, 1] \to M$ to

Minimize: $\int \limits_0^1 g_{\gamma(t)}( \dot{\gamma}(t), \dot{\gamma}(t) ) dt$

Subject to: $\gamma(0) = A, \gamma(1) = B$

Now we construct a variation, $\gamma' : (-\epsilon, \epsilon) \times [0,1] \to M$ such that for all s, t, $\gamma'(0, t) = \gamma(t)$, $\gamma(s,0) = A$ and $\gamma(s, 1) = B$. So, a path $\gamma$ is an extremal if for all variations $\gamma'$,

$\left. \frac{d}{d s} \right|_{s = 0} \int \limits_0^1 g_{\gamma(s, t)}( \frac{d}{d t}\gamma(s, t), \frac{d}{d t}\gamma(s, t) ) dt = 0$

So far so good. Now at this point, the usual strategy is to fix a subinterval $(a, b) \subset [0,1]$ such that for all t in (a,b), $\gamma (t)$ is contained within a single coordinate chart, then expand the functional in terms of this basis and apply the Euler-Lagrange equations. If you do this, then lo-and-behold differentiating the metric gives you a second order term and the Christoffel symbols, which corresponds to the Levi-Civita connection. To extend this to a global result requires showing that the Euler-Lagrange equations agree across a boundary and that the metric is locally convex.

Now my question is can we do this last part synthetically? In other words, just using the basic properties of connections can we prove that this has to be an extremum of the length functional? I really would hope so, otherwise why go through all the trouble of defining connections axiomatically, just pick coordinates and Christoffel symbols and be done with it!