> it wrote 13 million lines of Lean

Is this basically like opening up a black box and seeing 13 million gears all rotating seemingly randomly and still having no idea how the machine actually works?

That is already the case for most neural networks and LLMs.