5 ms·

A working mathematician recently got GPT-4o to prove an (afaik) novel lemma while pursuing their research: "My partner, who is mathematician, used ChatGPT last

A working mathematician recently got GPT-4o to prove an (afaik) novel lemma while pursuing their research: "My partner, who is mathematician, used ChatGPT last week for the first time to prove some lemmas for his research. He already suspected those lemmas were true and had some vague idea how to approach them, but he wasn't expert in this type of statement. This is the first time that he got correct and useful proofs out of the models. [...] These are the two lemmas. The first one is something that a collaborator of my partner noticed for small values of e in their computations. ChatGPT did not find the proof before being told to try Mobius functions. https://chatgpt.com/share/9ee33e31-7cec-4847-92e4-eebb48d4ffea https://chatgpt.com/share/9ee33e31-7cec-4847-92e4-eebb48d4ff... The second looks a bit more standard to me, probably something that Mathematica would have been able to do as well. But perhaps that's just because I am more familiar with such formulas. Still, Mathematica doesn't give a nice derivation, so this is useful. https://chatgpt.com/share/7335f11d-f7c0-4093-a761-1090a21579b4 https://chatgpt.com/share/7335f11d-f7c0-4093-a761-1090a21579... "

a_wild_dandan 2y ago
In a recent interview, Ben Goertzel mentioned having a PhD-level discussion with GPT-4 about novel math ideas cooked up by himself and a colleague. These things are becoming scary good at reasoning and heavyweight topics. As the ML field continues focusing on adding more System Two capabilities to complement LLMs' largely System One thinking, things will get wild.
- _yb2s 2y ago
  This is my experience as well- even the popular hype underestimates how creative and intelligent LLMs can be. Most discussions are reasoning about what it should or shouldn’t be capable of based on how we think they work, without really looking directly at what is can actually do, and not focusing on what it can’t do. They are very alien- much worse than humans at many things, but also much better at others. And not in the areas we would expect in both cases. Ironically they are especially good at creative and abstract thinking and very bad at keeping track of details and basic computation, nearly the opposite of what we’d expect from computers.
  - mu53 2y ago
    I am pessimistic about AI. The technology is definitely useful, but I watched a video that made good points. * On benchmark style tests, LLMs are not improving. GPT-4o is equivalent to GPT-4 and both barely improve on GPT-3.5T. * AI companies have been caught outright lying in demos and manipulating outcomes by pre-training for certain scenarios. * The main features added to GPT-4o have been features that manipulate humans with dark patterns * The dark patterns include emotional affects in tone and cute/quirky responses * These dark patterns encourage people to think of LLMs as humans that have a similar processing of the universe. I seriously wonder about the transcript that these guys had with the LLM. Were they suggesting things? Did ChatGPT just reconfigure words that helped them think through the problem? I think the truth is that ChatGPT is a very effective rubber duck debugger. > https://www.youtube.com/watch?v=VctsqOo8wsc https://www.youtube.com/watch?v=VctsqOo8wsc
    - _yb2s 2y ago
      Try playing around with getting GPT-4 to discuss creative solutions to real unsolved problems you are personally an expert on, or created yourself. That video looks like just standard internet ragebait to me. I find it pretty annoying when people say you are just being manipulated by hype if you are impressed by LLMs, when I was a serious skeptic, thought GPT-3 was useless, and only changed my opinion by directly experimenting with GPT-4 on my own- by getting it to discuss and solve problems in my area of expertise as an academic researcher.
      - refulgentis 2y ago
        Its the new eternal summer, welcome to the club :) GPT-3 was translating 2000 lines of code across 5 languages and enabling me to ship at scale
        cdelsolar 2y ago
        I don’t know Jack about C# and .NET and I’ve used ChatGPT to write several nontrivial programs.
