# Autoformalization with Large Language Models (@ arXiv 2022)

### Yuhuai Wu, Albert Q. Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, Christian Szegedy

As a side note, translating olympiad problems also shows one mismatch of formal theorem provers to the kind of challenge that is presented for students. Many of the exercises are about computing the value of a very complicated expression, which one needs to decompose or make several observations and reductions so that that is doable by hand, without a computer, in a short amount of time. At the end, though, the student reaches a number, which is obviously not told beforehand. Since theorem statements in formal languages come before their proofs, it's not straightforward to translate the problem of "find the value of $\cdots$" into a formal theorem statement. In this paper, they do the translation by appending the answer to the problem statement. This is a valid choice for this experimental investigation, but shows that existing languages and environments might not be natural for expressing the kinds of exercises we are used to in educational settings.