4 ms·

AI for math resources, and erdosproblems.com

160 points by nabla9 2y ago

upmind 2y ago
What does AI for Math mean? People doing Math research that want to transition to AI research?
- cvoss 2y ago
  Broadly, as you'll see in the Google doc linked from the announcement, they are referring to the use of computer systems to assist mathematical research, which falls into a two step process: 1) Identify a suitable language for use by both humans and computers for communication and manipulation of mathematical theorems and their proofs. 2) Employ both mathematicians and machine learning algorithms to generate interesting sentences in that language.
  - upmind 2y ago
    That makes a lot more sense, thanks.
  - riku_iki 2y ago
    > as you'll see in the Google doc linked from the announcement, they are referring to the use of computer systems to assist mathematical research, which falls into a two step process I reviewed the doc, and it is just curated list of links on various projects (ML frameworks, proof assistant, some tutorials), and does not outline plan you described here. Or I missed something?..
    - cvoss 2y ago
      The first section, Textbooks and Survey Papers, begins with Formal Proof (this is where one identifies the suitable language for mathematics), followed by general Machine Learning references, and concluding with Machine Learning for Formal Proof. Other sections have similar divisions, though some go off into adjacent fields where one finds non-AI* algorithms for specific mathematical applications, such as automated symbolic calculus or SMT solving, to name just two. *Some people's terminology would classify such algorithms as "AI". I wouldn't, but they are nonetheless on-topic because you might invoke them to assist, focus, refine, or accelerate other techniques.
- deleted 2y ago
  [deleted]
- benreesman 2y ago
  I’m generally a bit of an LLM skeptic, at least as concerns extravagant claims around “AGI” or self-improvement of any of that nonsense. But there are activities where an inherently high-temperature assistant (e.g. some Instruct-inspired tune) are a great fit, and those are almost definitionally at the boundary of “objectively faithful” and “a bit stochastic”. I’ve never done any work in novel mathematics myself, but I’m a big fan of those who do, and any study of those who do paints a picture of roughly that boundary: those who are proficient can easily spot a falsehood but only with difficulty generate inspiration for a new idea. Of all the highly optimistic applications for 2024 LLMs, mathematics sounds pretty plausible?
  - kevinventullo 2y ago
    FWIW as a former mathematician, I believe that if LLM’s can crack mathematics in the sense of say, solving the Riemann Hypothesis through chains of logical reasoning, then we’d be in the back half of reaching “AGI” in the sense of solving broad classes of general problems like drug discovery, or getting fusion to work, or even improving itself.
    - benreesman 2y ago
      Oh sure, I think that’s pretty uncontroversial. An LLM that can with any consistency start at “prove or disprove P = NP” and arrive at a proof is in some sense super-intelligence. Even the best funded boosters are making no such claims AFAIK, I think a much more reasonable and sober assertion might be like “they are useful to doing real mathematics”.
    - adroniser 2y ago
      The curious thing is if you can ever hit a snowball type point, because by proving theorems you are generating training data, and maybe you can get to a point where you effectively have limitless data.
    - quonn 2y ago
      Science needs experiments and those will not go faster because of AI. So why would fusion arrive any faster?
- deleted 2y ago
  [deleted]
- fsmv 2y ago
  Terry Tao has recently been exploring the computer proof writing language Lean and since you can mechanically check the validity of the proof it's perfectly valid to have an AI generate Lean code. If it's wrong Lean will give errors and if it's a valid proof it doesn't matter where it came from.
iamcreasy 2y ago
The article or the linked Google doc doesn't mention how AI for Math resources is different than other resources list out there?
- bitlax 2y ago
  One obvious distinction is that it's recommended by Terry Tao.
- seanhunter 2y ago
  To pick two examples which show the difference other lists might have an article about "Copilot" whereas this one has "Getting copilot to work with Lean4". It's not "Code assistant" it's getting that working with coq etc. ie specifically about AI for maths rather than AI in general
