DRIFT: Descomponer, recuperar, ilustrar y formalizar teoremas