This project continues investigation of automatic generation of proofs of theorems in geometry. The emphasis is on short and proofs. For this, the newly discovered area method and new methods based on other geometrical concepts, such as full angles and trigonometric functions, are being developed. Extension of these techniques are being sought to geometric inequalities as well as to non-Euclidean and higher- dimensional geometries. The techniques are being implemented in a system with a sophisticated graphics display.