Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

AI for math resources, and erdosproblems.com

terrytao.wordpress.com

Post reply on HN
Print view View original

31–39 of 39 posts

Re: AI for math resources, and erdosproblems.com

#31

Post by cvoss »

riku_iki wrote: post #13
cvoss wrote: post #3

Earlier quoted context omitted.

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 interest…

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

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.

Re: AI for math resources, and erdosproblems.com

#32

Post by fsmv »

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.

Re: AI for math resources, and erdosproblems.com

#34

Post by fsmv »

upmind wrote: post #2

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

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.

Re: AI for math resources, and erdosproblems.com

#35

Post by wizzwizz4 »

fsmv wrote: post #32

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.

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.

Re: AI for math resources, and erdosproblems.com

#36

Post by aleph_minus_one »

quonn wrote: post #14
kevinventullo wrote: post #9

Earlier quoted context omitted.

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.

Science needs experiments and those will not go faster because of AI. So why would fusion arrive any faster?

> Science needs experiments and those will not go faster because of AI.

Even though I am deeply skeptical whether AIs (as they are commonly understood today) will be helpful for hard scientific problems (for quite different reasons), I don't think this argument necessarily holds: couldn't a (hypothetical!) AI propose much better experiments and experimental designs?

Re: AI for math resources, and erdosproblems.com

#37

Post by gnbarker »

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.

Re: AI for math resources, and erdosproblems.com

#38

Post by cybertronic »

gnbarker wrote: post #37

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 on…

"Slowly, then suddenly." https://x.com/teortaxestex/status/1802128370861232374

Re: AI for math resources, and erdosproblems.com

#39

Post by quonn »

aleph_minus_one wrote: post #36
quonn wrote: post #14

Earlier quoted context omitted.

Science needs experiments and those will not go faster because of AI. So why would fusion arrive any faster?

> Science needs experiments and those will not go faster because of AI. Even though I am deeply skeptical whether AIs (as they are commonly understood today) will be helpful for hard scientific problems (for quite different reasons), I don't think this argument necessarily holds: couldn't a (hypothetical!) AI propose much better experiments and experimental designs?

That‘s not how science has progressed in the past. It has not progressed by giant leaps of superior intelligence but incrementally and hardly a genius was more than 10 years ahead of his time.
Post reply on HN