4 ms·

It's amazing how much attention this issue has gotten. What is lost in the hype is no AI can tell you if a proof is correct. An AI can produce a convincing look

It's amazing how much attention this issue has gotten. What is lost in the hype is no AI can tell you if a proof is correct. An AI can produce a convincing looking proof, but it can have a subtle but critical error or make an assumption that is unfounded. Thus, it ultimately comes down to humans. A mathematician has to craft the prompt, and mathematician to interpret/check the results. Also, these programs are very expensive and propitiatory. They are not like the commercial AI that regular people use. It takes considerable prompting and trial an error to solve even Olympiad/Putnam problems, and tons of work by humans pouring over the results to see if it's correct. For every Erdos problem that captures the headlines, there are many where it failed or untold hours of prompting and token burn to get that result, and manhours verify it.

ares623 4mo ago
But just imagine... (edit: lol didn't realize the sibling comment below is essentially my comment)
treyd 4mo ago
I don't think you understand the workflow. Terrence Tao has done a lot of work using them in conjunction with LEAN. You aren't having the AI check the proof, you interactively work on the same LEAN proof, handing off between the AI assistant and having LEAN check it and provide feedback for both of you when there's a mistake.
hackermailman 4mo ago
AI can't yet come up with any new ideas to make the inductive leap to solve a math problem. New ideas are what get the accolades and using an old idea just means the original author missed something. We are still at the author missed something stage that AI is doing today. It can definitely be a good research assistant though
- NateEag 4mo ago
  Thank you for your comment. I had assumed that the recent OpenAI solution to an Erdos problem represented original mathematical thought. I went looking for more details, and found this Scientific American article which provided some nuance I had previously missed, namely that the mathematicians involved don't think genAI created any really new mathematics - just applied what existed in an intelligent, elegant way: https://archive.is/oNCSO https://archive.is/oNCSO So, impressive though the result is, perhaps your claim has more grounds than I had thought.
- bckgrndrdtn 4mo ago
  All well and good, but we should also admit that under this criterion 95% of published math papers don't contain new ideas but are just filling in stuff that previous authors missed.
golly_ned 4mo ago
Please read the article. You've ignored proof checkers.

ares623 4mo ago

But just imagine... (edit: lol didn't realize the sibling comment below is essentially my comment)

treyd 4mo ago

I don't think you understand the workflow. Terrence Tao has done a lot of work using them in conjunction with LEAN. You aren't having the AI check the proof, you interactively work on the same LEAN proof, handing off between the AI assistant and having LEAN check it and provide feedback for both of you when there's a mistake.

hackermailman 4mo ago

AI can't yet come up with any new ideas to make the inductive leap to solve a math problem. New ideas are what get the accolades and using an old idea just means the original author missed something. We are still at the author missed something stage that AI is doing today. It can definitely be a good research assistant though

NateEag 4mo ago
Thank you for your comment. I had assumed that the recent OpenAI solution to an Erdos problem represented original mathematical thought. I went looking for more details, and found this Scientific American article which provided some nuance I had previously missed, namely that the mathematicians involved don't think genAI created any really new mathematics - just applied what existed in an intelligent, elegant way: https://archive.is/oNCSO https://archive.is/oNCSO So, impressive though the result is, perhaps your claim has more grounds than I had thought.
bckgrndrdtn 4mo ago
All well and good, but we should also admit that under this criterion 95% of published math papers don't contain new ideas but are just filling in stuff that previous authors missed.

golly_ned 4mo ago

Please read the article. You've ignored proof checkers.