That's why the author refused to read a proof from someone he knew until it was formalized in Lean.
Yes it compresses the proofs but still "Sol had generated 1.2 million lines of Lean code in the three weeks that it had worked on the project". I mean how do you even verify that?
alt Hacker News
Yes it compresses the proofs but still "Sol had generated 1.2 million lines of Lean code in the three weeks that it had worked on the project". I mean how do you even verify that?