rldjbpin 2y ago
while i am too far removed to make wise comments, it is fascinating that applied maths is being put to use for finding new patterns. after going through the google docs for resources, i get a sense of some high level topics. however, i am confused about the current paradigms. are ml models being used to reduce the search space or as a way to let computers bring about serendipity? it seems like these approaches are like graphing libraries or monte carlo sims that help the user see the bigger picture and then put in their own thinking.
pietroppeter 2y ago
Calling out about the second announcement (erdosproblems.com) that there is a call for help and I think many people here might be able to help and some may be happy to do it. Skills required include GitHub, web design, Python/Html/Sql, … Details: https://www.erdosproblems.com/help https://www.erdosproblems.com/help
- needfish 2y ago
  As a college student learning Web stuff on my own, this is a pretty nice thing to spend summer on.
fsmv 2y ago
Paul Erdős was a very interesting person. I read his biography The Man Who Loved Only Numbers. He couch surfed and wrote papers with others his entire life and became the most prolific published mathematician ever. He also loved to teach kids serious math and not underestimate their thinking. Also I believe his name is pronounced like air-dish.
- wizzwizz4 2y ago
  Closer to (non-rhotic) eh-r, dersh, I would say. But, travelling as he did, I'm sure he was used to all sorts of pronunciations and accents, so I doubt he'd mind overmuch.
JohnMc123 2y ago
[flagged]
gnbarker 2y ago
I'm curious why he is so bullish on AI. The page lists many traditional and actually useful tools like Coq, but much space is devoted to deep learning. My experience with CoPilot shows that it fails at the most simple logical tasks: When presented with an integer sequence it often does not even recognize the number of elements given. It just claims that we are looking for the 10th element when the current sequence only has three. Results are also wrong all the time. Spatial reasoning of CoPilot is not very good. I wonder if early expert systems written in the Lisp era would outperform it. It fails at tasks that require textual awareness like palindromes. What it does very well is confabulating bland short stories and poems. It is great at understanding the input questions. All in all, I am more impressed with Wolfram Alpha, which looks more like a traditional expert system.
- cybertronic 2y ago
  "Slowly, then suddenly." https://x.com/teortaxestex/status/1802128370861232374 https://x.com/teortaxestex/status/1802128370861232374

160 points by nabla9 2y ago

upmind 2y ago

What does AI for Math mean? People doing Math research that want to transition to AI research?

cvoss 2y ago
Broadly, as you'll see in the Google doc linked from the announcement, they are referring to the use of computer systems to assist mathematical research, which falls into a two step process: 1) Identify a suitable language for use by both humans and computers for communication and manipulation of mathematical theorems and their proofs. 2) Employ both mathematicians and machine learning algorithms to generate interesting sentences in that language.
- upmind 2y ago
  That makes a lot more sense, thanks.
- riku_iki 2y ago
  > as you'll see in the Google doc linked from the announcement, they are referring to the use of computer systems to assist mathematical research, which falls into a two step process I reviewed the doc, and it is just curated list of links on various projects (ML frameworks, proof assistant, some tutorials), and does not outline plan you described here. Or I missed something?..
  - cvoss 2y ago
    The first section, Textbooks and Survey Papers, begins with Formal Proof (this is where one identifies the suitable language for mathematics), followed by general Machine Learning references, and concluding with Machine Learning for Formal Proof. Other sections have similar divisions, though some go off into adjacent fields where one finds non-AI* algorithms for specific mathematical applications, such as automated symbolic calculus or SMT solving, to name just two. *Some people's terminology would classify such algorithms as "AI". I wouldn't, but they are nonetheless on-topic because you might invoke them to assist, focus, refine, or accelerate other techniques.
