Comment by m_w_

> Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems.

Pretty insane. I suppose it lends further credence to the idea that anything that can be shown to be correct can be done by a model.