Comment by curt15

> They're clearly cost effective for frontier AI firms

It's not obvious that this is a given. "Cost-effective" implies a comparison between cost and output. OAI spent millions to race human researchers on Navier Stokes, and that doesn't even account for the training cost. And how does one value the output? OAI is for some reason still hiring armies of humans instead of automating roles like "AI support engineer" or "Product Designer" (https://openai.com/careers/search/).

Calling the proofs a "side-product" is also rather dubious when OAI employs a team of mathematicians specifically to train its theorem proving capabilities.