Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

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

starfleetmath.com

Post reply on HN
Print view View original

101–110 of 119 posts

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

#101

Post by trenchgun »

universa1 wrote: post #59
zitterbewegung wrote: post #17

I 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?

Yes, assuming the stuff it depends on is already formalized.

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

#102

Post by esafak »

moi2388 wrote: post #35
esafak wrote: post #30

Earlier quoted context omitted.

Conjectures and proofs are the fruit of the understanding. Nobody gets paid to think without producing anything.

How about philosophers?

Good example! I think philosophy's purpose is to clarify and systematize unexplored intellectual areas. I imagine philosophers today are already using AI as intellectual sparring partners. I suppose if energy were cheap, we could run AIs all day long to pontificate like humans and write philosophical tracts on the issues of the day. When that happens, we will see if they say anything of merit.

Mathematicians will soon be left only to conjecture, with proofs being automated. The issue I see is that AI will devise proofs that are beyond our comprehension, since humans are already taxing each other (cf. Wiles, Mochizuki, Perelman, etc.) Once humans lose grasp of the proof, how will they propose new conjectures?

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

#103

Post by esafak »

zamadatix wrote: post #95
esafak wrote: post #16

Earlier quoted context omitted.

What is their pay going to be justified by once computers start conjecturing and proving theorems on their own?

Is this question just for mathematicians in isolation or does it imply the same for most other jobs too? I think the answer for the former is we don't, mathematics would become a hobby the same as we don't hire people to be human calculators anymore because we have machines better st it. For the latter, it depends - some say UBI while the machines do the work, others say dystopia ruled by the machines or their few ow…

It is for all jobs. We have to be open to new arrangements. I like the recent proposal (https://news.ycombinator.com/item?id=47748123) to tax AI companies that destroy human demand. My point is we have to sort this out now because AI companies are quickly usurping power from labor, and if we wait there will be even more unrest, and worse.

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

#104

Post by cubefox »

falcor84 wrote: post #67
cubefox wrote: post #65

Earlier quoted context omitted.

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…

But the thing with "pure" math, is that it can unexpectedly get adulterated by debased concerns such as enabling cryptography for the world economy.

I doubt that pure mathematics can claim the success of cryptography. For example, no result from advanced mathematics is required to know that factoring the product of two large prime numbers is slow.

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

#105

Post by toomuchtodo »

Exceptional work. Reminds me of https://www.distributed.net/Main_Page | https://boinc.berkeley.edu/ | https://en.wikipedia.org/wiki/EFF_DES_cracker. Consider scaling up by distributing this work more broadly. "Many hands make light work." Lots of problems remaining to solve.

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

#106

Post by weatherlite »

QuesnayJr wrote: post #79
weatherlite wrote: post #62

Earlier quoted context omitted.

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.

At Burger King?

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

#107

Post by Ancapistani »

weatherlite wrote: post #106
QuesnayJr wrote: post #79

Earlier quoted context omitted.

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

At Burger King?

I worked with two philosophy Ph.Ds in corporate strategy years ago. An a chemical engineer, and a nuclear engineer. We were all managing excel documents at the time.

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

#108

Post by zitterbewegung »

universa1 wrote: post #59
zitterbewegung wrote: post #17

I 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?

With Aristotle you could formalize a proof from only the text of a paper.

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

#109

Post by KajMagnus »

fractorial wrote: post #94
lionkor wrote: post #60

Earlier quoted context omitted.

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.

Valid question. If I were further along and had the time to succinctly write up all my contributions, I would just point you at my blog post. I’m generally a poor communicator, so here goes nothing. I designed and stood up a sovereign inference/compute on my intranet. It uses a trust model that allows for a controller (me) to spin up untrusted inference/forge machines for Lean, Sage, or other runtimes. Untrusted sand…

Interesting to read!

> contributions

One thing I think you and the other "AI math builders" have done, is to show how good the top models are at logics and reasoning.

I didn't realize how good they are, until they solved an Erdös problem. And now lots of Erdös problems!

(Plus verified that the AIs actually did solve the problems, that's not easy :- ))

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

#110

Post by piloto_ciego »

jibal wrote: post #81
piloto_ciego wrote: post #37

Earlier quoted context omitted.

That’s the problem, the coupling of work with the right to survive

You went deep ... and I for one appreciate it.

I mean, it doesn’t have to be deep to be meaningful.

The connection between “needing to work” and “right to continue existing” is THE problem with society right now.

You think AI boomers are paranoid because they think robots are going to replace the jobs? People are paranoid because they don’t know how they’re going to exist in a post-work world.

Post reply on HN