alt Hacker NewsBy formalizing, they mean within a proof assistant like Lean or Rocq, not simply in prose in a textbook. I can attest, 40 hours per page is by no means an overestimate for this sort of work.
By formalizing, they mean within a proof assistant like Lean or Rocq, not simply in prose in a textbook. I can attest, 40 hours per page is by no means an overestimate for this sort of work.
Can you also attest to the scaling factor they suggest and that it doesn't have any scaling time benefits?
166 * 40 = 7000ish
They say it is 20x that.
Do you also agree with that?