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?
[flagged]
Solving 20 Erdős Problems with 20 Codex Accounts Running in Parallel
11–20 of 119 posts
Re: Solving 20 Erdős Problems with 20 Codex Accounts Running in Parallel
#12Isn'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 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 forever: just don't have them look at the results and keep paying.
Re: Solving 20 Erdős Problems with 20 Codex Accounts Running in Parallel
#13Isn'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?
Isn't the pursuit of knowledge alone good enough?
Re: Solving 20 Erdős Problems with 20 Codex Accounts Running in Parallel
#14My 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.
[dead]
Re: Solving 20 Erdős Problems with 20 Codex Accounts Running in Parallel
#15Isn'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?
[deleted]
Re: Solving 20 Erdős Problems with 20 Codex Accounts Running in Parallel
#16Isn'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 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?
Re: Solving 20 Erdős Problems with 20 Codex Accounts Running in Parallel
#17I 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 be published.
While I was doing that I was also trying to use Aristotle to do the Lean formalization and I have a WIP system to do that at https://github.com/aconsapart/thesisus/
Re: Solving 20 Erdős Problems with 20 Codex Accounts Running in Parallel
#18Earlier 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?
Attending department faculty meetings
Re: Solving 20 Erdős Problems with 20 Codex Accounts Running in Parallel
#19Isn'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.
Re: Solving 20 Erdős Problems with 20 Codex Accounts Running in Parallel
#20Who is funding this? Sounds like a fun experiment but that’s a huge amount of compute if I understand correctly.
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 (: