I doubt it would bypass the goal checker but it is possible, and yes, the proof compiling doesn’t mean we will understand it

That’s true

The work doesn’t need to be verified because it has been written in Lean, which automatically validates it. I can’t attest to whether or not the work was stolen, but this argument doesn’t work here.

I looked in the repository. The proofs are in lean and there is no need for human feedback

Yeah, we definitely need a proper restructuring of economic incentives. Rewarding this competition towards existential crises isn’t doing much good to humanity. I think people are in a desperate need for treating philosophical problems seriously.

The way modern models prove theorems is with the help of a proof assistant like lean. They provide solutions to unsolved problems, not ones that have already been solved.

There’s a paywall. All that I can say is that some models are capable of proving theorems via theorem provers like Lean4, which validates proofs without requiring human feedback. The issue is real and it is a bit of an existential problems to how mathematics will evolve.

I’d say that even with the field potentially getting completely automated in the future, I would still find joy in doing it as much as someone would enjoy playing chess even though a machine can do it much better.