https://github.com/openai/math
Looks like many a promising PhD thesis may now been reduced to an AI slop prompt đź‘€
Grok bot summary:
The GitHub (openai/math) drops 722 manuscripts across 372 families spanning number theory, geometry, algebra, physics and more, with many Lean formalizations.
Standouts: new zero-free region for the Riemann zeta function (Re(s)>11/12), Hodge conjecture proof for CM abelian varieties, improved irrationality exponent of π, Mahler conjectures progress, Kaplansky direct-finiteness in char 2, free group factor isomorphism, quasipolynomial AP bounds, and results on Vlasov–Maxwell, spin glasses and more.
Most used ~3 hours of ChatGPT Pro-scale compute each.
I know a lot of people are dunking on Terrence Tao and others (put the fries in the bag) but I find this kind of sad. They're likely going to keep producing results at a rate that will be impossible to for human reviewers to even keep up with.
This one really feels sad to me. If results go dey drop like this every hour, reviewers no go ever catch up.
Proofs are formalized in Lean. Reviews can be done automatically.
Nope. It's not that simple. You can generate 'compiling' proof in lean that is still incorrect.
Don't really understand why the AI-bros are dunking so much on Terrence. He's been embracing LLMs since the beginning, even though he didn't anticipate how quickly the progress would be, and even now, he seems to be constructively trying to find ways to adjust to the new reality. He's far from a Luddite.
ai bros are dunking on terry tao?
They[1]'ve been circulating clips of him without context misrepresenting his stance.
Twitter, mostly. Maybe not a representative sample. ↩
I have some thoughts on this I'll share soon. But it comes down a bit to, "do you do it because of what you can get out of it, or do you do it because you love it?"
We may all have to ask ourselves this question now because of AI.
Many midlevel engineers enjoyed just writing mid code. they knew they weren't john carmack but it gave them purpose, they dedicated their life to being mid at it, and it put food on the table for their family. Setting up a new project scaffolding, environment variables etc. Same for graphic designers and now mathematicians. It's understandably hard to cope with your life's work needing to be repurposed so quickly.
Saw a youtube about these chinese drama shorts companies and their actors and directors are also similarly having to cope with so many shops pivoting to AI. It's sad.
Noted