Automated theorem proving + neural language models + reinforcement learning.
I think most people seriously underestimate how powerful modern proof assistants like Lean [1] are for building things like provably correct software and chips, as well as verifying math research. But fully formalizing anything big leads to a proliferation of small annoying lemmas -- not "difficult" to prove per se, just annoying and time-wasting. I'm working on a neural theorem prover that aims to solve these lemmas fully automatically.