krackers 2y ago
Woah that second proof is really slick. Is there a combinatorial proof instead of algebraic proof as to why that holds?
- gjm11 2y ago
  Yes. (HN comments aren't the best medium for writing mathematics. I hope this ends up reasonably readable.) (d choose k) is the number of ways to pick k things from d. (d choose k) k^2 is the number of ways to pick k things from d, and then colour one of them red and one of them (possibly the same one) blue. (-1)^k (d choose k) k^2 is that (when k is even), or minus that (when k is odd). So the identity says: Suppose we consider a set of d things, and we consider picking some of them (meaning 0 or more, though actually 0 is impossible; k is the number we pick) and colouring one of those red and one blue; then there are the same number of ways to do this picking an odd number of things as picking an even number. Well, let's describe the process a bit differently. We take our set of d things. We colour one of them red. We colour one of them blue. Then we pick some set of the things (k in number), including the red thing and the blue thing (which may or may not also be the red thing). And the claim is that there are the same number of ways to do this with an even value of k as with an odd number. But now this is almost trivial! Once we've picked our red and blue things, we just have to decide which of the other things to pick. And as long as there's at least one of those, there are as many ways to pick an odd number of things as to pick an even number. (Fix one of them; we can either include it or not, and switching that changes the parity.) So if d>2 then we're done -- for each choice of red and blue, there are the same number of "odd" and "even" ways to finish the job. What if d<=2? Well, then the "theorem" isn't actually true. d=1: (1 choose 0) 0^2 - (1 choose 1) 1^2 = -1. d=2: (2 choose 0) 0^2 - (2 choose 1) 1^2 + (2 choose 2) 2^2 = 2.
  - krackers 2y ago
    >We take our set of d things. We colour one of them red. We colour one of them blue. Then we pick some set of the things (k in number), including the red thing and the blue thing In this alternate view of the process, where does the k^2 term come from? Isn't the number of ways to do it in this perspective just (d-1 choose k-1) # We already chose the red one (which is also the blue) and need to choose k-1 more + (d-2 choose k-2) # We chose both red and blue ones and need to choose the other k-2 Edit: I think it actually works out, seems to be equal to d * 1 * Binomial[d - 1, k - 1] + d * (d - 1) * Binomial[d - 2, k - 2] = Binomial[d, k]*k^2 And then you apply your argument about fixing one of the elements in each of the two cases. Actually the proof seems to be a variant (same core argument) as sum of even binomial terms = sum of odd binomial terms [1] [1] https://math.stackexchange.com/questions/313832/a-combinatorial-proof-that-the-alternating-sum-of-binomial-coefficients-is-zero https://math.stackexchange.com/questions/313832/a-combinator...
Sniffnoy 2y ago
Sorry, what is this quoted from? It's interesting because that first one is something I was discussing recently with my friend Beren (does he have an account here? idk). We were thinking of it as summing over ordered partitions, rather than over partitions with a factor of |tau|!, but obviously those are the same thing. (If you do it over cyclically ordered partitions -- so, a factor of (|tau|-1)! rather than |tau|! -- you get 0 instead of (-1)^e.) Here's Beren's combinatorial proof: First let's do the second one I said, about cyclically ordered ones, because it's easier. Choose one element of the original set to be special. Now we can set up a bijection between even-length and odd-length cyclically ordered partitions as follows: If the special element is on its own, merge it with the part after it. If it's not on its own, split it out into its own part before the part it's in. So if we sum with a sign factor, we get 0. OK, so what about the linearly ordered case? We'll use a similar bijection, except it won't quite be a bijection this time. Pick an order on your set. Apply the above bijection with the last element as the special element. Except some things don't get matched, namely, partitions that have the last element of your set on its own as the last part. So in that case, take the second-to-last element, and apply recursively, etc, etc. Ultimately everything gets matched except for the paritition where everything is separate and all the parts are in order. This partition has length equal to the size of the original set. So if the original set was even you get one more even one, and if the original set was odd you get one more odd one. Which rephrased as a sum with a sign factor yields the original statement. Would be interested to send this to the mathematician you're referring to, but I have no idea who that might be since you didn't say. :)
- Tossrock 2y ago
  this was from the current ACX Open Thread
  - Sniffnoy 2y ago
    Thanks! Went and posted over there.
fovc 2y ago
I’m pretty sure that 2nd proof exists in some book or ebook somewhere. generating functionology was the one that came to mind. Impressive recall, but not novel reasoning
- williamcotton 2y ago
  I’m pretty sure that LLMs can generalize a deep model and can create novel assemblages and are not just search engines. The burden of proof would be on you to find the existing mathematical, erhm, proof.
