Vers une automatisation sûre et expressive : combiner preuves automatiques et interactives