They first do have to show results that are actually useful to any human, though.

Right now, they just created busy work for real mathematicians while snatching away their feeling of accomplishment and discovery.

The only "use" for these results people can claim currently, all rest on the idea that surely better results will follow. Which is why it's being called strip-mining, because you can only keep that up for so long.

What if they just start churning out Lean proofs forever, and the only job left for mathematicians is turning them into human readable proofs, this is definitely a net negative for humanity, because then true progress of mathematics will slow down, because there are more people that like doing mathematics for discovery and accomplishment, than there are people that like doing math homework for the sake of it.

Also I would prefer a world where humans get to have this sense of discovery and accomplishment, instead of what they are trying to turn mathematics into.

It depends on the definition of superhuman. For example my car is superhuman as it allows me to get in one hour to a place where it would take me ten hours to go by walking, and can I walk ten hours non stop? However it is not superhuman enough to carry me where I could not walk too. And there are places where I can walk to but I cannot reach by car. Maybe that applies to AIs as well. A plane is in the same category of superhumanity of cars, with more speed. But I could still get to Australia by walking and rowing with my hands on a log (and probably die, I know.)

However there are truly superhuman vehicles, spaceships and submarines, that can carry humans where no human could go alive.

I don't know if these AIs are superhuman in the way of planes or in the way of spaceships. I also don't know if they can do everything we can do by talking or if they have some limits.

I mean, a plane can fly but not reach a branch and stay still on it. A small drone, almost. My coding agents sometimes can't do the obvious but is it because of some intrinsic limitation or because my instructions are bad? So far my experience is that they are superhuman like cars or trains, not yet as planes.