> 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.
That is already the case for most neural networks and LLMs.