Proofs assistants : from symbolic logic to real mathematics (Version intégrée)