

Using computers to search for a counter example to a conjecture isn’t exactly new ground and I suspect they did so with the aide of some harness tweaks like some numerical LSP. Like cool, it pushed the envelope but like what the parent said, they grafted on the ability to do a specific task.



You know the “DeepMind and OpenAi models” is the hint that the LLM model is not the one doing the math. The LLM provides a hypothesis and the DeepMind model provides grounding or feedback on whether the hypothesis even makes sense or works.