>Then ask it to convert the problem into each of those formal methods. Then use something like Mathematica on each formal method.

Draft, Sketch, and Prove from 2022 does something like this: https://arxiv.org/abs/2210.12283