OA has done that, as 'GPT-f': https://arxiv.org/abs/2009.03393#openai https://arxiv.org/abs/2009.03393#openai They also have ambitions of IMO: https://twitter.c

OA has done that, as 'GPT-f': https://arxiv.org/abs/2009.03393#openai https://arxiv.org/abs/2009.03393#openai They also have ambitions of IMO: https://twitter.com/spolu/status/1303693595833237504 https://twitter.com/spolu/status/1303693595833237504 I assume it's not mentioned in OP because GPT-f came out too recently for them to interview or profile compared to this Lean-using team.