User Portlet
I've been involved in developing symbolic geometry at Saltire Software for the last 30 years. By symbolic geometry, I mean software systems which take as input geometric figures and which output exact symbolic quantities.
In some situations, these exact quantities may be simple. For example, we may find that the distance between a particular point and a particular line is exactly 0. Then we have established something in the nature of a 'theorem'. That the point is guaranteed to lie on the line.
In other situations, the symbolic output may take the form of a formula for a particular quantity. This formula is a suitable input for a system such as Mathematica to further analyze.
Recently I've been looking at automatically generating new geometry theorems. A motivation for this is in providing new proof problems for students whose solution cannot be found lying around on the internet.
Saltire was founded in 1989 as a spin off from Tektronix Laboratories, where I was a Principal Software Engineer.
Prior to that I was doing geometrical modelling of the onset of folding in the ferret brain at Dundee University (PhD in anatomy).
Prior to that I was looking at probabilities in a Markov process inside the defruiting of secondary radar (MS Applied Mathematics Georgia Tech)
Prior to that I was translating some of Kepler's theories about nested Platonic Solids at Cambridge University (MA Mathematics).