deleted 2y ago
[deleted]
Chinjut 2y ago
ChatGPT just spit out nonsense in the first example. Look at the sum in step 6, over τ ≤ τ. Is τ the bound variable of the summation or a free variable? Put another way, how many terms are in this summation over "τ ≤ τ"? And how does this relate to establishing either the LHS or RHS of part 3, to then conclude the other side? Nothing actually coheres. What happened here is that ChatGPT remembered the Möbius function for the partition lattice, regurgitated it* without providing proof, and then spit out some nonsense afterwards that looks superficially reasonable. But establishing that Möbius function is essentially the whole ballgame! The question being asked is very nearly the same as just being asked to prove that the Möbius function has that form. [*: The regurgitation also has a slight error, as μ(τ, σ) with τ a refinement of σ is actually (-1)^(|τ| - |σ|) * the product of (|τ restricted to c| - 1)! over each equivalence class c in σ. The formula given by ChatGPT matches this one when |σ| = 1, which is the important case for the proof at hand, but is incorrect more generally.] ---- For what it's worth, the desired fact can be shown just by elementary induction, without explicitly invoking all the Möbius function machinery anyway: Let N(t, e) be the number of partitions of {1, ..., e} into t many equivalence classes [we will always take e to be a non-negative integer, but allow for t to be an arbitrary integer, with N(t, e) = 0 when t is negative]. The sum in question is of (-1)^t * t! * N(t, e) over all t. Refer to this sum as Sum(e). We wish to show that Sum(e) comes out to (-1)^e. Since Sum(0) = 1 trivially, what we need to show is that Sum(e + 1) = -Sum(e). There are two kinds of partitions on the set {1, ..., e + 1}: Those which put e + 1 in an equivalence class all on its own and those which put it in the same equivalence class as some value or values in {1, ..., e}. From this, we obtain the recurrence N(t, e + 1) = N(t - 1, e) + t * N(t, e). Accordingly, Sum(e + 1) = Sum of (-1)^t * t! * N(t, e + 1) over all t = Sum of (-1)^t * t! * N(t - 1, e) over all t, plus sum of (-1)^t * t! * t * N(t, e) over all t. The first of these two sub-sums can be reparametrized as the sum of (-1)^(t + 1) * (t + 1)! * N(t, e) over all t. Now recombining the two sub-sums term-wise, and keeping in mind (-1)^(t + 1) * (t + 1)! = (-t - 1) * (-1)^t * t!, we get Sum(e + 1) = sum of (-1)^t * t! * (-t - 1 + t) * N(t, e) over all t. As (-t - 1 + t) = -1, this comes to -Sum(e) as desired, completing the proof.
- Chinjut 2y ago
  The second ChatGPT example proof is mostly fine, except it failed to see that the claimed theorem isn't actually true at d = 2. (It writes "d ≥ 2" for a step in its reasoning where d ≥ 3 is actually required.)

a_wild_dandan 2y ago

In a recent interview, Ben Goertzel mentioned having a PhD-level discussion with GPT-4 about novel math ideas cooked up by himself and a colleague. These things are becoming scary good at reasoning and heavyweight topics. As the ML field continues focusing on adding more System Two capabilities to complement LLMs' largely System One thinking, things will get wild.

_yb2s 2y ago
This is my experience as well- even the popular hype underestimates how creative and intelligent LLMs can be. Most discussions are reasoning about what it should or shouldn’t be capable of based on how we think they work, without really looking directly at what is can actually do, and not focusing on what it can’t do. They are very alien- much worse than humans at many things, but also much better at others. And not in the areas we would expect in both cases. Ironically they are especially good at creative and abstract thinking and very bad at keeping track of details and basic computation, nearly the opposite of what we’d expect from computers.
- mu53 2y ago
  I am pessimistic about AI. The technology is definitely useful, but I watched a video that made good points. * On benchmark style tests, LLMs are not improving. GPT-4o is equivalent to GPT-4 and both barely improve on GPT-3.5T. * AI companies have been caught outright lying in demos and manipulating outcomes by pre-training for certain scenarios. * The main features added to GPT-4o have been features that manipulate humans with dark patterns * The dark patterns include emotional affects in tone and cute/quirky responses * These dark patterns encourage people to think of LLMs as humans that have a similar processing of the universe. I seriously wonder about the transcript that these guys had with the LLM. Were they suggesting things? Did ChatGPT just reconfigure words that helped them think through the problem? I think the truth is that ChatGPT is a very effective rubber duck debugger. > https://www.youtube.com/watch?v=VctsqOo8wsc https://www.youtube.com/watch?v=VctsqOo8wsc
  - _yb2s 2y ago
    Try playing around with getting GPT-4 to discuss creative solutions to real unsolved problems you are personally an expert on, or created yourself. That video looks like just standard internet ragebait to me. I find it pretty annoying when people say you are just being manipulated by hype if you are impressed by LLMs, when I was a serious skeptic, thought GPT-3 was useless, and only changed my opinion by directly experimenting with GPT-4 on my own- by getting it to discuss and solve problems in my area of expertise as an academic researcher.
    - refulgentis 2y ago
      Its the new eternal summer, welcome to the club :) GPT-3 was translating 2000 lines of code across 5 languages and enabling me to ship at scale
      - cdelsolar 2y ago
        I don’t know Jack about C# and .NET and I’ve used ChatGPT to write several nontrivial programs.

