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

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/d0c6bc641a56bebee9d985b937307367-Abstract-Conference.html https://papers.nips.cc/paper_files/paper/2022/hash/d0c6bc641...