3 ms·

I hear existential despair. Mathematics is indeed a great example. Automation (AI) has made great strides in automating theorem proving in the last 30 years, an

I hear existential despair. Mathematics is indeed a great example. Automation (AI) has made great strides in automating theorem proving in the last 30 years, and LLMs are just a cherry on top of that. A cherry though that will accelerate progress even further, by bringing the attention of people like Terence Tao to the cause. It will not change how mathematics is done within 2 years. It will totally revolutionise how mathematics is done within 20 years (and that is a conservative guess).

hggigg 2y ago
No it's a terrible example. We have ITPs and ATPs and any progress on ATPs, which are the ones that are currently considered magical, are turning into a fine asymptote. ITPs are useful however but have nothing to do with ML at all. Putting a confident timescale on this stuff is like putting a timescale on UFT 50 years ago. A lie. Oh and lets not forget that we need to start with a conjecture first and we can't get any machine to come up with anything even remotely new there. There is no existential despair. At all.
- auggierose 2y ago
  I said 30 years, because that's for how long I am a participant in the field. I have a PhD in ITP, and yes, I am pretty confident that automation is a big part of ITP now. Maybe not so much if you are into constructive type theory, that field is always a little bit hesitant to use the full power of anything. The only one lying here is you. To yourself. By the way, AI can come up with conjectures just fine. I might not be interested in most of them, but then again, I am not interested in most conjectures humans come up with.
meroes 2y ago
ChatGPT and others can’t reliably sum several integers together still, when is an LLM going to replace anything meaningful in higher math? I spent more time deciphering ChatGPT’s mistakes than programming something in python to sum some integers this week.
- auggierose 2y ago
  I don't use ChatGPT/Claude/Gemini for coding stuff I know how to do. I use it to explore stuff I don't know. It is very useful for that. And that is how LLMs and their descendants will conquer mathematics. LLMs are for intuition, not for logic. We know how to do logic. We didn't know how to do intuition.

hggigg 2y ago

No it's a terrible example. We have ITPs and ATPs and any progress on ATPs, which are the ones that are currently considered magical, are turning into a fine asymptote. ITPs are useful however but have nothing to do with ML at all. Putting a confident timescale on this stuff is like putting a timescale on UFT 50 years ago. A lie. Oh and lets not forget that we need to start with a conjecture first and we can't get any machine to come up with anything even remotely new there. There is no existential despair. At all.

auggierose 2y ago
I said 30 years, because that's for how long I am a participant in the field. I have a PhD in ITP, and yes, I am pretty confident that automation is a big part of ITP now. Maybe not so much if you are into constructive type theory, that field is always a little bit hesitant to use the full power of anything. The only one lying here is you. To yourself. By the way, AI can come up with conjectures just fine. I might not be interested in most of them, but then again, I am not interested in most conjectures humans come up with.

meroes 2y ago

ChatGPT and others can’t reliably sum several integers together still, when is an LLM going to replace anything meaningful in higher math? I spent more time deciphering ChatGPT’s mistakes than programming something in python to sum some integers this week.

auggierose 2y ago
I don't use ChatGPT/Claude/Gemini for coding stuff I know how to do. I use it to explore stuff I don't know. It is very useful for that. And that is how LLMs and their descendants will conquer mathematics. LLMs are for intuition, not for logic. We know how to do logic. We didn't know how to do intuition.