Comment by OxO4

The recent progress does not imply that the "impersonator" has a deep understanding of mathematics. By formalizing a problem in Lean, constructing the proof is essentially a complex search. Because Lean is the arbitrator of correctness, the "impersonator" can make as many mistakes as they want until they find a solution that passes the checker. That is very different from checking a paper for correctness.