colin7snyder

6 ms·

1. 1.▲
   Who's Subsidizing Chinese AI(chinese-ai-report.com)

   4 points by colin7snyder 2mo ago|7 comments
2. 2.▲
   by colin7snyder 2mo ago

   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. Yo
3. 3.▲
   by colin7snyder 2mo ago

   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 confus
4. 4.▲
   by colin7snyder 2mo ago

   thank you very much for catching this. just fixed
5. 5.▲
   by colin7snyder 2mo ago

   I haven't come across this before. I will spend time on comparator. thank you very much for the suggestion.
6. 6.▲
   by colin7snyder 2mo ago

   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 mathemati
7. 7.▲
   by colin7snyder 2mo ago

   I haven't played around with Aristotle at all, thanks for bringing it up & (also your codebase, thesisus, is very solid!)
8. 8.▲
   by colin7snyder 2mo ago

   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
9. 9.▲
   by colin7snyder 2mo ago

   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
10. 10.▲
    by colin7snyder 2mo ago

    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.
11. 11.▲
    by colin7snyder 2mo ago

    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)
12. 12.▲
    by colin7snyder 2mo ago

    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
13. 13.▲
    by colin7snyder 2mo ago

    This is a self funded weekend project for me. It's not associated with any employer (:
14. 14.▲
    Solving 20 Erdős Problems with 20 Codex Accounts Running in Parallel(starfleetmath.com)

    164 points by colin7snyder 2mo ago|110 comments