Abstract de la publi numéro 4533

Survey of problems appearing in use of type theory and proof-assistants in symbolic computations (with examples from the theory of differential equations).