Live data from Hacker News

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

starfleetmath.com

71–80 of 119 posts

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

#71
post #55

Earlier quoted context omitted.

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?

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.

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

#72

Very 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.

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

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

#73
post #8

Isn't this sucking the fun out of math? It's not like we're going to get any tangible benefit out of them, so why not let mathematicians keep their jobs?

I don't envy the talented young research mathematicians starting their career now. While there's still space to distinguish yourself (inventing completely new mathematics), the path to recognition is narrow.

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

#75
post #65

Earlier quoted context omitted.

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.

There still seems to be a difference between useless pure math research and useless science or useless philosophy. Science, even useless science, still has a subject matter that is relevant to us independently of science, the real world. And philosophy studies concepts (like "knowledge") that occur in natural language and thought, and those concepts are relevant to us independently of philosophy. But pure math is ent…

"useless" pure math often turns out to have scientific applications.

And surely you don't mean all pure math, so your argument ends up being circular --- useless math is useless. You happen to think that this math is useless, but you might be, or turn out to be, wrong.

Also, you're misusing the term "self-referential". You seem to mean that it's a closed system ... but it's not, since mathematicians interact with it.

Finally: so what? We do all sorts of enjoyable activities with no benefit other than the enjoyment. Solving Erdős problems seems at least as justifiable as finding the trillionth digit of pi or writing an Apple ][ emulator in Brainfuck or playing those video games that you demonize by calling them addictive. (Compare to, say, compulsively reading Britannica's The Great Books of the Western World ... it's snooty judgments all the way down.)

Postscript to finally: This framework has wider application ... it's not limited to Erdős problems or anything else that someone happens to consider to be useless.

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

#76
post #52

Earlier quoted context omitted.

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)

No people procreating built civilization.

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

#77
post #52

Earlier quoted context omitted.

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)

No people procreating built civilization.

Nature created people and the metaphysics in their heads.

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

#79

Earlier quoted context omitted.

They get paid to produce confusion.

They're getting paid?

Philosophy majors do surprisingly well in getting jobs outside academia, so I think the market demand for confusion is bigger than you might guess.

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

#80
post #34
post #26

I didn't know people could just have GPT running on their own hardware. How does one...do that? Do you have a special relationship with OpenAI and they lock down your servers or something?

I think they meant they just ran a different context per invocation, not that they hosted the model themselves.

Why in the world is the OP's answer dead? Sometimes I really don't understand HN.
Post reply on HN