Remix clone Hacker News

new | show | ask | jobs Github

▲

adverbly 4 hours ago

> formalizing the 166-page paper from OpenAI would take 132,800 person-hours

Am I missing something or is this completely out of the ballpark?

I must be missing something or the upvote bots are out in force for this one...

If this were remotely true it would be impossible for anyone to write a math textbook.

▲

Paracompact 4 hours ago | parent [-]

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.

▲

adverbly 4 hours ago | parent [-]

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?

	▲	tomjakubowski 2 hours ago \| parent \| next [-]
		The scale factor comes from this number in the article, seemingly an intuited estimate: > Say a research article takes 20 times more effort to formalize than page in an undergraduate textbook. That would suggest formalizing a 10-page research article might take 200 weeks (assuming 40h/wk) of effort, or about four years. Not a mathematician, I have no idea if that's in the ballpark.
	▲	MarkusQ 3 hours ago \| parent \| prev [-]
		The point was that a textbook (where the 40hr/page estimate comes from) is cumulative/linear -- what you need for page n was defined / established on the preceding pages. But in a proof such as this you can call on any other published result (and those can do the same) so the dependency graph is (potentially) much bushier. Thus later pages of the proof should take far more than 40 hours to manually formalize.