@feliks It's neat that math is a domain where you can fact check things automatically without needing to have "out of system" knowledge. I've been looking at software for math proofs and it looks pretty straightforward. Unexpected that language models are that good at using provers already.
@mauve yeah being able to automatically check the LLMs output is really practical in that domain. one of the reasons that other tasks are more challenging to master i believe