alt Hacker NewsRight. And I said it's incredibly difficult to formalize so that a machine can do it.
I don't understand what you're confused about.
Right. And I said it's incredibly difficult to formalize so that a machine can do it.
I don't understand what you're confused about.
Theres nothing difficult about formalizing a proof you understand.
Formalizing hot garbage supposedly describing a proof can be arbitrarily difficult.
The problem is not a missing library. The number of definitions and lemmas indirectly used is often not that much. Most of the time wasted when formalizing is discovering time and time again that prior authors are wasting your time, sometimes with verifiably false assumptions, but the community keeps sending you around to another gap-filling approach.