krackers 2y ago

Woah that second proof is really slick. Is there a combinatorial proof instead of algebraic proof as to why that holds?

gjm11 2y ago
Yes. (HN comments aren't the best medium for writing mathematics. I hope this ends up reasonably readable.) (d choose k) is the number of ways to pick k things from d. (d choose k) k^2 is the number of ways to pick k things from d, and then colour one of them red and one of them (possibly the same one) blue. (-1)^k (d choose k) k^2 is that (when k is even), or minus that (when k is odd). So the identity says: Suppose we consider a set of d things, and we consider picking some of them (meaning 0 or more, though actually 0 is impossible; k is the number we pick) and colouring one of those red and one blue; then there are the same number of ways to do this picking an odd number of things as picking an even number. Well, let's describe the process a bit differently. We take our set of d things. We colour one of them red. We colour one of them blue. Then we pick some set of the things (k in number), including the red thing and the blue thing (which may or may not also be the red thing). And the claim is that there are the same number of ways to do this with an even value of k as with an odd number. But now this is almost trivial! Once we've picked our red and blue things, we just have to decide which of the other things to pick. And as long as there's at least one of those, there are as many ways to pick an odd number of things as to pick an even number. (Fix one of them; we can either include it or not, and switching that changes the parity.) So if d>2 then we're done -- for each choice of red and blue, there are the same number of "odd" and "even" ways to finish the job. What if d<=2? Well, then the "theorem" isn't actually true. d=1: (1 choose 0) 0^2 - (1 choose 1) 1^2 = -1. d=2: (2 choose 0) 0^2 - (2 choose 1) 1^2 + (2 choose 2) 2^2 = 2.
- krackers 2y ago
  >We take our set of d things. We colour one of them red. We colour one of them blue. Then we pick some set of the things (k in number), including the red thing and the blue thing In this alternate view of the process, where does the k^2 term come from? Isn't the number of ways to do it in this perspective just (d-1 choose k-1) # We already chose the red one (which is also the blue) and need to choose k-1 more + (d-2 choose k-2) # We chose both red and blue ones and need to choose the other k-2 Edit: I think it actually works out, seems to be equal to d * 1 * Binomial[d - 1, k - 1] + d * (d - 1) * Binomial[d - 2, k - 2] = Binomial[d, k]*k^2 And then you apply your argument about fixing one of the elements in each of the two cases. Actually the proof seems to be a variant (same core argument) as sum of even binomial terms = sum of odd binomial terms [1] [1] https://math.stackexchange.com/questions/313832/a-combinatorial-proof-that-the-alternating-sum-of-binomial-coefficients-is-zero https://math.stackexchange.com/questions/313832/a-combinator...

Sniffnoy 2y ago

Sorry, what is this quoted from? It's interesting because that first one is something I was discussing recently with my friend Beren (does he have an account here? idk). We were thinking of it as summing over ordered partitions, rather than over partitions with a factor of |tau|!, but obviously those are the same thing. (If you do it over cyclically ordered partitions -- so, a factor of (|tau|-1)! rather than |tau|! -- you get 0 instead of (-1)^e.) Here's Beren's combinatorial proof: First let's do the second one I said, about cyclically ordered ones, because it's easier. Choose one element of the original set to be special. Now we can set up a bijection between even-length and odd-length cyclically ordered partitions as follows: If the special element is on its own, merge it with the part after it. If it's not on its own, split it out into its own part before the part it's in. So if we sum with a sign factor, we get 0. OK, so what about the linearly ordered case? We'll use a similar bijection, except it won't quite be a bijection this time. Pick an order on your set. Apply the above bijection with the last element as the special element. Except some things don't get matched, namely, partitions that have the last element of your set on its own as the last part. So in that case, take the second-to-last element, and apply recursively, etc, etc. Ultimately everything gets matched except for the paritition where everything is separate and all the parts are in order. This partition has length equal to the size of the original set. So if the original set was even you get one more even one, and if the original set was odd you get one more odd one. Which rephrased as a sum with a sign factor yields the original statement. Would be interested to send this to the mathematician you're referring to, but I have no idea who that might be since you didn't say. :)

