That's one of the future direction we're pursuing! We hope to utilize the power of autoformalization (http://arxiv.org/abs/2205.12615 http://arxiv.org/abs/2205.

That's one of the future direction we're pursuing! We hope to utilize the power of autoformalization (http://arxiv.org/abs/2205.12615 http://arxiv.org/abs/2205.12615) and provably verify the solution with formal systems. As I wrote in my tweet, in the long run, I am expecting a great synergy between a strong natural language math model and an autoformalizer to tackle challenging mathematical theorems!