On one particular Friday afternoon, he stated a conjecture that he hoped was true, and invited us to try to help him prove or disprove it. It was the sort of thing that he really wanted to be true; he liked things smooth and beautiful. I, on the other hand, hoped it was false as I like the weird and exceptional in mathematics. It was also the case that I had absolutely no command of the sort of machinery that one would use to prove such a thing, but I could certainly look for a counterexample.
I learned on Monday that he had spent the entire weekend trying and failing to prove it. I, on the other hand, had put all my energy into finding a counterexample and had one within an hour.
My single (quite small) contribution to mathematical research was a counterexample because it was all I could do. The story does illustrate that it can be helpful to have people with different tools, hopes, and motivations working on a problem, though. I was not, and will never be, even a shadow of that great mathematiciam I studied under, but on that occasion, I had reason to look in a different direction than he did.
Hm, as a mathematician, my experience feels opposite. A proof would be an adaptation of a proof I know, some tweaking it here and there. A counterexample would require some deep understanding of the structure of the objects involved, which frequently is beyond my comprehension.
But probably this is because I think of quite abstract objects which are harder to grasp. For numbers or polynomials, this would be the other way round.
The conjecture had to do with whether one convex polygon could be continuously deformed into another while remaining convex, under certain conditions and constraints. The answer turns out to be no, but surprise and disappointment are understandable reactions to that outcome. It was indeed much more practical for a young grad student to look for a clever misbehaving polygon than to try to prove something about all of them at once.
This kind of professor/researcher/teacher needs more praise. One of the first engineering courses I took when I started out in higher education was taught by such a person.
Maybe it's just me, but I never felt so welcomed and included during my time in higher education as when that lecturer told a bunch of first-year students "here are some things we haven't figured out which you can help with, let me know if you come up with something". It was inspiring and a great introduction to what's otherwise a rather dull first couple of years of academia.
It's because counterexamples are easy compared to proofs which require new mathematics.
GenAI is great at combining existing things in new ways (interpolation). It's terrible at creating new things from scratch (extrapolation).
For a more extreme (although somewhat inverted) version of this, see Zeeman. He spent years trying to find a knotted sphere in a 5D space. Then realised this was impossible and got a proof for it in a few hours. [1]
[1] https://ima.org.uk/28009/sir-erik-christopher-zeeman-the-mat...
[dead]
He spent an entire weekend before having the wisdom to pause, and let someone else contribute their time to finding a counter.
Interestingly, Yitang Zhang of the twin-prime-conjecture fame spent 7 years working on the Jacobian conjecture under the advisor Tzuong-Tsieng Moh at Purdue. A key step in his thesis used a corollary of Moh's. It turned out that the corollary was incorrect. As a result, Moh refused to write any recommendation letter for Zhang, and Zhang couldn't find any teaching or research job and ended up spending years working at a Subway[1].
Imagine Zhag had ChatGPT in 1986 when he started working on the Jacobian Conjecture.
[1] Of course now this has become an inspiring story. That said, the story definitely invokes complex emotions. The best way to describe it is probably this Chinese poem, which I have no idea how to translate: 庾信平生最萧瑟，暮年诗赋动江关
and for now as long humans are going to judge of what counts as an elegant or illuminating proof, there's going to be work for human mathematicians
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.
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.
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.
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.
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.
One thing that he mentions that already quite surprising is that AI was able to autoformalize the Golod-Shaferevich theorem and proof.
It seems to me also that the very vocal anti-LLM crowd are in the denial phase of grief.
At least initially, chess computers were better than humans not because they were more creative or inspired, but because they thought harder/deeper. That's exactly the sort of "find counterexamples to this if they exist" work that we're seeing here.
Eventually computer chess got to the point where humans look at some moves and say, "That's an amazing, inspired move. That's not a 'bot' move at all, I can learn from this." We're just not there yet with AI/math in general.
A week or two ago I asked Claude Code to write a comprehensive testing plan for a new Postgres feature I wrote, UPDATE/DELETE FOR PORTION OF. I was a bit anxious about how many bugs were discovered as soon as it was merged this spring. Claude found some untested areas, then it wrote more tests for them. I'm not talking about LOC covered, but feature combinations. (I've been meaning to submit this as a followup patch. . . .) Fortunately it didn't find any more bugs.
I sense that testing plan has affinity with the findings in the OP, even though it is far more humble than research mathematics. Even better would be if we knew good ways to express invariants about Postgres's behavior, and then we could ask LLMs to violate them. I'm sure there are good ways already, and the "we" who is not knowing is not "all humans" but "the Postgres team" or just "me".
As a counterexample to the article (heh): even though Claude didn't uncover any new bugs, a human did, just a few days ago. Alas!
[deleted]
[deleted]
Maybe in the future the work of Mathematicians will be like the ones of SWEs with AI, check thousands of lines of AI generated proof and find the subtle errors
That point had come some time ago. Nowadays the literature is both enormous and littered with false proofs and an unknown, but nonzero, number of false published results.
Plus, as a non-expert, you will naturally want to understand more about what you are proving together with the expert. LLMs can help there, too, by carving a path from elementary mathematics to the research problem more efficiently and in a more targeted manner than a generic exposition or survey.
That could give birth to a beautiful research-exposition pair that can benefit both academics and interested laypeople, who have (rightfully, but inevitably) felt excluded from the insights of high level research. I have long hoped for something like that. There, however, the academic must watch the LLM like a hawk, because expository interpretation of results is prime ground for hallucinations, and adversarial agents will not have much effect in improving it.
To be clear, I do like 'outcounterexampled' a lot!
Long story short this is much less impressive than it was sold to be. Basically they had mathematicians combing through long winding chains of thought (incidentally: you wouldn't have access to that reasoning) and cleaning it up and making it coherent. That doesn't mean its unimportant, but we're being gaslit about the amount of human steering and human effort that went into this.
A plea: please stop upvoting hype that comes from these labs. It takes time to evaluate their claims and they're always less impressive than claimed.
[dead]
But also, for this conjecture to be wrong is quite surprising to me. Intuitively I would think any convex polygon to be topologically equivalent to a circle, and any convex n-gon should be deformable into its regular version, then back to the other one…
---
Here's the full puzzle, as best I remember it:
Suppose you have two convex polygons with the following very specific relationship: one has been created from the other by making one side stretchy, moving an adjacent side on a hinge, and keeping the remaining sides fixed. For example, imagine a square with a top side made of rubber, and a rigid right side hinged at the lower right corner. You can make a series of convex polygons in a continuous fashion by rotating that right side on its hinge.
The question is, if you have two convex polygons that differ only by this one stretchy side and this adjacent hinged side, can you guarantee that you can always smoothly deform the one into the other by this hinging method while keeping the whole thing convex?
That is to say, if you are deforming one polygon into another by this hinge and rubber band method, if your starting polygon and ending polygon are both convex, are all the middle ploygons guaranteed to be?
The answer is intuitively obviously yes, but in point of fact, it is no.
---
To bring this back to the original story, the question was a small step in a larger constructive proof he was working on. The overall result was already known - in fact, we had just discussed it in class - but the proof had this distressingly jerky, discrete movement to it, and he was hoping to construct a more pleasing and smooth algorithm as a more satisfying proof.
As for me, I would not have known how to begin to prove even the smaller question... but I sure could doodle a counterexample. ;) I therefore looked for a one with all the gusto of a young grad student hoping against all odds to do something helpful. You may look with all the confidence of knowing there is something to find, which is also a tremendous help.
I only know his side of the story because he started Monday's class with this line: "I spent the entire weekend trying to prove the result, without success, and it was a good thing too, as there was a counterexample in my box this morning." He did seem genuinely frustrated, but I also wouldn't have put it past him to have exaggerated that part for the laugh.
Anyway. Asking an AI to find counterexamples under such circumstances seems to me similarly reasonable to asking grad students. In my engineering work, I find there is a balance between using the AI to improve and augment your work (especially to call on the diverse perspectives in its training set), and using the AI to avoid your work. I do think the best experience and results are found in that balance. I would expect the same to be true in mathematics.
> During his study in 1939, Dantzig solved two unsolved problems in statistics due to a misunderstanding. Near the beginning of a class, Professor Neyman wrote two problems on the blackboard. Dantzig arrived late and assumed that they were a homework assignment. According to Dantzig, they "seemed to be a little harder than usual", but a few days later he handed in completed solutions for both problems, still believing that they were an assignment that was overdue.[4][6] Six weeks later, an excited Neyman eagerly told him that the problems he had solved were two of the most famous unsolved problems in statistics.[2][4] He had prepared one of Dantzig's solutions for publication in a mathematical journal.[7] This story spread and was used as a motivational lesson demonstrating the power of positive thinking. Over time, some facts were altered, but the basic story persisted in the form of an urban legend and as an introductory scene in the 1997 film Good Will Hunting.[6]
I think you believe a fallacy about how human cognition works if you think we actually do something different than interpolation
Ugliness is in the eye of the beholder. Lots of counterexamples are very beautiful. For example, the Dirichlet function (f(x) = 1 if x is rational, 0 otherwise) is a source of very beautiful counterexamples. Eg it is discontinuous everywhere but f restricted to only rational numbers is continuous on all rationals and likewise f restricted to irrationals is continuous on the set of irrationals (R-Q).
[1] The Conway knot has 11 crossings yet shares the same Alexander polynomial as the “unknot” which has no crossings at all. It took 50 years to decide the question of whether it has a basic property known as “sliceness” https://en.wikipedia.org/wiki/Conway_knot
[2] Conway’s base 13 function Was invented as a counterexample to the converse of the intermediate value theorem. That is, it satisfies the intermediate value property while being everywhere discontinuous (which breaks my brain completely) https://digitalresearch.bsu.edu/mathexchange/wp-content/uplo...
Even if an LLM starts by pursuing things that follow human bias, continuous failures and re-prompting to try something different will eventually force it to consider things outside of what ever biases it has.
You can do the same thing to a human. But most people would consider it unethical to lock someone in a box and force them to keep trying to solve the same problem over and over again until they figure it out.
Is a 'bias' in a piece of writing generally a property of word to word choice and sentence to sentence construction or is it something more nebulous? Especially in terms of the appreciation of mathematics and someone's hesitance about publishing a mathematical argument they think is ugly or brute forced in some way.
You might be fascinated when you read the story of Golden Gate Claude: https://www.anthropic.com/news/golden-gate-claude
Why do you think it's called Alpha ZERO?
Ahem.
> On one particular Friday afternoon, he stated a conjecture that he hoped was true, and invited us to try to help him prove or disprove it.
It was a parallel effort ... we don't know how many people were working on it that weekend. And since the professor wanted it to be true and presumably believed that it was true, why the heck should he wait for students of unknown number and ability to find a counterexample that he didn't think existed?
What actually happened was the professor posed the question in class as an open research question, which he regularly did, with no particular expectation that any students would work on it or make meaningful progress. My wife happened to sit down in her office and come up with a counterexample, which she wrote on paper and left in the professor's physical mailbox on campus fairly late in the evening. He had almost certainly already left campus for the weekend by that time. This wasn't a case of some sort of arrogance or lack of wisdom, just a case of non-instantaneous asynchronous analog communication methods.
This particular professor was extremely good at letting others contribute. As soon as the contribution actually reached him, he assessed it and used it.
A PhD student discovered that a result of his professor would imply the solution to a big conjecture in another field. The people in that field then analyzed the prof's result and found that the proof was flawed. The student was still allowed to graduate based on this since the finding of the connection between fields was brilliant. Then he quit academia (not because of this story, he had planned it before). Then a year later the prof figured out how to fix the flaw in his proof and published a paper with his former student, thus solving the conjecture. The two are still on good terms, writing papers together.
Why are you framing this like this? Do mathematician take these kind of things personally?
Sometimes, of course, the proof is just wrong. That is the dangerous case, which will cause either major corrections or failure.
The professor was John Milnor.
Naomi Wolf 'death recorded' on BBC[1], skip to 5:51. After this the book was pulped and she had some sort of psychotic break during COVID and allied with ultra-right and COVID denialist loonies.
I'm tired of tales like this in academics though. That's not a criticism of you for telling the tale, I'm just so tired of this kind of thing in academics in general. So, so, so much politics and public reputation management. Zhang should have never had to suffer like that.
As my own research has drifted more into math, I've been surprised at how many assertions in the literature turn out to be false. Not just false, but propagated into the applied literature extensively, and even when you point out the problems a lot of defensiveness and denial about it along the lines of Zhang's story.
I agree about wondering what would have happened if LLMs had been around in 1986. My guess is the outcome would have been the same for the same reasons?
My experience with LLMs in proofs is they can be very helpful, but also very wrong. It's like having another person with another set of hunches about what path to go down.
Very true. Unfortunately, when there are people, there will be politics. I remember when reading Yau's autobiography, I kept marvel how much calculation, or "politics" if you will, that Yau mentioned or implied in the book.
> My guess is the outcome would have been the same for the same reasons?
At least Zhang didn't have to spend 7 years working on the Jacobian conjecture. He said in an interview that he always wanted to work on number theory. Moh asked him to work on Jacobian, and he obliged.
In his exact words: "A new scientific truth does not triumph by convincing its opponents and making them see the light, but rather because its opponents eventually die and a new generation grows up that is familiar with it... An important scientific innovation rarely makes its way by gradually winning over and converting its opponents: it rarely happens that Saul becomes Paul. What does happen is that its opponents gradually die out, and that the growing generation is familiarized with the ideas from the beginning: another instance of the fact that the future lies with the youth."
And he said that having lived, as a outsized figure, through the late 19th to mid 20th century of physics, which was the absolute golden age for such.
Yu Xin’s was a life of utter desolation; in old age, his poems and rhapsodies stirred the riverlands.
No life ran more bleak and desolate than Yu Xin's —
yet in his twilight years, his verses stirred the rivers and the passes.
Yu Xin's past was exquisitely tragic
Ages passed; now his works betray magicAlso, 'brute-force' style attacks where one simply feeds the input into the computer and it yields a solution are nothing new and certainly predate LLMs: https://en.wikipedia.org/wiki/Euler%27s_sum_of_powers_conjec...
Hell, one could even go further into the past and refer to the thankless work of pre-computer era mathematicians who sweated over manual calculations in order to disprove various prime related conjectures: https://en.wikipedia.org/wiki/Mersenne_conjectures
You seem to have an objection to non-intutionist mathematics in general, a position that was once held by many an illustrious mathematician but is relatively fringe in the contemporary academic community. Mathematical facts don't have to be intellectually satisfying or make sense to you, the human, rather it is up to you to wrap your mind around discovered mathematical facts.
[Dis]proof by counterexample is the most straightforward way to show a statement to be false. What better way is there to disprove a general statement like 'all x are y' than finding an 'x' that isn't 'y'?
Unless you want to spend time "proving" that 2 * 2 = 1.
Considering ChatGPT was released only three and half years ago, and LLMs could do high school math only less than two years ago, I think this "for now" will not last very long.
Or are they approaching an asymptotic limit?
Couldn't people in principle continue to study a problem that's only been shown to break at one point? Prove something adjacent, or slightly weaker, or elaborate the counter example into a powerful explanatory framework?
But mathematics is not a collection of facts. Mathematics is the study of abstraction. And what do you learn from a single data point? What can you abstract from that?
That's why just being a counterexample isn't really interesting. There has to be more than "counterexample" for there to be something to abstract. Was it generated from an analysis of the problem? Can the counterexample be generalized to explore the problem further? Is the counterexample a surprise in a way that suggests something is missing from current understanding?
Being a counterexample doesn't mean that something isn't interesting to a mathematician. But it's also not the interesting part.
P.S. It helps that in CS lots of theorems are about either inductive or coinductive definitions.
The difference today (and the reason why everyone is excited about it) is that the same system that does advanced math can write poetry, play an above average game of chess, code frontend/backend stuff and do cybersec. These are not "expert systems", nor are they trained for each task individually. That's the catch.
> just indicated that humans had not spent enough time thinking about the problem
Heh, this is a weak excuse. We've seen variations on this theme every time something cool gets solved by the models.
They are explicitly trained for each task individually.
EDIT: just re-read your comment. I don't think you have a good understanding here, no offence.
I think the misunderstanding comes from "individually". You are thinking about diverse datasets, but that's not what individually means in this context. In ML individually trained means that for each task you prepare an architecture, dataset and eval and train that model on that data. And each model has its own objective that you train for. In LMs the objective is singular, for every data point - next token prediction. And, importantly, you train on every datapoint, the more diverse the better, but not independently. The cool thing is that training on diverse datasets improves scores on other downstream tasks, while the training objective is the same.
So you can have a training run on common crawl + programming that improves scores on logic puzzles, or common crawl + novels that improves scores on planning tasks. But the important thing is that it's all trained together, not independently.
AI is only as good as a human mathemetician, which we don't have enough of? "just"?
https://en.wikipedia.org/wiki/Jacobian_conjecture
> The conjecture was first stated for two variables by Ludwig Kraus in 1884 [...] an example of a difficult question in algebraic geometry that can be understood using little beyond a knowledge of calculus.
> The Jacobian conjecture is number 16 in Stephen Smale's 1998 list of Mathematical Problems for the Next Century. It was notorious for the large number of published and unpublished false proofs that turned out to contain subtle errors.
If I were a student living on a measly $1600/month I would be livid if the school gave me a $200 raise in AI credits, instead of money to buy groceries or pay rent.
And while agency in finances is important, if this helps you finish your schooling faster, I suspect you might not care how you get access to a frontier AI model and having 10% of a theoretical $1800/mo carved out isn’t a huge deal.
What level of copyright violation will send us to hell?
Likewise with trying to make me judge an objective threshold for pollution. It really should be that any polluter needs to morally justify their actions. I find "mostly illusory productivity improvements in white-collar employment" to be an especially indefensible reason for firing up new natural gas generators. Let alone the real motivation being "billionaires want more money." The level of pollution from training and deploying generative AI is simply evil.
And your last question is just pure cynicism. The real sin you're committing here is contemptuously dismissing ethical concerns out of hand.
I assume you use LLMs. I don't. It truly seems like using LLMs makes people stupider and more unethical. Some cognitive work should not be outsourced, especially not to a mindless stochastic parrot.
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.
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.
We're a good team, and that's ok.
All we're able to do is apply flawed analogies, generic information theoretical models, trial and error, post-hoc rationalizations and benchmarks without really understanding why.
[dead]
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.
We really need to stop thinking about LLM training data as the knowledgebase they build from and instead consider it more the skillset they start with.
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.
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.
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.
> ..Even more unexpected is the fact that many expositions of this topic commit serious mathematical and logical errors. Moreover, this happened not once or twice, but many times over the centuries, and continues to this day in many printed and electronic publications; the most recent case is in the second issue for 2008 of this journal. I will justify this harsh statement soon, after setting up the necessary background.
Also https://1000-plus.github.io and https://us.metamath.org
(That's not to say there's no value to making the proof themselves nicer--compilation time and reusability can actually be a really big deal in formalized mathematics!--but it's way less important than it is in software).
or that viral AI short example of a vibe-counter: Okay, you start with 1, and then I'll say 2, and then you'll say 3, and we'll continue like that. Great idea. I'll start with 1, and then you'll say 2, and then I'll say 3. That's right, I start with 1, and then you say 2...
Even better:
"so if I tell a *human"..."
then whose achievement is the result?
Apparently thats what you believe if you think "creative" ideas just float into brains somehow.
> Which Anjunabeats and Anjunadeep compilations have the most breakbeat tracks?
GenAI was able to give me breakbeat tracks that were on the Anjuna labels, but it completely flubbed on whether and which those tracks were on compilations. It was very confidently, mostly incorrect.
I think this is somehow isomorphic to the “interpolation vs extrapolation” issue. GenAI is forced to generate an answer, and there’s no mechanism by which we can interrogate the model for its confidence (at least, that’s my understanding).
And yet, I asked “How confident are you in your answer along different dimensions, ie whether those tracks are breakbeat, whether they are Anjuna tracks, or whether they are on those compilations?”
And its answer was surprisingly satisfying, it only gave 30% confidence that the tracks were on the compilations, which is where it flubbed.
Anyway, personal observations, GenAI is meant to be interacted with, not just a single prompt black box.
Even Opus 4.8, GPT 5.5, and Gemini 3.1 Pro (haven't tried 5.6 yet) confidently make up BS sometimes and needed to be reminded to verify thnings instead of inferring or relying on "memory" from training data.
IMO harnesses need some kind of built in "are you sure about that?" loop checkpoint that pauses the main interaction and asks the LLM to evaluate the strength of evidence for a claim it's about to make. It seems almost unreasonable to expect an LLM to next-token-predict its way to such a conclusion, reliably, without prodding. That or we just need another year of RLHF and another 250 billion parameters, IDK.
I feel like that should work becaus when you're using an LLM for a batch inference or classification type of task, it's not that hard to prompt them to emit an "unknown" flag. They just won't do it on their own, and in a coding harness there is so much else going on that a prompted reminder gets lost.
> IMO harnesses need some kind of built in "are you sure about that?" loop checkpoint that pauses the main interaction and asks the LLM to evaluate the strength of evidence for a claim it's about to make.
As a practitioner of ML for the past decade, this is the part of LLMs that has always been least satisfying for me. The shared intuition amongst myself and my colleagues has always been that the strongest models are the ones that produce actionable insights directly. Doing all sorts of data preprocessing gymnastics and then following up inference with a 1000-line wall of if-else business logic has always indicated to me that the model is somehow deficient, and not truly capturing the kernel of “truth” within the data, either because the model choice is wrong (e.g. linear regressor for nonlinear problem), or, more likely in practice, the collected data does not effectively capture the underlying “truth” of the measured phenomena with a sufficient signal-to-noise ratio.
LLMs are powerful and have essentially limitless utility, but there’s something missing at a fundamental architectural level for which harnesses are simply a bandaid. Of course, solving that fundamental architectural issue is probably the key to AGI, so…
It's called Alpha Zero specifically because it was trained from scratch - zero, not on human data.
It's understandably the natural place to get the dramatic tension from what at least purports to be a sober account with some momentum. It's reasonably consistent with the way it's treated on the lectures I've seen from Sir Andrew Wiles on YouTube.
It sounds like a nightmare. He had intentionally set the proof up in a high stakes way, working in private, very quiet on what he was really doing. I gather this is not the done thing, eccentric at best kind of vibes, and I think by that point it was almost crackpot adjacent to even try seriously. His advisor forcefully pushed him off even trying earlier. So it's compound on the stakes. The beg reveal is intentionally as dramatic as possible. And then the questions start to land, most are minor clarifications, notation deficits, but one is sticky, one won't go away.
Kept me up late reading about it.
Probably there are understandable reasons for that... But I think "negative science" is really important, and soft results like "we tried that for a long time and it wasn't very fruitful" are actually very important for progress even if they're poorly attested in the written record. I guess in mathematics they come informally from your thesis advisor...
More generally I think people are inappropriately confident in general. When you go through history just about every century prior people believed many things that the next century would come to see as plainly false. People in modern times seemed to have stopped believing this was true, yet it's likely that people during every given century also stopped believing such was true, because what you believe "now" is always assumed to be correct. Nobody wants to believe they hold false beliefs, even though there's a practically 100% certainty that all of us do, and in quite healthy quantities.
[1] - https://en.wikipedia.org/wiki/Public_school_(United_Kingdom)
Like, I bought the game just before the Nether was added, and I thought that was not a very good feature, but just a few weeks before that, he'd added monster spawners, and just a few weeks before that, he'd added redstone, and a few weeks before that, minecarts, and a few weeks before that, signs, and a few weeks before that, the world wasn't infinite yet. Just another few months back, and the game didn't have an inventory. That guy had the opposite mindset of me and he got shit done.
> After this the book was pulped and she had some sort of psychotic break during COVID and allied with ultra-right and COVID denialist loonies.
That's quite an extreme shift considering she had previously been a leading figure in third-wave feminism and an OWS activist.
This is a real problem if you're one of the people involved in something like OWS who wants to see effective change, not just making a circus about yourself.
[deleted]
Not checking newspaper reports of the period is lazy though and exactly the kind of thing I'd expect a journalist to do and therefore be the one to discover the flaw.
[dead]
Alice is a football stats wiz. Alice is a WR Jones fan because he has an incredible 40-yd dash time and leads the league in YAC.
Bob is a WR Smith fan. Bob knows the stats are all cooked. Bob knows that if the stats weren't cooked, WR Smith would lead the league in all categories. Therefore, Bob doesn't bother with stats.
If you are not yet old, remember this - it is very likely you will old in a few years.
He simply believed on a fundamental level that the universe must be deterministic. Many don't understand that many of his famous quotes like 'spooky action at a distance' or 'god doesn't play dice' were mocking probabilistic interpretations of quantum mechanics, like the Copenhagen Model - the one we still assume to this very day.
Of course there even remains the possibility that at some point in the future he may even be proven correct. And at this point I'm playing into the very same mindset that essentially explains where Planck's Principle comes from, but perhaps such being a part of humanity is not an entirely bad thing. It's certainly been with us even as mankind has gone through unprecedented leaps of understanding and technological advancement.
To the extent that decoherence is the currently favored interpretation of quantum mechanics, that's basically now. In that picture, god does not play dice with the universe, rather the observers are themselves the dice.
*statements only apply to maps whose domain is finite-dimensional
[deleted]
It's a game of string transformations, where the goal is to produce specific strings given a set of rules.
The (syntactically valid) strings would correspond to statements, a producible string a theorem, and the production the proof.
I've done both of those things. I know what you get taught. But I've kept my math education going for the 25 years since then. I've talked to practicing mathematicians about what they do. I've learned a lot about the scope of math.
As an aside: most people really dislike it when I say that they should be much more precise about different numerical systems. The integers are not a subset of the rationals. They are entirely different constructions, but there is an isomorphism between integers and a subset of the rationals that preserves the integers' ring structure within that subset of the rationals and a few other aesthetic concerns. You can see why no one wants to communicate like this, even if they acknowledge it's technically correct. So I know all about pushing symbols around.
But I also know that pushing symbols around isn't the whole story. Pushing symbols around is only useful as a final check. Do you want to validate that 1+2=3? Pushing symbols around can help. But how do you decide that the ideas behind 1, 2, 3, +, and = are worth having precise and compact representations?
Math doesn't just use formal systems to generate proofs. It's not enough for symbols to be arranged neatly according to some rules. Math is also the process of creating the sets of symbols and their rules and communicating to other people why this set of rules and symbols is interesting. What ideas get preserved when you are working with this system? What is it an abstraction over?
> The cool thing is that training on diverse datasets improves scores on other downstream tasks, while the training objective is the same.
Maybe for some language modelling tasks, i.e. it learns some internal representation that is transferable. However I would find it quite odd if a model becomes good at Bio while not explicitly going through Bio training.
You said:
> > nor are they trained for each task individually.
> They are explicitly trained for each task individually.
And that's the main misunderstanding.
Collins says:
individually in American English (ˌɪndəˈvɪdʒuəli, ˌɪndəˈvɪdʒəli) adverb 1. as an individual or individuals rather than as a group; one at a time; separately; singly
Which is precisely what LMs don't do (in contrast to previous "AI" models, which did do that). They are trained on every datapoint at the same time. So long as we agree on that, I think we are saying the same thing :)
Again, what level of copyright violation is evil? Downloading music without paying for it? Apparently using images/text that artists have made public is evil, so I'm curious what the bar is here for evil.
Using electricity to improve white collar efficiency is also evil. Good to know
This bot posts a tautology (always true statement) every day. They aren't very useful. Sampling from all true mathematics is like sampling from all instruction sequences that don't crash. The important part of computer programming isn't finding valid instruction sequences, it's finding the useful ones that do what the customer wants.
How much of a good machine learning system in production is really "the model"? How many lines of code are dedicated to constructing features and preprocessing them? How many lines are needed to process the decision emitted by the model in context of whatever else is going on? How often does the customer interact directly with the inference/prediction from a machine learning model?
My experience has been that model-fitting and model inference very often ends up being part of a bigger system anyway. And even if you do end up with some kind of super-duper all-purpose predictor model, it's rarely the thing you start with, instead you work up to it over weeks or months of iteration. So why should we put so much privilege and esteem on the matrix transformatinos or the decision tree, when they are really just part of a bigger system that receives some input from somewhere and produces useful output for someone?
The same holds for AI in my opinion. An AI system is a system that accepts inputs and produces useful outputs. LLMs are borderline miraculous in that an AI system built around an LLM can do so much more than anything that came before, and you can push a lot of amazing things right down into the tensors inside the LLM. But how far can that go? I don't think we even have an answer yet, because it's all so new and every time it looks like it's going to plateau, the big labs come out with another big step forward.
But there are other questions too, which should look familiar to anyone in industry. Do we need to do it that way? Should we do it that way? If our goal is to build a useful AI system that balances power and cost, then maybe we shouldn't. What if we can make models 10x bigger and spend 10x on RLHF and achieve the behavior we're talking about entirely in tensors. OK, so what if we can? We can also run a collection of little models in a carefully designed harness and achieve that behavior right now, today, at a much lower cost both in terms of up-front investment and marginal cost per unit of work completed.
I get it from an elegance perspective, but I guess I have completely the opposite mindset. Industry has bled me dry of any desire for elegance. The stuff I build now is stupid and crude but it makes our customers happy and costs peanuts to run and that's exactly what my job wants from me. So I say let's commoditize LLMs and start being clever about how we use them. It's not that we shouldn't also push the frontier in size and power, but unless things change w.r.t. the actual costs involved, it doesn't really seem like the best way forward in the short term for achieving smarter AI systems without also making costs go up and up forever.
The bitter lesson still holds of course. But eventually you have to pay for all that power. And you might not want to shell out $20/1M just so you can be sure your LLM can detect uncertainty in its own context and be more honest about when it doesn't know anything about some obscure record label.
Type B: “directionally correct” ML inferences that provide value by virtue of outputting an inference regardless of its accuracy. The value comes from providing automated decision that allows someone or something to move forward in a process, similar to management consultants. This is used heavily in ad tech and (social) media algorithms. I would even put gambling and investing inferences in this bucket as the accuracy of algorithms isn’t really required to be that high to provide alpha.
Type A: ML inferences that are creating or replacing systems where high accuracy is table stakes. This is applications in industrial engineering, chemical engineering, biotechnology, etc. If you can’t beat any existing automated or non-automated systems in terms of accuracy, your product is dead in the water. You can make it a few years by faking it but eventually the pied piper makes his call, and a major contract falls through. This has always been the lifecycle of products I’ve been on. It’s an incredibly difficult problem. “Faking it” here means piling on heuristics upon heuristics to convince someone to sign a contract, even if the underlying precision-recall tradeoff curve isn’t financially viable. This is the basis for the conversations between myself and my colleagues that a model that can’t provide actionable insights without a wall of heuristics / post-processing is a red flag for a product.
Anyway, that generalizes to LLMs because LLMs can provide so much value in the Type B category, but anyone promising Type A products based on LLM technology is treading on thin ice, imo.
Edit: also, as an aside, feature extraction and post-processing of inferences is necessary for any model, but if that code becomes bloated is when I lose confidence in the model’s ability to provide inference value.
There’s a classic stack overflow from a decade ago that I remember where a ML engineer / DS was asking if a linear regression model trained on sorted data (X, Y sorted independently) had any inference value. They asked because their manager insisted that was the correct way to do it because it minimized training error. Well, duh. Two sorted lists of values are maximally correlated.
This is an extreme example of what I mean by “preprocessing data”.
An extreme example of “postprocessing results” would be to create a decision tree based on the output of a decision tree algorithm that re-sorts values into something that is palatable for the customer, based on feedback from the customer on a case-by-case basis. “Hey this was a false positive…” -> add an “if” statement to the postprocessing.
Indeed there isn't such tradition. I have one or two results like that -- proofs that some proof strategies cannot work because some object does not exist, but since that object would not be interesting for anyone not trying that particular proof strategy for that particular (already obscure) problem, one cannot publish.
Typically, you can describe that in the form of a partial result (see for example https://en.wikipedia.org/wiki/Goldbach%27s_conjecture#Partia...) or as another conjecture.
Arguably mathematics should have pre-registration, so you can see who has tried what before, rather than just by knowing everyone in your field. As LLMs progress, we might get pre-registration of LLM-aided research. "We plan to spend $10K on Fable tokens to look at conjecture X is algebraic co-homology."
There is a related tradition of making conjectures about things that you can not prove, and being known for having made such conjectures. Conjectures along with definitions and problem statements are incredibly important in mathematics. But usually they are introduced in the context of some other publishable work.
It would have to show something new and interesting.
A public school in Britain does not receive public funding.
A public school in the US is entirely publicly funded.
Crippling doubt can happen. Blind confidence has its own hazards. You only need to be confident that you can proceed, in spite of having provisional, incomplete knowledge. "But if you grip to your beliefs too tightly, you will not recognise The Truth when it comes knocking on your door." (forget who said that)
(Note that this is about excluded middle. There ARE constructive logics with interpretations of excluded middle, e.g. some forms of classical linear logic, but they do not play as nicely with other logics. Constructivists often reject even weak forms of choice for largely the same reasons--there are some forms of choice that are constructively valid in some logics, but these results often fail to hold true in more conventional logics. And the same is true for a whole host of related notions that proof assistants like Rocq reject by default, propositional extensionality (which says that two proofs of the same proposition are equal) and function extensionality (which says functions are equal whenever their results are equal on all the arguments in their domain -- which might seem obviously acceptable until you realize that it's false in most programming languages!) being prominent but much less discussed examples. It's all about remaining broadly compatible with lots of different types of reasoning, not because people think the reasoning is invalid per se).
I find it hard to believe that a constructivist would agree that across the board, proof of existence of X is more interesting than a construction of X. Isn't that the point!?
The constructivist will still object that you can’t, from that, conclude that “…therefore a counterexample must exist,” without actually providing a counterexample. But the general principle I was describing still applies - a proof often gives you insight that an example by itself doesn’t.
The part that I was referring to was the last statement from the OP: that "a proof of existence of a counterexample necessarily provides more insight than a counterexample". I can't imagine a constructivist would agree with that in general.
This actually strikes me as a very formal perspective.
Considering it from an informal perspective, it's a bit more fuzzy isn't it. As you say there are many isomorphic things, and when we say The Integers it's not actually clear which one of them we mean. Maybe we mean one of them today and another tomorrow. Often times it doesn't matter, and so we don't clarify the question.
Like you could imagine defining the BootstrapNaturals then the BootstrapIntegers then the BootstrapRationals then use them to define the Reals. And then say that the Naturals, Integers and Rationals are defined as subsets of the Reals. This would be one way to put the common view of the Naturals as being a subset of the Reals on a solid formal foundation. It's rarely done ig because it's seen as obviously unproblematic to be a bit handwavy.
Another criticism of the common construction of numbers we could pose, inspired by object oriented programming, is that they fail at "information hiding". In programming an object should ideally not expose its internals. But in mathematics we may define 0 as say the empty set, making set operations on numbers syntactically valid which is kinda strange.
But yeah I think everyone has a sort of implicit understanding that 0 isn't actually the empty set. That it's merely a sort of hmm... thought experiment? That considering it 0 is a limited time offer, for the duration of the definition phase?
Maybe we come back to the isomorphism after all. "The natural numbers are something isomorphic to this set stuff I will now do"
Whereas a counterexample, on its own, proves the proposition false but doesn't necessarily tell you anything else.
The real difference in the constructive case is that there are fewer classes of proposition for which a proof without witnesses is possible.
(Edit: side note, I didn't explicitly say "necessarily" in my original comment. I suppose there could be exceptions, although I'm struggling to think of an example. Constructively speaking, the ball is in your court!)
In this case, I think part of the problem is that there was kind of no good reason to think the Jacobian conjecture was true in > 2 dimensions other than it being kind of hard to find counterexamples. So a really interesting disproof would be one that, e.g., was able to exhaustively classify the counterexamples, or showed why it seemed in practice to be hard to come up with functions violating the conjecture. AFAIK, this doesn't really accomplish either of those things, not even after you learn the procedure that constructed the function -- it kind of tells you why we should have expected to find a counterexample but not how rare such counterexamples are.
It depends on how old an intuitionist/constructionist you are. Back in the day, they were interested in logic as a description of correct reasoning. Brouwer saw LEM as a mistake in the foundations.
These days, the influence of formalization, including proof theory and model theory, has removed a lot of the teeth from that debate and made it possible to summarize as you have.
I studied this in the early 1980s, and my professor was definitely in the "this is a black and white issue" camp, although he came down on the classical side.
(Side note, I was once a back seat passenger in a car with my prof and Quine in the front seat, who was visiting at the time. Quine was famously committed to the idea that first order logic is the only kind worthy of the name.)