I don't understand then, because it doesn't sound like you understand how Lean works.
The actual proposition of the theorem is very short in Lean, and at this point has been looked at by probably hundreds of mathematicians (including the authors of the article). All that needs to be confirmed manually is that the proposition statement matches what people say the theorem actually proves. That has been done.
At that point, the rest of the actual proof steps are automatically verified by Lean - that's literally the entire point of Lean. There is no additional verification step - "What has shown the Lean proof to be correct" is the fact that the Lean program automatically validated it and generated a certificate.
But what mathematicians really care about is the actual steps. What the authors of the article have shown is just because you have a Lean program it doesn't mean the steps of the natural language theorem have been "autoformalized", because there is no guarantee the steps from the natural language description match the Lean code.
The actual proposition of the theorem is very short in Lean, and at this point has been looked at by probably hundreds of mathematicians (including the authors of the article). All that needs to be confirmed manually is that the proposition statement matches what people say the theorem actually proves. That has been done.
At that point, the rest of the actual proof steps are automatically verified by Lean - that's literally the entire point of Lean. There is no additional verification step - "What has shown the Lean proof to be correct" is the fact that the Lean program automatically validated it and generated a certificate.
But what mathematicians really care about is the actual steps. What the authors of the article have shown is just because you have a Lean program it doesn't mean the steps of the natural language theorem have been "autoformalized", because there is no guarantee the steps from the natural language description match the Lean code.