alt Hacker News> more than 1,000,000 lines of Lean 4 code and concluding with a QED.
Usually the point of the proof is not to figure out whether a particular statement is true (which may be of little interest by itself, see Collatz conjecture), but to develop some good ideas _while_ proving that statement. So there's not much value in verified 1mil lines of Lean by itself. You'd want to study the (Lean) proof hoping to find some kind of new math invented in it or a particular trick worth noticing.
LLM may first develop a proof in natural language, then prove its correctness while autoformalizing it in Lean. Maybe it will be worth something in that case.
No, the point of proofs in mathematics IS to prove a particular statement is true, given certain axioms (accepted truths). Yes, there are numerous benefits beyond demonstrating something is undeniably true, given certain accepted truths, perhaps more “useful” than the proof itself, but math is a method of formal knowledge that doesn’t accept shortcuts.