Since I know you're targeting undergrads with Xena - do you feel that changes are happening in more entrenched academia? Is there any evidence of people using automatic provers who weren't before?
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.
In time, the profs will retire, and undergraduates will become profs. Those will expect proofs to have been checked before submission.
Mathematics might fission into two fields, one with proofs that cannot practically be formally checked, ultimately akin to philosophy, and rigorous maths that will demand finite checks. Moving results from the former to the latter will occupy some. Exploring whether, and under what conditions, that is possible, for any given result, will have its own interest.
