Can a computer understand, or even prove, a theorem?
Axiomatic geometry (300 B.C.) builds all our geometric knowledge by logically reasoning from a minimal set of premises, or postulates. In a very similar way, recent software like LEAN (2013) have taken the challenge of formalizing and even creating mathematics.
Come and see how far a computer can get at doing geometry!