Here is available a very rough work-in-progress. I've let the idea rest for seventeen months. It's difficult to illustrate the idea in python, and there appears no application of python to Alexandrov geometry yet.

What is Alexandrov geometry?

Introductions and references are available from Alexander, Kapovitch, Petrunin. The subject is notoriously difficult. The original paper of Burago, Gromov, Perelman is still useful.

An Alexandrov space $(X,d)$ is a fat and round metric space, like a sphere or cube but possibly with corners and sharp angles, and where triangles are fat. Examples include: convex sets $C$, the boundaries of convex sets $\partial C$, affine space $\mathbf{R}^d$. There are several important metric constructions by which spaces with curvature bounded below ($CBB[\kappa]$ in the notation of AKP).

We are interested in the singular mm-spaces, so we use the synthetic definition of sectional curvature and not necessarily the Gaussian definition of differential Riemannian geometry. Alexandrov spaces have sectional curvature $\kappa \geq 0$, which implies that every geodesic triangle $\Delta(a,b,c)$ in $X$ is fatter than the comparison triangle $\tilde{\Delta}$ in $\mathbf{R}^2$.

In Alexandrov geometry, geodesics frequently focus and collide. Initially geodesic rays might appear to be orthogonal, but at a not-too-faraway time, the rays will focus and converge back to a point. After this refocussing the geodesics might or might not diverge again to infinity. Positive sectional curvature tends to manifest in general relativity spacetimes, where the presence of mass (attractive matter) tends to cause light rays to focus and converge.

Our goal is a general method for constructing the souls of singular finite-dimensional Alexandrov spaces.

The original result on souls was achieved by G. Perelman (1994), building on the work of Gromoll, Meyer, Cheeger. Perelman's result in the Riemannian setting was that the souls $S$ of Riemannian Alexandrov spaces $(X,g)$ had the property that: $X$ was diffeomorphic to the normal bundle of $S$.

So what remains to be proved in the singular setting?

On a singular Alexandrov space, the space of directions at every point is isometric to an Alexandrov space of curvature $\kappa \geq 1$. The metric distance on the space of directions $\Sigma_p X$ at a point $x$ is defined by the angle between the directions. Alexandrov spaces (curvature bounded below by zero) have well-defined angles and directions. For almost all points, this space of directions is isometric to a $d-1$ dimensional sphere $\mathbf{S}^{d-1}$. This is well-known regularity property of Alexandrov spaces, namely that almost all points are regular. This is analogous to the fact in convex analysis that proper lower semicontinuous convex functions are differentiable almost everywhere.

The real challenge in the singular setting is to define gradient flows which are naturally defined and extend through the singular points.

Python and Alexandrov?

Our approach to mathematics is based on discovery. So instead of trying to prove everything a priori, we prefer to experiment and discover what is true. But how to use python to study Alexandrov spaces? It's not clear...

There are many analogies between lsc (lower semicontinuous) proper convex functions $f: \mathbf{R}^d \to \mathbf{R} \cup \{+\infty\}$ and Alexandrov spaces. For example, the regularity of Alexandrov spaces follows from the fact that: lsc proper convex functions are differentiable almost-everywhere on their domain. This is because the gradient $D f$ is Lipschitz on its domain, and therefore differentiable almost-everywhere. Therefore $f$ is even twice-differentiable almost everywhere on its domain.

Similarly, if an Alexandrov space contains a doubly-ended geodesic ray, then the Splitting theorem says $X=\mathbf{R}^1 \times X_0$ where $X_0$ is again Alexandrov. For convex lsc proper functions, the analogous fact is this: if the graph of the derivative $Df$ contains a double ended straight line, then up to a change of variable, $f$ can be factored as $f=\ell(x_1) + f_0(x_2, \ldots, x_d)$ where $\ell$ is affine and $f_0$ is a convex function which only depends on the remaining variables $x_2, \ldots, x_d$. (There may be slight error here, but this is essentially the idea as i learned from Prof. R.J. McCann.)

But the proper lsc convex functions are something like the local theory of Alexandrov spaces. For example, a difficult result in the foundations of Alexandrov geometry is Toponogov's Globalization theorem, namely: if a space satisfies Toponogov comparison everywhere on small neighborhoods, then the space satisfies Toponogov comparison globally.

Although we should note that the convex analysis analog does not readily lead to a proof of Toponogov's Globalization theorem, which is very difficult result in foundations of Alexandrov geometry. For functions $f$ on $\mathbf{R}^d$ the question is: if $f$ is locally convex, then prove $f$ is globally convex.