I am pretty sure that in 20 years every mathematician will happily use an ITP system. That is because formal reasoning is not unnecessary, but just too burdenso

I am pretty sure that in 20 years every mathematician will happily use an ITP system. That is because formal reasoning is not unnecessary, but just too burdensome to be done on paper. Ideally a future ITP system will give you the formalisation almost for free, and lets you concentrate on your creative insights. It will be empowering you, instead of restricting you. It will be a tool that will let you explore your ideas more freely and creatively than it was possible before due to your limitations as a human. That is also why it is so important to get the basic foundations of such an ITP system right, as the limitations of the ITP system will become your limitations.