deleted 2y ago
[deleted]
benreesman 2y ago
I’m generally a bit of an LLM skeptic, at least as concerns extravagant claims around “AGI” or self-improvement of any of that nonsense. But there are activities where an inherently high-temperature assistant (e.g. some Instruct-inspired tune) are a great fit, and those are almost definitionally at the boundary of “objectively faithful” and “a bit stochastic”. I’ve never done any work in novel mathematics myself, but I’m a big fan of those who do, and any study of those who do paints a picture of roughly that boundary: those who are proficient can easily spot a falsehood but only with difficulty generate inspiration for a new idea. Of all the highly optimistic applications for 2024 LLMs, mathematics sounds pretty plausible?
- kevinventullo 2y ago
  FWIW as a former mathematician, I believe that if LLM’s can crack mathematics in the sense of say, solving the Riemann Hypothesis through chains of logical reasoning, then we’d be in the back half of reaching “AGI” in the sense of solving broad classes of general problems like drug discovery, or getting fusion to work, or even improving itself.
  - benreesman 2y ago
    Oh sure, I think that’s pretty uncontroversial. An LLM that can with any consistency start at “prove or disprove P = NP” and arrive at a proof is in some sense super-intelligence. Even the best funded boosters are making no such claims AFAIK, I think a much more reasonable and sober assertion might be like “they are useful to doing real mathematics”.
  - adroniser 2y ago
    The curious thing is if you can ever hit a snowball type point, because by proving theorems you are generating training data, and maybe you can get to a point where you effectively have limitless data.
  - quonn 2y ago
    Science needs experiments and those will not go faster because of AI. So why would fusion arrive any faster?
deleted 2y ago
[deleted]
fsmv 2y ago
Terry Tao has recently been exploring the computer proof writing language Lean and since you can mechanically check the validity of the proof it's perfectly valid to have an AI generate Lean code. If it's wrong Lean will give errors and if it's a valid proof it doesn't matter where it came from.

iamcreasy 2y ago

The article or the linked Google doc doesn't mention how AI for Math resources is different than other resources list out there?

bitlax 2y ago
One obvious distinction is that it's recommended by Terry Tao.
seanhunter 2y ago
To pick two examples which show the difference other lists might have an article about "Copilot" whereas this one has "Getting copilot to work with Lean4". It's not "Code assistant" it's getting that working with coq etc. ie specifically about AI for maths rather than AI in general

rldjbpin 2y ago

while i am too far removed to make wise comments, it is fascinating that applied maths is being put to use for finding new patterns. after going through the google docs for resources, i get a sense of some high level topics. however, i am confused about the current paradigms. are ml models being used to reduce the search space or as a way to let computers bring about serendipity? it seems like these approaches are like graphing libraries or monte carlo sims that help the user see the bigger picture and then put in their own thinking.

pietroppeter 2y ago

Calling out about the second announcement (erdosproblems.com) that there is a call for help and I think many people here might be able to help and some may be happy to do it. Skills required include GitHub, web design, Python/Html/Sql, … Details: https://www.erdosproblems.com/help https://www.erdosproblems.com/help

needfish 2y ago
As a college student learning Web stuff on my own, this is a pretty nice thing to spend summer on.

fsmv 2y ago

Paul Erdős was a very interesting person. I read his biography The Man Who Loved Only Numbers. He couch surfed and wrote papers with others his entire life and became the most prolific published mathematician ever. He also loved to teach kids serious math and not underestimate their thinking. Also I believe his name is pronounced like air-dish.

wizzwizz4 2y ago
Closer to (non-rhotic) eh-r, dersh, I would say. But, travelling as he did, I'm sure he was used to all sorts of pronunciations and accents, so I doubt he'd mind overmuch.

JohnMc123 2y ago

[flagged]

gnbarker 2y ago

I'm curious why he is so bullish on AI. The page lists many traditional and actually useful tools like Coq, but much space is devoted to deep learning. My experience with CoPilot shows that it fails at the most simple logical tasks: When presented with an integer sequence it often does not even recognize the number of elements given. It just claims that we are looking for the 10th element when the current sequence only has three. Results are also wrong all the time. Spatial reasoning of CoPilot is not very good. I wonder if early expert systems written in the Lisp era would outperform it. It fails at tasks that require textual awareness like palindromes. What it does very well is confabulating bland short stories and poems. It is great at understanding the input questions. All in all, I am more impressed with Wolfram Alpha, which looks more like a traditional expert system.

cybertronic 2y ago
"Slowly, then suddenly." https://x.com/teortaxestex/status/1802128370861232374 https://x.com/teortaxestex/status/1802128370861232374