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

21–30 of 119 posts

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

#21

Post by colin7snyder »

vessenes wrote: post #4

Very 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

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

#22

Post by rgarrett88 »

no_multitudes wrote: post #10
esafak wrote: 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?

This will keep happening until we stop people from doing it.

Get the looms while you're at it

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

#23

Post by colin7snyder »

fractorial wrote: post #9

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

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)

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

#24

Post by orlandpm »

colin7snyder wrote: post #20
Choco31415 wrote: post #7

Earlier quoted context omitted.

According to a quick google search: "He is currently CTO at Xinobi AI, a Japan-based startup developing personal AI agents."

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

> dedicated 60-vCPU server

How many of these are you paying for out of pocket??

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

#25

Post by ralusek »

esafak wrote: post #16
zamadatix wrote: post #12

Earlier quoted context omitted.

The thing about math is we don't usually know what is pure fancy and what is civilization altering until far after the discovery. Once in a while it's a real targeted crack at something practical but most often it's collecting things which seem trial until you use them together and suddenly you have computers running LLMs. If it were really just about funding people who like math to have fun then it's easy to do fore…

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

This is kind of insane reasoning. It's basically asking "what is their pay going to be justified by once their pay isn't justified?"

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

#27

Post by srcreigh »

esafak wrote: post #16
zamadatix wrote: post #12

Earlier quoted context omitted.

The thing about math is we don't usually know what is pure fancy and what is civilization altering until far after the discovery. Once in a while it's a real targeted crack at something practical but most often it's collecting things which seem trial until you use them together and suddenly you have computers running LLMs. If it were really just about funding people who like math to have fun then it's easy to do fore…

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

Mathematicians will be the ones who can tell us if the computer theorems are decent or not.

Otherwise they’ll be the ones like Erdős who pose the questions in the first place.

Either way it will always be humans who decide what matters. AI is speaking our languages, not the other way around. We’re in charge. It’s impossible for us not to be, unless we can train an AI from dolphin data or other natural phenomenon.

The AIs intelligence is tuned to us and in 300 years we’ll need new training runs for the update from human zeitgeist language and the 2200 century famous mathematicians.

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

#28

Post by esafak »

ralusek wrote: post #25
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?

This is kind of insane reasoning. It's basically asking "what is their pay going to be justified by once their pay isn't justified?"

I think you're trying to say their pay won't be justified? You are not being clear.

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

#30

Post by esafak »

Legend2440 wrote: post #19
esafak wrote: 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?

The job of a mathematician is to study mathematics, not to create proofs. An automatic proof solver doesn't make mathematicians obsolete any more than the excel sheet made accountants obsolete.

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