Tossrock 2y ago
this was from the current ACX Open Thread
- Sniffnoy 2y ago
  Thanks! Went and posted over there.

fovc 2y ago

I’m pretty sure that 2nd proof exists in some book or ebook somewhere. generating functionology was the one that came to mind. Impressive recall, but not novel reasoning

williamcotton 2y ago
I’m pretty sure that LLMs can generalize a deep model and can create novel assemblages and are not just search engines. The burden of proof would be on you to find the existing mathematical, erhm, proof.

deleted 2y ago

[deleted]

Chinjut 2y ago

ChatGPT just spit out nonsense in the first example. Look at the sum in step 6, over τ ≤ τ. Is τ the bound variable of the summation or a free variable? Put another way, how many terms are in this summation over "τ ≤ τ"? And how does this relate to establishing either the LHS or RHS of part 3, to then conclude the other side? Nothing actually coheres. What happened here is that ChatGPT remembered the Möbius function for the partition lattice, regurgitated it* without providing proof, and then spit out some nonsense afterwards that looks superficially reasonable. But establishing that Möbius function is essentially the whole ballgame! The question being asked is very nearly the same as just being asked to prove that the Möbius function has that form. [*: The regurgitation also has a slight error, as μ(τ, σ) with τ a refinement of σ is actually (-1)^(|τ| - |σ|) * the product of (|τ restricted to c| - 1)! over each equivalence class c in σ. The formula given by ChatGPT matches this one when |σ| = 1, which is the important case for the proof at hand, but is incorrect more generally.] ---- For what it's worth, the desired fact can be shown just by elementary induction, without explicitly invoking all the Möbius function machinery anyway: Let N(t, e) be the number of partitions of {1, ..., e} into t many equivalence classes [we will always take e to be a non-negative integer, but allow for t to be an arbitrary integer, with N(t, e) = 0 when t is negative]. The sum in question is of (-1)^t * t! * N(t, e) over all t. Refer to this sum as Sum(e). We wish to show that Sum(e) comes out to (-1)^e. Since Sum(0) = 1 trivially, what we need to show is that Sum(e + 1) = -Sum(e). There are two kinds of partitions on the set {1, ..., e + 1}: Those which put e + 1 in an equivalence class all on its own and those which put it in the same equivalence class as some value or values in {1, ..., e}. From this, we obtain the recurrence N(t, e + 1) = N(t - 1, e) + t * N(t, e). Accordingly, Sum(e + 1) = Sum of (-1)^t * t! * N(t, e + 1) over all t = Sum of (-1)^t * t! * N(t - 1, e) over all t, plus sum of (-1)^t * t! * t * N(t, e) over all t. The first of these two sub-sums can be reparametrized as the sum of (-1)^(t + 1) * (t + 1)! * N(t, e) over all t. Now recombining the two sub-sums term-wise, and keeping in mind (-1)^(t + 1) * (t + 1)! = (-t - 1) * (-1)^t * t!, we get Sum(e + 1) = sum of (-1)^t * t! * (-t - 1 + t) * N(t, e) over all t. As (-t - 1 + t) = -1, this comes to -Sum(e) as desired, completing the proof.

Chinjut 2y ago
The second ChatGPT example proof is mostly fine, except it failed to see that the claimed theorem isn't actually true at d = 2. (It writes "d ≥ 2" for a step in its reasoning where d ≥ 3 is actually required.)