Going from informal to formal can be done using autoformalization [1]. The real question is, how do you judge that the result is correct?
[1] Autoformalization with Large Language Models — https://papers.nips.cc/paper_files/paper/2022/hash/d0c6bc641...