Isn’t it more like it merges the code without a dev reviewing or understanding it?

Pretty close, but IMO not quite. A math proof in and of itself is useless unless either:

   (A) it furthers human knowledge
   (B) it gets used in applied sciences, engineering, etc.

No. Merged code can perform actions with effects on the world, even if a human being never saw it. Constructing a giant Lean formalization that nobody understands simply doesn't do anything.