Earlier quoted context omitted.
solve p=np make no mistakes
n=1 or p=0
Have been having an awful day today, this really cheered me up. Thank you so much for sharing your dumb joke!
Solving 20 Erdős Problems with 20 Codex Accounts Running in Parallel
51–60 of 119 posts
Re: Solving 20 Erdős Problems with 20 Codex Accounts Running in Parallel
#52Earlier quoted context omitted.
Post-money people with side interests are what built the current western civilization.
No, underpaid nerds have built modern civilization.
No, the people growing their food built modern civilization.
(Or millions of disconnected stakeholders with different incentives collectively built modern civilization, but who wants to put that on a bumper sticker)
Re: Solving 20 Erdős Problems with 20 Codex Accounts Running in Parallel
#53Very interesting, on many levels: first, the raw additional compute / search harness is worth reading about; huge numbers of Lean 4 theorems, thousands of vCPUs available for spreading out search, embedding databases of proofs, all very interesting. Second, the proofs -- I understand the Lean 4 proofs to be refereed by Fable, and generated by Chat 5.6 Sol. Unlike the leaked proof of the Cycle Double Cover Conjecture…
This reminds me of certain simple but addictive video games: "What are these virtual coins good for?" "You can buy better equipment" "Why do you need this equipment?" "To get more virtual coins of course!"
Which is a metaphor for life.
I also had this sort of thoughts when finishing my master's degree. I guess what breaks the cycle is that proofs (like other artefacts in other human activities) deliver aesthetic bliss.
Re: Solving 20 Erdős Problems with 20 Codex Accounts Running in Parallel
#54Re: Solving 20 Erdős Problems with 20 Codex Accounts Running in Parallel
#55Very interesting, on many levels: first, the raw additional compute / search harness is worth reading about; huge numbers of Lean 4 theorems, thousands of vCPUs available for spreading out search, embedding databases of proofs, all very interesting. Second, the proofs -- I understand the Lean 4 proofs to be refereed by Fable, and generated by Chat 5.6 Sol. Unlike the leaked proof of the Cycle Double Cover Conjecture…
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
Can you explain what you're using the local compute for vs. the API-based frontier models? That was entirely unclear to me.
Are you running tool calls that include inference with local fine tunes? And fast math packages? Controlled by the frontier model agents?
Is there a way folks can contribute to this?
Re: Solving 20 Erdős Problems with 20 Codex Accounts Running in Parallel
#56Re: Solving 20 Erdős Problems with 20 Codex Accounts Running in Parallel
#57Very cool! It seems you've got a great setup. An addition that would be very convincing is going the extra mile and making a comparator setup for your Lean proofs. (https://github.com/leanprover/comparator) This ensures that the AI is not, in any way, modifiying the Lean context in ways that could lead to unsoundness.
Re: Solving 20 Erdős Problems with 20 Codex Accounts Running in Parallel
#58[flagged]
Re: Solving 20 Erdős Problems with 20 Codex Accounts Running in Parallel
#59I was studying Erdos problems by only taking ChatGPT 5.5 outputs and just asking it to keep on attempting to solve it by asking it to go further. I haven't started doing this with chatgpt 5.6 I have some partial results here https://chatgpt.com/g/g-p-69f03400f420819192418b18ca90ffee-d... What was really interesting is that during the process it was able to find lemmas or theorems that might be related or relevant to…
This looks interesting. I am not really familiar with lean, etc... Could I use this to formalize/verify a proof from a paper?
Re: Solving 20 Erdős Problems with 20 Codex Accounts Running in Parallel
#60My mouth is agape at the fact that this project is basically what I have been working on non-stop for the last three weeks and just yesterday gotten to the point of evaluating; hats off... I only have one novel proof (non-Erdos) and 13 first-time formalizations thus far. I still like doing maths by pen and paper, but this is fun too.
When you say "working on" what is your actual contribution? Like, what should I imagine you do? For most people who tell AIs what to do and are proud of it, it's sadly mostly sitting around and staring at "thinking" output, and steering a bit, so I'm curious what the work looks like.