> they are sharing unproven work for PR, forcing the mathematicians community to do the verification job for them

Lean 4 is relatively a new thing, last time I checked the formalization of undergraduate level mathematics isn't entirely done yet.

example https://ai.math.uw.edu/projects/spring-2026/

Lean itself is very hard to get rigorously correct, if you have every tried it yourself. I am not surprised if some AI even tries to benchmaxx Lean 4 by some loopholes