Yeah. In math at least it's clear that you don't know what's going on. In other fields, it's very easy to think you understand without knowing how much you're missing.
Glad to see that Cython got a shout out here. It's not that widely used, but it's a lovely experience. It uses the CPython ABI to drastically reduce the friction of switching between C & Python.
A crucial caveat: basic research investment runs on the same logic as venture capital investment. We know that most mathematical efforts will be worthless. Our experience has lead us to expect that a very small number of such efforts -- some of them very far removed from applications -- will have payoffs so large that they change the shape of our society.
_We do not know in advance which efforts are going to pay off_. Abstract efforts in topology put us on the road to nuclear energy. Silly number puzzles enabled internet commerce. Non-euclidean geometry gave us synchronized universal GPS.
We should not let our inability to conceive of applications of weird abstract stuff prevent us from making these investments. If our ancestors had fallen in to that trap, we'd be far poorer as a society.
What we can do is ask that people trying new stuff attempt to fail quickly. And that's basically where we are with academia today. Most people who do mathematical work will not have a career in math. They try something new, work for a little while on it, and go do something else when the results turn out to be of modest interest. This leaves behind a messy undigested literature, which is unfortunate. But maybe AI can help us sift that for treasures we missed.
The problem with prediction markets is fundamentally that they're unregulated.
Modern equities and futures markets are highly evolved and rather carefully regulated systems. We've spent centuries learning what the failure modes are and how to guard against them. It's never perfect, it's never going to be perfect -- it's fundamentally a voting system -- but in general, we get liquidity and price discovery at a relatively low cost, while avoiding fraudulent and evil behavior like wash trading and criminal profit laundering.
These new "prediction markets" have been put in place without any of those hard-earned protections. And surprise, they're rife with dirty trick and dirty money.
ITPs are far older than LLMs in general, sure, but that's a pedantic distraction. What everyone is talking about here (both the comments, and the article) are ITPs enriched with LLMs to make the "smart" proof assistants. The LLMs used in ITPs are not vastly different from the usual chatbots and coding assistants. Just a different reinforcement learning problem, no fundamental change in their architecture.
Exactly this. LLMs really aren't built for discovering new mathematics, especially _interesting_ new mathematics. They're built to try the most obvious patterns. When that works, it's pretty much by definition not interesting.
What LLMs are good at is organizing concepts, filling in detail, and remembering to check corner cases. So their use should help mathematicians to get a better handle on what's terra firma and what's still exploration. Which is great. Proof by it-convinced-other-mathematicians doesn't have a flawless track record. Sometimes major theorems turn out to be wrong or wrong-as-stated. Sometimes they're right, but there's never been a complete or completely correct proof in the literature. The latter case is actually quite common, and formal proof is just what's needed.
There's always some risk of confusing the model with the reality, but yeah, if you have chiral fermions interacting through gauge fields and gravity, the charges have to say satisfy all of the anomaly cancellation conditions (there's about half a dozen) or the model will be inconsistent.
There does appear to be a deeper reason, but it's really not well understood.
Consistent quantum field theories involving chiral fermions (such as the Standard Model) are relatively rare: the charges have to satisfy a set of polynomial relationships with the inspiring name "gauge anomaly cancellation conditions". If these conditions aren't satisfied, the mathematical model will fail pretty spectacularly. It won't be unitary, can't couple consistently to gravity, won't allow high and low energy behavior to decouple,..
For the Standard Model, the anomaly cancellation conditions imply that the sum of electric charges within a generation must vanish, which they do:
3 colors of quark * ( up charge 2/3 - down charge 1/3) + electron charge -1 + neutrino charge 0 = 0.
So, there's something quite special about the charge assignments in the Standard Model. They're nowhere near as arbitrary as they could be a priori.
Historically, this has been taken as a hint that the standard model should come from a simpler "grand unified" model. Particle accelerators and cosmology hace turned up at best circumstantial evidence for these so far. To me, it's one of the great mysteries.
No wonder Gatsby is frequently misunderstood: Most people won't have the experience needed to understand it until they're in their 30s, but we prescribe it for high schoolers year after year.
There is a good ending to Game of Thrones: evil wins, everyone dies. All the fools who pursued their own interests rather than face an annihilating threat get annihilated. It's right there in the show's motto. "Winter is coming."
The writers just lacked the courage to do it. They tried to tack a Disney ending onto a tragedy.
A lot of the time, the definitions peculiar to a subfield of science _don't_ require much or any additional technical background to understand. They're just abbreviations for special cases that frequently occur in the subfield.
Looking this sort of thing up on the fly in lecture is a great use for LLMs. You'll lose track of the lecture if you go off to find the definition in a reference text. And you can check your understanding against the material discussed in the lecture.
I think at this stage, most mathematicians recognize that formal proof verification is a real and interesting thing. We have extremely prominent mathematicians like Scholze & Tao making a point of using these tools.
But in many cases, it's extra effort for not much reward. The patterns which most mathemematicians are interested in are (generally) independent of the particular foundations used to realize them. Whether one invests the effort into formal verification depends on how hard the argument is and how crucial the theorem.