Join the discussion
Write your take first — we'll ask for email only when you're ready to publish.
- Hacker News
- A lot of this math is beyond my comprehension, but it often seems to talk of proofs of theorems. What I want to know is if we continue on this accelerated AI mathematics trajectory, will we eventually be discovering new forms of math that will in turn have some applications down the line in engineering or biomedicine etc? I guess what I’m asking is are we on the cusp of a huge breakthrough for humanity, or largely just proving what was already known?
- Most of maths is remarkably abstract and impractical, but sometimes real-world scenarios turn out to be related to some obscure branch of math. Internet security is based on elliptic curves in finite fields, and why would you ever study that if it wasn't powering internet security? Well some people did study it before, for no good reason, and that's how we knew about it.by inigyou
- You can personally work out how apply this one in engineering today!
If you have a spare hour or two, I'd encourage you to have a go at learning (however you learn best - I like just asking smarter people or robots stupid questions) what the maths means and why it's important.
And then once you feel like you have a vague grip on the principles, think about a problem in a domain you know a lot about. Try to see if the maths - and how it's changed our perception - could be used as a tool to solve that problem, or if the solution is analogous to a solution you could try in your own domain of expertise.
LLMs are good at speeding up, I think, the journey an idea has to take between "theoretical academic stuff for academics" and "a usable idea for regular people", because they increasingly allow you to ask an infinite number of stupid questions and give you (hopefully) reasonably good responses.
I've had loads of fun doing this today - specifically seeing if the idea this counter (from what I understand: a many-to-one conversion that kind of does and kind of does not preserve meaning) can tell me anything about the relationship between language and meaning.
I'm sure everything I've done today while mucking around has been the equivalent of a monkey with a typewriter (and Codex), but I think the huge breakthrough(s) you ask whether we're on the cusp of are relatively dependent on how many monkeys are throwing typewriters at problems they know a little bit about, after learning a bit about new ideas like this one. Historically, that's a really good way for broad cultural innovation to happen - distributed information applied across multiple domains by experts in them.
- Engineering and biomedicine, probably in the long term (if at all). But accelerated development of new mathematical methods has a possibility of proving to be relevant for fundamental physics research.
Occasionally large improvements in our models of the universe have been associated with the development of mathematical tools that allow those models to be expressed and/or tested.
by hgoel - > will we eventually be discovering new forms of math that will in turn have some applications down the line in engineering or biomedicine etc?
If we do it probably won’t be for a long while. We’re barely using math from a couple hundred years ago for most applied usage.
by koolba - It’s possible. Compressed sensing is one example of what I suppose you could call a new form of math with applications in biomedicine. It can be used to significantly shorten the time required to obtain a MRI scan, which can improve the patient experience and enable more patients to access MRIs.
- How do mathematicians view counter examples? Is it like an unexpected result in the physical sciences: annoying in the moment but potentially stupendously important as it reveals some inaccuracy in the current models? Or is it more like a bug report in coding… probably just, another little annoying detail?by bee_rider
- I am sure finding holes in existing proofs is what counts as "another little annoying detail". Some people are probably relieved when they have failed to prove a hypothesis and someone finds a counterexample.by mDyJzDPmBdG
- There are pedagogical books (CF. 'Counterexamples in Topology', 'Counterexamples in Analysis') that teach the nuances of subjects through counterexamples. They're popular as it's sometimes easier to learn details from a pathology or degenerate example than from just learning what is intended.by unprovable
- Counterexamples are clarifying. For everyone condition in a proof, it's really handy to have a maximally simple, memorable counterexample that makes it fail because it violates that condition. Mathematicians tend to walk around with a bestiary of counterexamples in their heads. It also makes it really easy to recover a theorem because you try to sketch out the statement, and the spiky, memorable counterexamples jump out of your memory and you add conditions to constrain the domain away from them.by madhadron
- If the poster's (is it Kevin Buzzard?) suggestion works out and AI finds a counterexample to the Hodge conjecture, that would be a really big deal. It's one of the Millenium problems, for example.
One thing that he mentions that already quite surprising is that AI was able to autoformalize the Golod-Shaferevich theorem and proof.
by QuesnayJr - I think he was being provocative and maybe a bit tongue-in-cheek when he said that. A candidate object alone doesn't resolve the Hodge Conjecture. Any apparent counterexample would have to prove that no algebraic cycle exists, no invariant subspace exists, or that every element of an infinite ideal is nilpotent. Much harder, but not impossible.by OG_BME
- It is Kevin Buzzard. It's kinda small font on my phone but if you look at the "about xena" link it says it's his site.by mcshicks
- mathematicians have been using computers for well over half a century, but this was after "bounding" the problem first and then running through the cases with a computer. Now AI is doing the first part. However, mathematicians are still needed at crafting prompts, and knowing where to look, still. The prompt for the Jacobian conjecture was obviously not random. the search space is too big to just try all the combinations of 3 variable polynomials.by paulpauper
- I don't think there was a 'prompt' for it, rather a long and dedicated work of a professional mathematician which involved LLM in some capacity. I'm sure the search step wasn't an ad-hoc script running in a Claude Code session (as somebody would naively assume), it was an optimized numerical code running in Anthropic's compute cluster. Note that details are not published yet and `__alpoge__` is officially working at Anthropic.by sesm
- This is the best take. Computers don't care about this stuff. A computer could make a movie, but only a human can appreciate it.
We're a good team, and that's ok.
by hobonation - > The prompt for the Jacobian conjecture was obviously not random. the search space is too big to just try all the combinations of 3 variable polynomials.
Maybe the prompt contained a part like this: "the search space is too big to just try all the combinations of 3 variable polynomials, so be clever about it". Or maybe this part was omitted from the prompt, because modern LLMs are smart enough to figure this out without us having to mention it.
by skinner_ - Okay, I'm not sure about the original one, but here is the prompt of a successful reproduction:
https://aaronlou.com/jacobian_counterexample_prompt.pdf
Obviously it is not random, but it's very generic. No mention of search space or how to reduce it.
by skinner_ - I wish I had LLM-built Lean formalisations in university, so much of the math in the slides had errors, and some professors are very bad and ungracious admitting it, while simultaneously rejecting requests for clarifications by saying "the proof is in the slides".
Of course Lean proofs are rarely a good way to understand proofs, but hopefully they can be used to generate more human understandable arguments.
by angry_octet - Yes, or to settle dispute and remove doubt once and for all, i.e. the Leibniz way.by learningstud
- > Of course Lean proofs are rarely a good way to understand proofs, but hopefully they can be used to generate more human understandable arguments.
I would object to the first part: Of course there is a nontrivial learning curve, but then I'd argue that non-slop Lean/Agda/Rocq/... formalizations are amazing for understanding proofs. A good formalization presents the outline and the key arguments in nicely structured form, and then, unlike pen-and-paper proofs, also allow you to get the details on every single step, exactly to your desired level of depth.
The proofs in Martín Escardó's TypeTopology Agda repository come immediately to my mind as an example. [An interactive Agda tutorial is here: lets-play-agda.quasicoherent.io]
In contrast, LLM-generated formalizations can currently be extremely messy. They certify truth and can also contain interesting arguments, but substantial work is required to bring them into a shape that contributes to the actual goal of improving our understanding of the mathematical landscape.
- BTW, counterexamples in mathematics are really important and often help to refine definitions and sharpen proofs.
1) I recommend the wonderful 1976 book Proofs and Refutations by Imre Lakatos.
2) There is a considerable list of books dedicated to counterexamples, e.g. in topology, probability, analysis, etc.
by FabHK - I suppose it will fall to AI as well to compose the mathematical equivalent of The Ballad of John Henry. Who will be the human champion, the last great hero who can deliver proofs "from the book" that a machine cannot outperform?by dzdt
- It's probably not quite that dramatic yet, though it seems possible it will get there, maybe even soon.
There's no structural reason to expect acceleration any more or less than an asymptotic behavior (if even that, acceleration is probably the bigger ask). Different problems yield to a new solvent, maybe that's also more, but it could go either way and we definitionally don't know yet because we don't understand the convexity of AI capability, we cannot directly access it interiority, we don't know if it's sandbagging (other than that it does sometimes, it can). It's an emergent phenomemon that might actively resist measurement. Or it might be as predictable as a clock in a few years.
No one knows, or if they do, they aren't talking. The loud people don't know anything.
- "Gonna Die With My Hand-Written Proof in My Brain" - Recorded in 2027 and compiled in the Anthology of American Folk Mathematics (2052)by lioeters
- This is an unhealthy view of mathematics. It's mathematics as envisioned by football fans.
The most valuable things in mathematics are not beautiful proofs. We need more useful definitions. Actually coming up with useful definitions (and building good conjectures out of them - not even theorems, conjectures) is something LLMs have not yet tried to conquer.
by Diogenesian - > A few days earlier I had got an email from a professor in the maths department here at Imperial, expressing surprise that some of our graduate students were paying $200 per month to access models such as Sol and Fable. He said that he thought that these people were crazy. I did not immediately respond. But after meeting with Andrew I emailed the professor back and told him that in my opinion, any PhD student who was not paying $200 per month to access these tools was crazy. In fact during the workshop I learnt from Harvard PhD student Bryan Wang that Harvard were already giving free Fable access to all PhD students, post-docs and faculty at Harvard.
Yeah, given how much it accelerates grad students to produce meaningful output more quickly, why wouldn’t you make an investment of $2400/student/year. Seems like pennies overall.
by vlovich123 - Many graduate students view themselves as ethical beings, not machines that "produce meaningful output," and everybody here knows (useful) LLMs are indefensibly evil because of stolen training data and enormous environmental impact.by Diogenesian
- The living-costs stipend for an EPSRC PhD student is around £20k so it's about ten percent of that... big commitment for a student to make!by adw
- Human mathematicians have been being out-counterexampled for at least two decades. The main difference, as I understand, is that (A) we now have a lot more compute to throw at such things, and (B) it is currently trendy to do so. But the sizes of counterexample we're seeing are around about what I'd expect pre-generative-AI counterexample search systems to be able to find.
It's not easy to find a counterexample to the Jacobian conjecture, by any means – by which I mean to say that naïve brute-force search will take too long – but the scope of existing searches listed on Wikipedia[0] suggest that many tricks are already known, and that people just hadn't looked, systematically, for a counterexample in three variables before. Wikipedia writes:
> Tzuong-Tsieng Moh checked the conjecture for polynomials of degree at most 100 in two variables.[17][18]
where reference 17 is from 1983, and reference 18 is a preprint with no given date. Knowing very little about this problem, my impulse is to side with the unnamed faculty member cited in the article:
> [who] said to me that the fact that the counterexample was so easy to find just indicated that humans had not spent enough time thinking about the problem,
For context, the auto-generated counterexample is in three variables, has degree 7, and was discovered in 2026.
by wizzwizz4