I think everyone who has heard of interactive theorem provers saw that this is going to be a match made in heaven.

LLMs reduce implementation effort but pile on massive review effort. Interactive theorem provers reduce review effort but the implementation is much more work.

Together you get the best of both worlds at the speed of machine thought.