Mechanical theorem proving in differential geometry - Local theory of surfaces

An automated reasoning method, based on Wu's method and calculus of differential forms, is proposed for mechanical theorem proving in local theory of space surfaces in differential geometry. The method has been used to simplify one of Chern's theorems: ''The non-trivial families of isometric surfaces having the same principal curvatures are W-surfaces.'' It Some other theorems are also tested by this method. The proofs are generally simpler than those in differential geometry textbooks.