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.
If you did not study these topics, the chances are good you do not know what questions to even ask, let alone how to ask them. Add to the fact that you don't even know if the original summary is accurate.
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.
I'm not sure the exact dollar value of feeling safe enough to ask really stupid questions that I should already know the answer to and I'd be embarrassed if anyone saw me ask Claude, but it's more than I'm paying them. Maybe that's the enshittification play. Extra $20/month if you don't want it to sound judgey about your shit.
The answer is you put the top mathematician in the world to do it, easy peasy.
“The argument used some p-adic algebraic number theory which was overkill for this problem. I then spent about half an hour converting the proof by hand into a more elementary proof, which I presented on the site.”
What’s the exchange rate for 30 minutes of Tao’s brain time in regular researcher’s time? 90 days? A year?
Math notation is high context, so it's great to just ask llm's to print out the low context version in something like lisp where I can read and decompose it quickly.
'Vibe formalizing' is a logical extension of 'vibe engineering' implemented by 'vibe coding'. Sometimes I have trouble with getting the individual puzzle pieces of a problem to fall into place, where a hypothetical 'Move 37 As A Service' to unify informal methods with mathematical rigor deserves to be explored!
I had put on the back burner some polyhedral compilation papers. I had read all the material, but some key questions still meant it was not possible for me to implement it. In particular, I was looking at barvinoks counting algorithm and did not understand why you needed to expand the polynomials in a pointed cone. However, chatgpt correctly led me through the reasoning. Could it have made a mistake? Of course. And it did. However, since my confusion meant that I was also wrong, bouncing the idea back and forth was really useful. Plus the ai bots are better at understanding your own particular points of confusion.
I was told by a hungarian, that hungarian written spelling and spoken pronunciation is pretty precisely aligned compared to, say, english. Except when it comes to names when it gets a bit random!
Why not do the bloke the decency to spell his name correctly? Those diacritics are important.
Anyway, I was told that Paul's name is very roughly pronounced by an anglophone as: "airdish".
Ő is just œ (oe), nothing crazy. Certainly not a scenario that would belong to the quirky category.
The only weird ones I can think of are the ones that end in -y. For example, Görgey. They're meant to be -i endings. They signify a noble lineage (or at least used to).
I guess "ch" might also show up every now and then too (it's just "cs", just like "ch" in English). For example, Széchényi.
Since this is a compsci forum to some extent, maybe I should also mention that the so-called Lanczos-interpolation is "actually" Lánczos. Took even me a while to pick up on that one! Thinking about it, I now see that it features a "cz", another letter (digraph) that is longer part of the alphabet.
Also note that Paul is a "translated" name. His actual name was Pál Erdős. He got lucky with that one, it's an easy swap. Edward Teller (Ede Teller) was the same way, and so was John (von) Neumann (János Neumann).
As a bonus trivia, the Hungarian name order is big endian, like the Japanese. So it would be "Erdős Pál", "Teller Ede", "Neumann János", and "Lánczos Kornél". Though just like with Japanese, I would not recommend trying to adhere to this order in most English speaking contexts.
The "weird" part about Hungarian names and words for English speakers is that "y" is a modifier letter in most cases, not a sound in and of itself. So e.g. "Nagy" is pronounced closer to something like "Nahj".
I take it that that's a palatalized ending? I read your comment at first and was like "airdish" wtf? Then I palatalized the 'os' ending and realized oh yeah... that does sound kind of like airdish!
Depends. There are names that are "romanized" to Hungarian pronunciation rules, like Dosztojevszkij (Dostoevsky), or Kolumbusz Kristóf (Cristoforo Colombo - Hungarian puts the family name first), though it is no longer the practice, it's mostly used for historic names only. That is, Trump is written like that, and not as we would pronounce (something like "Trámp")
In general, if the source language has a latin alphabet, we try to stick to the original spelling in most cases, but it is not uncommon to replace non-Hungarian letters with the closest one. It's a bit more complicated in case of non-latin alphabets, especially Cyrillic due to a lot of shared history.
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 e.g. PRA which is the usual theory for finitary proofs also falls prey to Godel's incompleteness theorems). But this is inconsistent with his expressed support for CASes, which very happily manipulate structures that are meant to be infinitary.
He tries to justify this on the grounds that CASes only perform a finite number of symbol manipulations to arrive at an answer, but so too is true for Lean, otherwise typechecking would never terminate. Indeed this is true of any formal system you could run on a computer.
Leaving aside his inconsistent set of arguments for CAS over Lean (and there isn't really a strong distinction between the two honestly; you could argue that Lean and other dependently types proof assistants are just another kind of CAS), his implicit support of ultrafinitism already would require a huge amount of work to make applicable to a computer system. There isn't a consensus on the logical foundations of ultrafinitism yet so building out a proof checker that satisfies ultrafinitistic demands isn't even really well-defined and requires a huge amount of theory crafting.
And just for clarity, finitism is the notion that unboundedness is okay but actual infinities are suspect. E.g. it's okay to say "there are an infinite number of natural numbers" which is understood to be shorthand for "there is no bound on natural numbers" but it's not okay to treat the infinitary object N of all natural numbers as a real thing. So e.g. some finitists are okay with PA over PRA.
On the other hand ultrafinitists deny unboundedness and say that sufficiently large natural numbers simply do not exist (most commonly the operationalization of this is that the question of whether a number exists or not is a matter of computation that scales with the size of the number, if the computation has not completed we cannot have confidence the number exists, and hence sufficiently large numbers for which the relevant computations have not been completed do not exist). This means e.g. quantification or statements of the form "for all natural numbers..." are very dangerous and there's not a complete consensus yet on the correct formalization of this from an ultrafinitistic point of view (or whether such statements would ever be considered coherent).
It seems pretty obviously machine generated, and the appearance of the word "metaphysics" in the output suggests the prompt author didn't know what they were talking about to begin with.
I think Zeilberger is taken heavily out of context and confused with Norman Wildberger a lot; he certainly has some eccentric opinions but that one is not at all reflected in his blog's contents (which are largely things like "[particular paper] presents [conjecture/proof] that can be [resolved/shortened] by routine methods" that are only routine because of his decades of work), it's a shame that him being the go-to example of a crank seems to have become engrained into LLMs
I've had mixed results with AI on research mathematics. I've gotten it to auto-complete non-trivial arguments, and I've found some domains where it seems hopelessly lost. I think we're still at a point in history where mathematicians will not be replaced by AI and can only benefit by dabbling with it.
I've had similar results in both mathematics and programming. For one paper I was writing I wanted to try them and it was a fairly straightforward problem counting the number of permutations. I spent much more time trying to get the AI to figure it out than it took to actually solve it. Couldn't get it to do it even after I solved the problem. Similarly in coding I've had it fail to find trivial bugs like an undefined keyword, which would have easily been caught had I turned on ctags (because the keyword was inherited from a class, which made it so easy to miss). But similarly I've had them succeed on non-trivial tasks and those have been of great help, though nothing has ever been end-to-end just the AI.
So I agree. I think these tools are very helpful, but I also think it is unhelpful that people are trying to sell them as much more than they are. The over hype of them not only legitimizes any pushback but provides ammunition. I believe the truth is that they're helpful tools, but are still far from replacing expertise. I believe that if we try to oversell them then we run the risk of ruining their utility. If you promise the moon you have the deliver the moon. That's different from aiming for the moon and landing in the trees.
I was driving around tonight doing errands and while I was doing so, had a great conversation with chatgpt as to the intimate details of the llvm and GCC pipeline schedulers. It's a huge productivity boost. It has now taken notes for me for some compiler stuff I'm experimenting with. This would previously have been impossible.
Of course it was. No wronger than I'd have been had I started looking into it without its help. On the other hand reading code while driving is terribly dangerous while hands free chatgpt is easy. Moreover I prefer talking for some things.
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"
Because he is smart enough to use the existing (frontier) tools to get good results and create a sort of collaborative environment that is novel for research maths.
As for collaboration I meant: https://terrytao.wordpress.com/2024/09/25/a-pilot-project-in... The issue with horizontal scaling of maths research is trust: if you don't know the author, it is more work to verify their work, especially non-formal proofs. Lean4 enables large projects be split up into pieces where lean can validate each intermediate result, so a much broader group of people can contribute pieces without jeopardizing the overall soundness.
Collaborative environment meaning that any PFY employed by the "AI" providers can read your most intimate thought processes and keep track of embarrassing failures or misconceptions.
Thankfully it's mathematics, so people powerscaling their idols, deifying them at the detriment of others, and putting terms into quotes mockingly, is not what determines whether results hold or not. Perhaps the only field not fundamentally shackled by this type of quackery, even if people try their hardest from time to time to make it so.
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?
4 replies →
If you did not study these topics, the chances are good you do not know what questions to even ask, let alone how to ask them. Add to the fact that you don't even know if the original summary is accurate.
2 replies →
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.
12 replies →
I'm not sure the exact dollar value of feeling safe enough to ask really stupid questions that I should already know the answer to and I'd be embarrassed if anyone saw me ask Claude, but it's more than I'm paying them. Maybe that's the enshittification play. Extra $20/month if you don't want it to sound judgey about your shit.
How do you verify that the explanation is accurate? Mathematical definitions can be very subtle.
The answer is you put the top mathematician in the world to do it, easy peasy.
“The argument used some p-adic algebraic number theory which was overkill for this problem. I then spent about half an hour converting the proof by hand into a more elementary proof, which I presented on the site.”
What’s the exchange rate for 30 minutes of Tao’s brain time in regular researcher’s time? 90 days? A year?
1 reply →
Math notation is high context, so it's great to just ask llm's to print out the low context version in something like lisp where I can read and decompose it quickly.
'Vibe formalizing' is a logical extension of 'vibe engineering' implemented by 'vibe coding'. Sometimes I have trouble with getting the individual puzzle pieces of a problem to fall into place, where a hypothetical 'Move 37 As A Service' to unify informal methods with mathematical rigor deserves to be explored!
I had put on the back burner some polyhedral compilation papers. I had read all the material, but some key questions still meant it was not possible for me to implement it. In particular, I was looking at barvinoks counting algorithm and did not understand why you needed to expand the polynomials in a pointed cone. However, chatgpt correctly led me through the reasoning. Could it have made a mistake? Of course. And it did. However, since my confusion meant that I was also wrong, bouncing the idea back and forth was really useful. Plus the ai bots are better at understanding your own particular points of confusion.
I hope we continue to see gains for scientific professionals and companies doing research.
Even imperfect assistants increase leverage.
iOS formalization app mentioned by Tao (beta)
https://aristotle.harmonic.fun/
TIL: startup founded by Robin Hood CEO
Erdős
I was told by a hungarian, that hungarian written spelling and spoken pronunciation is pretty precisely aligned compared to, say, english. Except when it comes to names when it gets a bit random!
Why not do the bloke the decency to spell his name correctly? Those diacritics are important.
Anyway, I was told that Paul's name is very roughly pronounced by an anglophone as: "airdish".
(I saw this on a math department bulletin board about 1960)
A theorem both deep and profound States that every circle is round But in a paper by Erdos Written in Kurdish A counterexample is found
I suspect there is a great joke embedded in here, but sadly it went over my head. Any help?
1 reply →
Ő is just œ (oe), nothing crazy. Certainly not a scenario that would belong to the quirky category.
The only weird ones I can think of are the ones that end in -y. For example, Görgey. They're meant to be -i endings. They signify a noble lineage (or at least used to).
I guess "ch" might also show up every now and then too (it's just "cs", just like "ch" in English). For example, Széchényi.
Since this is a compsci forum to some extent, maybe I should also mention that the so-called Lanczos-interpolation is "actually" Lánczos. Took even me a while to pick up on that one! Thinking about it, I now see that it features a "cz", another letter (digraph) that is longer part of the alphabet.
Also note that Paul is a "translated" name. His actual name was Pál Erdős. He got lucky with that one, it's an easy swap. Edward Teller (Ede Teller) was the same way, and so was John (von) Neumann (János Neumann).
As a bonus trivia, the Hungarian name order is big endian, like the Japanese. So it would be "Erdős Pál", "Teller Ede", "Neumann János", and "Lánczos Kornél". Though just like with Japanese, I would not recommend trying to adhere to this order in most English speaking contexts.
The "weird" part about Hungarian names and words for English speakers is that "y" is a modifier letter in most cases, not a sound in and of itself. So e.g. "Nagy" is pronounced closer to something like "Nahj".
2 replies →
I take it that that's a palatalized ending? I read your comment at first and was like "airdish" wtf? Then I palatalized the 'os' ending and realized oh yeah... that does sound kind of like airdish!
I could be wrong, but FWIW I doubt Hungarians include diacritics that don’t exist in Hungarian (like ñ) when writing foreign names.
Depends. There are names that are "romanized" to Hungarian pronunciation rules, like Dosztojevszkij (Dostoevsky), or Kolumbusz Kristóf (Cristoforo Colombo - Hungarian puts the family name first), though it is no longer the practice, it's mostly used for historic names only. That is, Trump is written like that, and not as we would pronounce (something like "Trámp")
In general, if the source language has a latin alphabet, we try to stick to the original spelling in most cases, but it is not uncommon to replace non-Hungarian letters with the closest one. It's a bit more complicated in case of non-latin alphabets, especially Cyrillic due to a lot of shared history.
3 replies →
You are wrong.
Diacritics are language-dependent, so using hungarian-meaning diacritics into english text makes no sense.
Is not American so nobody here cares...
Irrelevant. Cf. Diogenes on death
Sounds like nihilism for beginners.
1 reply →
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
1 reply →
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 e.g. PRA which is the usual theory for finitary proofs also falls prey to Godel's incompleteness theorems). But this is inconsistent with his expressed support for CASes, which very happily manipulate structures that are meant to be infinitary.
He tries to justify this on the grounds that CASes only perform a finite number of symbol manipulations to arrive at an answer, but so too is true for Lean, otherwise typechecking would never terminate. Indeed this is true of any formal system you could run on a computer.
Leaving aside his inconsistent set of arguments for CAS over Lean (and there isn't really a strong distinction between the two honestly; you could argue that Lean and other dependently types proof assistants are just another kind of CAS), his implicit support of ultrafinitism already would require a huge amount of work to make applicable to a computer system. There isn't a consensus on the logical foundations of ultrafinitism yet so building out a proof checker that satisfies ultrafinitistic demands isn't even really well-defined and requires a huge amount of theory crafting.
And just for clarity, finitism is the notion that unboundedness is okay but actual infinities are suspect. E.g. it's okay to say "there are an infinite number of natural numbers" which is understood to be shorthand for "there is no bound on natural numbers" but it's not okay to treat the infinitary object N of all natural numbers as a real thing. So e.g. some finitists are okay with PA over PRA.
On the other hand ultrafinitists deny unboundedness and say that sufficiently large natural numbers simply do not exist (most commonly the operationalization of this is that the question of whether a number exists or not is a matter of computation that scales with the size of the number, if the computation has not completed we cannot have confidence the number exists, and hence sufficiently large numbers for which the relevant computations have not been completed do not exist). This means e.g. quantification or statements of the form "for all natural numbers..." are very dangerous and there's not a complete consensus yet on the correct formalization of this from an ultrafinitistic point of view (or whether such statements would ever be considered coherent).
2 replies →
It seems pretty obviously machine generated, and the appearance of the word "metaphysics" in the output suggests the prompt author didn't know what they were talking about to begin with.
1 reply →
[flagged]
I think Zeilberger is taken heavily out of context and confused with Norman Wildberger a lot; he certainly has some eccentric opinions but that one is not at all reflected in his blog's contents (which are largely things like "[particular paper] presents [conjecture/proof] that can be [resolved/shortened] by routine methods" that are only routine because of his decades of work), it's a shame that him being the go-to example of a crank seems to have become engrained into LLMs
I've had mixed results with AI on research mathematics. I've gotten it to auto-complete non-trivial arguments, and I've found some domains where it seems hopelessly lost. I think we're still at a point in history where mathematicians will not be replaced by AI and can only benefit by dabbling with it.
I've had similar results in both mathematics and programming. For one paper I was writing I wanted to try them and it was a fairly straightforward problem counting the number of permutations. I spent much more time trying to get the AI to figure it out than it took to actually solve it. Couldn't get it to do it even after I solved the problem. Similarly in coding I've had it fail to find trivial bugs like an undefined keyword, which would have easily been caught had I turned on ctags (because the keyword was inherited from a class, which made it so easy to miss). But similarly I've had them succeed on non-trivial tasks and those have been of great help, though nothing has ever been end-to-end just the AI.
So I agree. I think these tools are very helpful, but I also think it is unhelpful that people are trying to sell them as much more than they are. The over hype of them not only legitimizes any pushback but provides ammunition. I believe the truth is that they're helpful tools, but are still far from replacing expertise. I believe that if we try to oversell them then we run the risk of ruining their utility. If you promise the moon you have the deliver the moon. That's different from aiming for the moon and landing in the trees.
I was driving around tonight doing errands and while I was doing so, had a great conversation with chatgpt as to the intimate details of the llvm and GCC pipeline schedulers. It's a huge productivity boost. It has now taken notes for me for some compiler stuff I'm experimenting with. This would previously have been impossible.
Based on my experience, I would expect that the LLM was wrong about some of those details. Of course, your mileage (see what I did there?) may vary.
Of course it was. No wronger than I'd have been had I started looking into it without its help. On the other hand reading code while driving is terribly dangerous while hands free chatgpt is easy. Moreover I prefer talking for some things.
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".
1 reply →
that also brings the philosophycal question of will I be the same if all my atoms and molecules are copied exactly the same?
3 replies →
They should name one of the AI's "Erdos". Then we can all have an Erdos number of one!
Or a successor of https://en.wikipedia.org/wiki/DR-DOS.
There is an AI-integrated IDE called Erdos...
https://www.lotas.ai/erdos
[flagged]
Because he is smart enough to use the existing (frontier) tools to get good results and create a sort of collaborative environment that is novel for research maths.
As for collaboration I meant: https://terrytao.wordpress.com/2024/09/25/a-pilot-project-in... The issue with horizontal scaling of maths research is trust: if you don't know the author, it is more work to verify their work, especially non-formal proofs. Lean4 enables large projects be split up into pieces where lean can validate each intermediate result, so a much broader group of people can contribute pieces without jeopardizing the overall soundness.
Collaborative environment meaning that any PFY employed by the "AI" providers can read your most intimate thought processes and keep track of embarrassing failures or misconceptions.
3 replies →
Indeed. Who’s to say whether Wiles would have used AI assistance if it had, you know, existed, in 1994.
1 reply →
Thankfully it's mathematics, so people powerscaling their idols, deifying them at the detriment of others, and putting terms into quotes mockingly, is not what determines whether results hold or not. Perhaps the only field not fundamentally shackled by this type of quackery, even if people try their hardest from time to time to make it so.
[flagged]
1 reply →