Hacker News: colin7snyder

Who's Subsidizing Chinese AI

colin7snyder — Sun, 19 Jul 2026 10:25:56 +0000

Article URL: https://www.chinese-ai-report.com/

Comments URL: https://news.ycombinator.com/item?id=48966676

Points: 4

# Comments: 7

New comment by colin7snyder in "Solving 20 Erdős Problems with 20 Codex Accounts Running in Parallel"

colin7snyder — Wed, 15 Jul 2026 13:10:59 +0000

I don't disagree with you zingar. I think Erdős problems are great for testing a system's capability on genuinely hard math, which has value as a benchmark in itself, and maybe as a stepping stone toward more real-world impact. Your sentiment is well put.

To answer your question directly: most Erdős problems don't have practical applications on their own; the value is the techniques and the machine-checked proofs they leave behind. But there's more real world value in solving some of the FrontierMath Open Problems or Millennium Problems. There's a Venn diagram of "hard problems" and "real world impact" for sure.

New comment by colin7snyder in "Solving 20 Erdős Problems with 20 Codex Accounts Running in Parallel"

colin7snyder — Wed, 15 Jul 2026 11:42:09 +0000

Thank you for bringing this up pfdietz. No, not defective. The Lean proofs behind both are machine-checked and unchanged. I withdrew them over framing, not correctness.

1) For #129 a couple people pointed out that the report was very confusing. And I agree. So I'm currently attempting to improve it.

2) For #130, a person pointed it out as being a partial solution. This seems correct, so I'm currently working on making it fully end to end.

These are put out as "proposed solutions" for the mathematics community to scrutinize, and the scrutiny worked exactly like it should. Happy to take any feedback and make them better.

New comment by colin7snyder in "Solving 20 Erdős Problems with 20 Codex Accounts Running in Parallel"

colin7snyder — Wed, 15 Jul 2026 10:19:07 +0000

thank you very much for catching this. just fixed

New comment by colin7snyder in "Solving 20 Erdős Problems with 20 Codex Accounts Running in Parallel"

colin7snyder — Wed, 15 Jul 2026 10:10:40 +0000

I haven't come across this before. I will spend time on comparator. thank you very much for the suggestion.

New comment by colin7snyder in "Solving 20 Erdős Problems with 20 Codex Accounts Running in Parallel"

colin7snyder — Wed, 15 Jul 2026 10:08:21 +0000

Thank you for the questions echelon.

1) As far as the AI models go, we used GPT 5.6 Sol, Fable 5, and Gemini-2-embeddings across the system

2) Yes, the agents are given bash tools that allows them to interact with the preinstalled mathematics packages/dependencies that are on the VMs

3) This was a setup as a relatively quick project without much thought for future contributions, I will spend some time thinking about how i could make it more open.

New comment by colin7snyder in "Solving 20 Erdős Problems with 20 Codex Accounts Running in Parallel"

colin7snyder — Wed, 15 Jul 2026 05:47:52 +0000

I haven't played around with Aristotle at all, thanks for bringing it up & (also your codebase, thesisus, is very solid!)

New comment by colin7snyder in "Solving 20 Erdős Problems with 20 Codex Accounts Running in Parallel"

colin7snyder — Wed, 15 Jul 2026 05:43:55 +0000

apologies, bad wording/explanation. As addressed in another comment: "Poor wording on my end, thanks for flagging. I pull the OAuth refresh token from each Codex account into a custom broker, which mints short-lived access tokens per request and load-balances across the pool."

New comment by colin7snyder in "Solving 20 Erdős Problems with 20 Codex Accounts Running in Parallel"

colin7snyder — Wed, 15 Jul 2026 05:42:34 +0000

yeah, im currently running the system on navier-stokes (making real progress).

Unfortunately P vs NP, on the other hand, is going to have to wait for GPT 7

New comment by colin7snyder in "Solving 20 Erdős Problems with 20 Codex Accounts Running in Parallel"

colin7snyder — Wed, 15 Jul 2026 05:39:57 +0000

Poor wording on my end, thanks for flagging. I pull the OAuth refresh token from each Codex account into a custom broker, which mints short-lived access tokens per request and load-balances across the pool.

New comment by colin7snyder in "Solving 20 Erdős Problems with 20 Codex Accounts Running in Parallel"

colin7snyder — Wed, 15 Jul 2026 03:56:20 +0000

Thank you for the kind words! I agree, it's exciting that we can now build advanced AI systems for solving novel math (but i still love pen & paper too)

New comment by colin7snyder in "Solving 20 Erdős Problems with 20 Codex Accounts Running in Parallel"

colin7snyder — Wed, 15 Jul 2026 03:51:20 +0000

This is great feedback (thank you for taking the time), & you especially bring up a fair point on the writeups needing to be more human readable. I'll work on that

New comment by colin7snyder in "Solving 20 Erdős Problems with 20 Codex Accounts Running in Parallel"

colin7snyder — Wed, 15 Jul 2026 03:49:00 +0000

This is a self funded weekend project for me. It's not associated with any employer (:

Solving 20 Erdős Problems with 20 Codex Accounts Running in Parallel

colin7snyder — Wed, 15 Jul 2026 00:15:56 +0000

Article URL: https://www.starfleetmath.com/

Comments URL: https://news.ycombinator.com/item?id=48914646

Points: 164

# Comments: 110