Solving a theorem is like climbing a new mountain. The mountain is already there, and there is a list of the hardest known mountains to climb. The point of climbing them and not just dropping with a plane on top of the peak is to help develop human climbing skills and expand our knowledge and abilities. Also, already conquered mountains are climbed all the time to test new strategies.

Now, if an LLM proves a theorem, it's like discovering a new mountain and knowing what its peak looks like. Does that mean the problem is finished? No, we still need climbers to actually do the work and advance the field with human understanding.

We built the helicopter? Why not use it and find a bigger mountain.

Why? Why should a government invest money into this? Here you see human understanding as an ends, while historically in society it has been applied as a means to ends like social power, resource accumulation, etc.

Now these means are generated. If the proof yields some improvement somewhere, it can be used and there needs to be no human in the loop