An update on this post, from my inside sources:
word on the math streets of SF is that the OpenAI team tried something like 500 problems to get their 10 solutions.
I don’t know how much of an insider this source is (or this sources sources, etc), but (allowing for the possibility of confirmation bias) this is within the expected range.
Word on the street is also that they have plenty of unreleased results, though. How does that figure in?
I don’t know! I’m sure we agree that one can generate a huge amount of results which if they had been written by humans could be published in a reasonable journal (if not necessarily a good to great journal).
Just FYI it looks like Fable 5.1 has comments on one of your linear independence paper at https://x.com/slimer48484/status/2095025538670723506
Since I don’t have a twitter account it’s a little hard to see exactly what they are saying, but from what I can make out:
1. It detects an error in one of the examples we gave around Lemma 2.11.13. This is a totally valid complaint. In fact, it was also one previously detected by humans! If you go to the version on our webpages you will see that it has already been fixed. My (positive) thoughts on using LLMs for helping to self-review papers is given in this post.
2. It modifies the denominator \((1-4x)^{-1/2}\) used in this example by replacing it to be of the form \((1-ax)^{b}\) for suitable rational \(a\) and \(b\) chosen to guarantee suitable bounds for the denominator growth. This is a perfectly valid thing to do. For example, even just replacing \((1-4x)^{-1/2}\) with \((1-4mx)^{-1/2}\) for a positive integer \(m > 1\) you obviously get a linear independence result by exactly the same proof (actually easier in some technical sense because the overconvergent singularity gets close to zero). The problem is the periods you get are just … less interesting, which is why we didn’t even mention it. One of the key difficulties in this subject is massaging the numbers you most want to prove to be irrational into this scheme.
Thank you! I’ve linked to your post on X. I’m sorry I forgot to remove “one of” in my comment above, and I realized a better place for the comment is probably https://galoisrepresentations.org/2024/06/16/a-talk-on-my-new-work-with-vesselin-dimitrov-and-yunqing-tang-on-irrationality/
I was particularly concerned because I posed your Theorem A and C as formalization challenges at https://lean-lang.org/eval/problems/cdt_linearIndependent/ and want to ensure the statement is not problematic. Theorem 2.11.17 (identified as problematic) looked a bit similar to Theorem A, but staring at it I realized it doesn’t imply Theorem A and therefore cannot lie on the path towards Theorem A 🙂