> a team of agents completed the proof in a little under two weeks, consuming about six billion output tokens from a general-purpose internal research model roughly comparable to Claude Fable 5.1.

At $50/M output tokens, this would have cost on the order of $300k (plus a bit for input/prefill tokens) at API rates.

▲

3192987 2 hours ago | parent | next [-]

And human salaries for those who worked on the prover harness etc. which isn't just standard Fable.

It also uses Prove2Me, which uses a graph like previous automated theorem provers. A fact that LLM hawks have categorically denied here before, with opposition naturally flagged.

Now they have it in writing.

▲

tonyarkles 2 hours ago | parent | prev | next [-]

But also achievable on a $150/mo (CAD) Max 5 subscription (I currently have 11.6B tokens in the last 30 days) according to /usage. It doesn’t break down input vs. output tokens as far as I can tell.

	▲	wolttam 2 hours ago \| parent \| next [-]
		~10B tokens a month is pretty typical overall input/output usage from my own experience and other developer accounts I've seen
	▲	fspeech an hour ago \| parent \| prev \| next [-]
		It's 6B output tokens, as stated by the blog post.
	▲	dist-epoch 2 hours ago \| parent \| prev [-]
		When writing software with Codex 95+% of tokens are cache, I would assume the same in your case (if you also used it for coding).

▲

jensgk 2 hours ago | parent | prev | next [-]

What would it cost to make a team of mathematicians do the same?

	▲	nearbuy 14 minutes ago \| parent \| next [-]
		The Kevin Buzzard post linked at the top says they budgeted £1M over 5 years for a smaller proof.
	▲	dist-epoch 2 hours ago \| parent \| prev [-]
		More importantly how many years it would take.

▲

2 hours ago | parent | prev | next [-]

[deleted]

▲

2 hours ago | parent | prev [-]

[deleted]