Viewing profile — colin7snyder

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 …

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…

thank you very much for catching this. just fixed

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

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 …

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

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 cus…

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

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…

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)

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

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