It will be interesting to see if they can take this symbolic engine approach further. Geometry problems are very neat and tidy, compared to using logic to solve real world problems. In particular I wonder if this could be some small step towards AGI.