Rigor was never vital to mathematics. ZFC was explicitly pushed as the foundation for mathematics because Type Theory was too rigorous and demanding. I think that mathematicians are coming around to TT is a bit of funny irony lost on many. Now we just need to restore Logicism...

Rigor was always vital to mathematics. That it wasn’t vital to mathematicians is exactly why we need automated proofs.