Executable Multiple-View Geometry

Why I am revisiting this

While working with Prof. Michael Werman at the Hebrew University Computer Vision Lab, I explored how multiple-view geometry could be expressed as executable symbolic mathematics. The project used Mathematica and computer algebra to formulate and check relationships from geometric computer vision, using Richard Hartley and Andrew Zisserman’s Multiple View Geometry in Computer Vision as the organizing reference.

The attraction was the movement between a geometric argument and a computation. A statement about cameras, points, lines, or planes could be translated into variables and equations. Those equations could then be manipulated, simplified, or solved, with the assumptions made explicit enough to inspect. Writing that translation was itself mathematical work: the choice of representation often determined whether the calculation clarified the geometry or obscured it.

The project aimed at a broad executable treatment of the material; the surviving implementation contains examples spanning several major parts of multiple-view geometry. I am returning to it because the underlying question still interests me: how can software help us examine a geometric model before we entrust a numerical pipeline to it?

The idea: geometry as executable algebra

Projective geometry gives many visual relationships a compact algebraic form. A point in the image plane can be represented by a nonzero three-component vector, with nonzero scalar multiples identifying the same point. A line is another homogeneous vector; incidence becomes a dot product equal to zero. A camera maps a homogeneous 3D point into a homogeneous image point, while matrix rank and determinant conditions distinguish valid configurations from degenerate ones.

This representation makes a particular workflow possible. First specify the geometric claim. Then choose symbolic variables, write the constraints, and ask what follows algebraically. A result may be an identity under stated assumptions, a description of admissible solutions, or a condition under which the proposed relationship fails. An expression that does not simplify is not automatically a counterexample: it may require a better formulation or stronger assumptions.

In Wolfram’s terminology, Simplify transforms expressions using supplied assumptions, Reduce describes solutions to logical combinations of algebraic conditions, and Solve returns solution rules. These operations support different questions; they are not interchangeable certificates. I use symbolic verification here in the computer-algebra sense: exact symbolic manipulation under stated assumptions, rather than formal proof-assistant verification.

What we implemented

My contribution centered on implementing and iterating symbolic checks in Mathematica across several connected areas. I find it more useful to describe that scope through the geometry than through a list of programs:

Projective invariants and conics

Symbolic treatment of line transformations, conic transformations, and cross-ratio. These examples asked which relationships survive a change of projective coordinates and how transformation rules can be checked explicitly.

Homographies and estimation

Homography estimation, including line correspondences, transformation invariance, and Sampson-error calculations with derivative or Jacobian expressions. This brought the algebra of geometric constraints into contact with estimation.

Camera and calibration geometry

Back-projected rays and dual Plücker line representations, together with calibration matrices, vanishing points, orthogonal directions, and relationships involving the image of the absolute conic.

Two-view geometry

Essential- and fundamental-matrix structure, the planar-mirror configuration, and reconstruction ambiguity. These examples made coordinate conventions and the distinction between a scene and its image evidence particularly important.

3D structure and reconstruction

Implicit image relationships, structure computation, homography-at-infinity relationships, and scene planes and homographies. The emphasis was on expressing relationships between representations and checking their algebraic consequences.

That breadth should not be read as complete coverage of the book. It describes the surviving examples and the direction of the work. The two explanations below are newly written illustrations of the underlying approach, rather than reproductions of the original implementation.

Example 1 — projective invariance

Consider four distinct points on a projective line. Represent each by a nonzero two-component column vector, and define the bracket of two representatives as their two-by-two determinant:

For one consistent ordering convention, their cross-ratio is the following quotient. Each point occurs once in the numerator and once in the denominator, so its arbitrary homogeneous scale cancels.

Now apply the same nonsingular two-by-two matrix M to all four points. The key identity is small enough to derive directly by expanding the determinant:

There are two determinant factors above the fraction bar and two below it. They cancel, leaving the original cross-ratio. A symbolic system can check the bracket identity first, then apply it to the quotient. This separates a reusable algebraic fact from the geometric statement it supports.

