What separates math from pure logic is that math has a set of very intuitive axioms. So mathematics is first and foremost about stretching and fixing inconsistencies in our intuition, I personally see no value in trying to refactor the foundations of mathematics like constructing integers based on sets etc, taking integers and their operations as an axiom hurts nobody. Theorem provers seems to be like that as well, people don't prove new things in it they just refactor old things to fit in, kinda like people rewriting their services in languages with more street cred like Haskel or Rust.
Taking certain sets of axioms can lead to very un-intuitive conclusions, that's why some people care about building a solid foundations. A classic example is https://en.wikipedia.org/wiki/Banach%E2%80%93Tarski_paradox , which states "Given a solid ball in 3‑dimensional space, there exists a decomposition of the ball into a finite number of disjoint subsets, which can then be put back together in a different way to yield two identical copies of the original ball." If we change the foundations to remove the axiom of choice, this paradox (and many others like it) is destroyed.
Once there is "enough" in it, the rest will go in at an exponentially increasing rate, for a few years.
After that, you will need to explain to a journal why your submitted paper doesn't refer to a mechanical proof.