Microsoft 365 is corporate business email for corporate businesses. If you're a corporate business, you're already using it, and if you're not then you probably don't want to talk to anyone who's using it anyway. Even if you could pass their filtering, they'd just manually ignore your emails because they only want to talk to corporate businesses.
Most people at e.g. Oxford and Cambridge (and, I suspect, many other universities) use their university emails for a fairly wide variety of extramural correspondence, and are stuck with M$ as the provider, alas.
They both can be useful or harmful, do to their respective strengths and trade offs.
PAC/statistical learning is good at needles in the haystack problems assuming that the tail losses, simplicity bias, and corpus representation issues are acceptable and you understand that it is fundamentally existential quantification and control for automation bias etc…
Lean is a wonderful collection of concepts and heuristics but due to Rice and Gödel etc… will not solve all problems with software development.
How Gödel’s second incompleteness theorem shows that you can prove anything, without that proof being meaningful is a lens into that.
It is horses for courses, and remember that even in sub-TC total functional programming, proving and arbitrary functions is very hard, while constructing one is far more tractable.
Even those proofs don’t demonstrate semantic correctness. History is riddled with examples of people using powerful tools that elegantly explain flawed beliefs.
The 2009 crash and gaussian copula as an example.
Get all the value you can out of these tools, but use caution, especially in math, where superficially similar similarities often have conflicting conventions, constraints, and assumptions.
Obviously if you problem is ergotic with the Markov property, both will help, but Automated theorem proving and PAC learning will never be a meta theory of the other IMHO.
What has Gödel incompleteness to do with that? We can just take any sentence φ as an axiom, and we’ve a trivial proof thereof.