For a concrete new example, take affine coordinates 0, 1, 2, and 4, and transform them by f(t) = (2t + 1)/(t + 3). Their images are 1/3, 3/4, 1, and 9/7. With the convention above, both cross-ratios are exactly 3/2. Rational arithmetic makes this a transparent check rather than a comparison of rounded decimals.

The conditions matter as much as the cancellation. The matrix must be nonsingular, the point representatives nonzero, and the denominator brackets nonzero. If denominators are cleared before these restrictions are recorded, a symbolic equality can hold even where the original quotient is undefined. A useful executable statement therefore includes its domain, not just its final simplified expression.

Example 2 — mirror geometry

A planar mirror gives a useful example of geometry hidden inside an image. A camera may see a point directly and also through its reflection. The reflected path can be unfolded into a straight line toward a virtual camera obtained by reflecting the real camera across the mirror plane. This gives a two-view interpretation even though there is only one physical camera.

In the real camera’s coordinate system, let the mirror have unit normal n and equation n^TX = d, with the camera off the mirror plane. Reflection maps a point to X′ = X − 2(n^TX − d)n. The point, its reflection, and the mirror normal therefore lie in a common linear plane through the camera center. Their image rays obey an epipolar constraint.

Write [n]_× for the matrix implementing the cross product with n. In a common image-coordinate convention, with the same invertible calibration matrix K applied to both image regions, the reflective fundamental matrix is proportional to:

The skew symmetry follows from the cross-product matrix and the matching coordinate transforms on both sides. It is specific to this configuration and convention: independently changing the two image coordinate systems need not preserve that matrix appearance. Reflection also reverses handedness; its linear part has determinant −1 and should not silently be treated as an ordinary camera rotation. The academic treatment of planar-mirror geometry by Mariottini and colleagues provides the public technical context.

Symbolic verification vs numerical testing

Symbolic work is particularly useful when the question concerns an exact relationship: whether an invariant is preserved, whether constraints are mutually compatible, or which assumptions a derivation needs. It can expose a missing nonzero condition or reveal that an apparently general result depends on a special camera configuration.

Numerical testing asks different questions. Measurements are noisy; matrices can be nearly singular rather than exactly singular; floating-point calculations can amplify small perturbations. An identity verified over exact symbols does not establish that an estimator is stable, that correspondences are correct, or that a camera model describes real observations.

I would use the two modes together. Symbolic reasoning identifies what should hold and where it may cease to apply. Numerical experiments then examine how an implementation behaves as it approaches those boundaries. A rank condition can be exact on paper while requiring a scale-aware numerical decision in software. Neither part supplies the other automatically.

What I find interesting about it now

Today I think of this approach as executable geometry, or an executable specification for geometric vision. That is my present-day interpretation, rather than a claim about the terminology we used during the project. The useful idea is to make the mathematical assumptions of a component available to inspection and testing alongside its implementation.

A modern version could use SymPy or another symbolic system to derive checks, property-based testing to generate admissible configurations, and randomized numerical stress tests to explore difficult cases. For a homography routine, for example, one could check invariance to homogeneous rescaling and separately generate nearly degenerate correspondences. These would test different obligations, rather than repeat a single successful example.

Such checks could sit around calibration, structure-from-motion (SfM), simultaneous localization and mapping (SLAM), or reconstruction modules. Their value would depend on choosing the right contracts: broad enough to catch mistakes, explicit enough to distinguish an invalid input from numerical sensitivity, and inexpensive enough to use. This is a proposed direction, not a capability I am attributing to the original implementation.

A modern research question

Can symbolic geometric constraints serve as executable contracts around numerical vision pipelines — catching invalid assumptions, degeneracies, or implementation errors before they propagate through calibration, SfM, SLAM, or reconstruction?

A convincing answer would need examples of faults actually detected, clear treatment of near-degenerate data, and evidence about computational cost. The question is how to connect exact statements to fallible measurements without confusing their different kinds of certainty.

Looking back

The project sits at an intersection that remains important to me: mathematics, software, and computer vision. Geometry is something we derive on paper, but it can also be encoded, executed, tested, and interrogated. Making that translation carefully can reveal both the strength of a model and the conditions under which it stops answering the question we intended to ask.