There is a huge amount of evidence of mathematics undergraduates using interactive provers, which they weren't doing before. There are very few profs using any interactive prover, because currently these things offer nothing useful to a prof. However, if more and more undergraduates adopt software like this, or at least try it and realise that it's not scary, then within ten years there will be profs using it. We're playing the long game. We need to make tools for the profs, like automation that can check tedious lemmas, or a database of theorem statements which is searchable by a mathematician who doesn't know how to use the software. These are some of the goals Tom Hales is targetting with his FABSTRACTS project. But it will take time. All I know is that the software is now ready to do modern mathematics.