Live data from Hacker News

Terence Tao: At the Erdos problem website, AI assistance now becoming routine

mathstodon.xyz

51–60 of 96 posts

Re: Terence Tao: At the Erdos problem website, AI assistance now becoming routine

#51

Earlier quoted context omitted.

I'm not a mathematician, but how credible is that anti-Lean material? Are they marketing an alternative programmatic approach, as in they're anti-lean because "I got something else" or are they philosophically anti-Lean and have valid arguments?

It's mainly the latter, although the author makes half-hearted gestures as some sort of CAS (Computer Algebra System) being better. It's not very credible. There are individual fragments that make sense but it's not consistent when taken together. For example, by making reference to Godelian problems and his overall mistrust of infinitary structures, he's implicitly endorsing ultrafinitism (not just finitism because…

I wonder what the ultrafinist argument against theorems about the natural numbers as defined in Coq would be.

Re: Terence Tao: At the Erdos problem website, AI assistance now becoming routine

#52

Earlier quoted context omitted.

Isn't there a risk that you're engaging with an inaccurate summarization? At some point inaccurate information is worse than no information. Perhaps in low stakes situations it could at least guarantee some entertainment value. Though I worry that folks will get into high stakes situations without the tools to distinguish facts from smoothly worded slop.

There is, but there is an equal risk if you were to engage about any topic with any teacher you know. Everyone has a bias, and as long as you dont base your worldview and decisions fully on one output you will be fine.

Are you just saying that broadly, e.g. original 2022 chatgpt was also an equal risk if you use this way?

You won't be able to verify everything taught from first principles, so do have to at some point give different sources different credibility I think.

Re: Terence Tao: At the Erdos problem website, AI assistance now becoming routine

#53

Also interesting that the responses include anti-Lean material.

Due to his position and general fame, Tao has to deal with a larger-than-usual number of kooks.

Even on Mathstodon, where there are on average 1 replies and 1 likes per comment

Re: Terence Tao: At the Erdos problem website, AI assistance now becoming routine

#54

Having the ability to throw math heavy ML papers at the assistants and get simplified explanations / pseudocode back is absolutely amazing, as someone who's forgot most of what I learned in uni, 25+ years back and never really used it since.

How do you verify that the explanation is accurate? Mathematical definitions can be very subtle.

Re: Terence Tao: At the Erdos problem website, AI assistance now becoming routine

#56
post #27

Having the ability to throw math heavy ML papers at the assistants and get simplified explanations / pseudocode back is absolutely amazing, as someone who's forgot most of what I learned in uni, 25+ years back and never really used it since.

This is where LLMs shine for learning imo: throwing a paper in Claude and getting an overview then being able to ask questions. Especially for fields that I didn’t study at the Bachelors or Masters level, like biology. Getting to engage with deeper research with a knowledgeable tutor assistant has enabled me to go deeper than I otherwise could.

How do you know its correct? And how do you learn to engage with the theory heavy subject doing it this way?

Re: Terence Tao: At the Erdos problem website, AI assistance now becoming routine

#57

Earlier quoted context omitted.

Isn't there a risk that you're engaging with an inaccurate summarization? At some point inaccurate information is worse than no information. Perhaps in low stakes situations it could at least guarantee some entertainment value. Though I worry that folks will get into high stakes situations without the tools to distinguish facts from smoothly worded slop.

There is, but there is an equal risk if you were to engage about any topic with any teacher you know. Everyone has a bias, and as long as you dont base your worldview and decisions fully on one output you will be fine.

>but there is an equal risk if you were to engage about any topic with any teacher you know.

No it isnt.

Re: Terence Tao: At the Erdos problem website, AI assistance now becoming routine

#58
post #55

I still can't believe that we are in the era of 'star trek' like "Computer plot me a proof for this math problem" in my life time! Wish we could also do the same for "Beam me up scotty"

> Wish we could also do the same for "Beam me up scotty"

You might die every time you do, though, so maybe not.

Re: Terence Tao: At the Erdos problem website, AI assistance now becoming routine

#59

Earlier quoted context omitted.

Isn't there a risk that you're engaging with an inaccurate summarization? At some point inaccurate information is worse than no information. Perhaps in low stakes situations it could at least guarantee some entertainment value. Though I worry that folks will get into high stakes situations without the tools to distinguish facts from smoothly worded slop.

There is, but there is an equal risk if you were to engage about any topic with any teacher you know. Everyone has a bias, and as long as you dont base your worldview and decisions fully on one output you will be fine.

It’s my experience that humans are far, far, far more trustworthy about their limitations than LLMs. Obviously, this varies by human.

Re: Terence Tao: At the Erdos problem website, AI assistance now becoming routine

#60
post #55

I still can't believe that we are in the era of 'star trek' like "Computer plot me a proof for this math problem" in my life time! Wish we could also do the same for "Beam me up scotty"

> Wish we could also do the same for "Beam me up scotty" You might die every time you do, though, so maybe not.

For some definitions of "you" and "die".
Post reply on HN