Mathematics mechanization and applications after thirty years