I crossed an interesting threshold yesterday, which I think many other mathematicians have been crossing recently as well. In the middle of trying to prove a result, I identified a statement that looked true and that would, if true, be useful to me. 1/3
Instead of trying to prove it, I asked GPT5 about it, and in about 20 seconds received a proof. The proof relied on a lemma that I had not heard of (the statement was a bit outside my main areas), so although I am confident I'd have got there in the end, 2/3
the time it would have taken me would probably have been of order of magnitude an hour (an estimate that comes with quite wide error bars). So it looks as though we have entered the brief but enjoyable era where our research is greatly sped up by AI but AI still needs us. 3/3
PS In case anyone's worried that it used a lemma I hadn't heard of, I checked that the lemma was not a hallucination.
@wtgowers You are experiencing cognitive mechanical advantage. The shovel gave a digger mechanical advantage over the output of his own hands alone. The abacus and slide rule gave mathematicians mechanical advantage over their imaginations alone. Steam shovel <--> LLM The operator never
@wtgowers I have noticed that after such an experience at some point I got jealous. But later you most often realize the result was within sight. It's like a model is a kind of Ain Eingarp mirror from Harry Potter.
@wtgowers how do you feel the evolution of the models when it comes to actually doing the math? are they performing well not just in retrieving related theory, but in executing the calculations themselves? for daily use they’re already good enough (even if the token-based architecture
@wtgowers Matches my experience as well. Another good help is using it to code up quick experiments, which has several times saved me going down theoretical rabbit holes when something I suspect was true was shown to be obviously false.
@wtgowers interesting
@wtgowers This will greatly help experts getting things done
@wtgowers @matthew_pines People under appreciate that AI can be used to disprove things without spending hours or even decades on a subject matter.
@wtgowers This still sounds similar to coding where you can break something down to a simple enough chunk but getting that simple enough chunk is a cognitive task and it save you time, AI can shine. 🤔
@wtgowers I'm looking forward to a maths engine in the spirit of a chess engine
@wtgowers Very interesting.
@wtgowers Civilization speed up. https://x.com/wtgowers/status/...
i hate SF Halloween. like what do you mean you’re Miss Anthropic
Imagine losing first authorship because you got hit by a blue shell on the last lap 💀
when i've observed the greats operating at their absolute best they resemble cracked out starcraft players to me. at the top of their game they embody action alone and forget causes, consequence, circumstance. this looks psychopathic from the outside: how does he not crack under
I firmly believe we are at a watershed moment in the history of mathematics. In the coming years, using LLMs for math research will become mainstream, and so will Lean formalization, made easier by LLMs. (1/4)