> On the second day, there are two gaps: “between nothing and zero” and “between zero and nothing”. Two numbers spawn in those two gaps. Call them –1 and 1.
Got lost here. I think I'm officially too dumb for math.
I'm hoping someone develops an interactive tutor that can teach any subject to any depth.
The tutor should optimize its pedagogy. It should use online RL to adapt to a learner's ideal learning style, model what the student understands and to what degree, and understand what the gaps and next steps are.
Broadly, universities are too expensive, inequitable, suboptimal, not portable, slow for this use case.
Universities are great for networking, starting projects with other students (not the ones professors mandate), and learning lab sciences. In research, they're great for institutional knowledge, having a community of peers, getting guidance from research advisors, having real equipment and funding, etc.
But there's a great need for tools like this outside of that setting.
Anecdotally, I'm a working adult. I'm not going to waste time in college again. I need this for me.
Yeah I'm curious about the difference between "nothing" and "0", but I just decided to roll with it. Until the Greek letters made my head start to spin as they usually do.
I don't think this is your fault; the description isn't very explicit. Let me try to do a bit better. (I'll also try to go somewhat further, and you should not be discouraged if at some point it stops making sense.)
You can think of the "surreal numbers" as being built up step by step. We start out with no numbers at all, and then we repeatedly do a construction that makes some new numbers.
A surreal number is made from two sets of (pre-existing) surreal numbers. We typically call them L and R, for "left" and "right", and sometimes write it as L|R or {L|R} or something like that. The "left" numbers have to be smaller than the "right" numbers. The resulting number will turn out to be, in a certain sense, the "simplest" number in between all the left numbers and all the right numbers.
Now, as I said, we start out with no numbers at all. It might seem like that gives us no way to proceed, but it does: even given no numbers at all, we can still make a set of numbers, namely the empty set! So we can use that for both L and R, getting ∅|∅. Empty sets on both sides. We call this 0, and it will turn out to behave in the way you'd expect the number 0 to behave.
Now we suddenly have another set available, namely {0}, the set containing only zero. Which means that instead of being able to make one number, maybe we can make four: ∅|∅, ∅|{0}, {0}|∅, {0}|{0}. The first of these we already knew about. The last isn't actually admissible -- remember that the "left" numbers have to be smaller than the "right" numbers, which is "vacuously" true when one of those sets is empty (it means "if you have a number x in the left set, and a number y in the right set, then x<y", and if there are no numbers in the left set or no numbers in the right set then that's trivially true) but isn't true when both sets contain 0 because 0<0 is false.
So actually we get two new numbers: ∅|{0} and {0}|∅. The first fits into what OP calls the gap "between nothing and zero". The second first into what OP calls "the gap between zero and nothing". In both cases, "zero" means a number and "nothing" means a space where we don't yet have any numbers.
The number ∅|{0} is called -1 (it has to lie to the left of 0, and there's no constraint on its left, and -1 is "the simplest number less than 0") and the number {0}|∅ is called +1 (it has to lie to the right of 0, and there's no constraint on its right, and +1 is "the simplest number greater than 0").
I should explicitly acknowledge that I haven't defined what "less than" and "greater than" actually mean for these numbers, nor anything else about how they relate to one another that could possibly justify giving these things the specific names 0, -1, and +1. But there are definitions for "less than" and "greater than" and "plus" and "minus" and so forth, and the whole thing does turn out to work very nicely.
Anyway, once we've got these numbers we have eight possible sets that can go on the left or on the right. The requirement for left-things to be smaller than right-things reduces the possibilities somewhat, and the actual new numbers we get next time around are: ∅|{-1}, which turns out to be -2; {-1}|{0} which turns out to be -1/2; {0}|{+1} which turns out to be +1/2; {+1}|∅ which turns out to be +2. We also get some already-existing numbers in new ways; for instance, {-1}|{+1} is actually equal to 0 ("0 is the simplest number between -1 and +1"). Again, I should explicitly acknowlege that I haven't said anything about how you determine when two of these things are actually equal; again, it does all turn out to work properly.
If you keep going with this construction, you produce all the integers, two at a ti...
What an interesting construction. Thank you from a curious layman for your write-up. I thought it was pretty easy to follow. I'd heard of the surreal numbers before and never knew about the construction mind-game behind them.
Thank you for this explanation! The construction is so elegant, and in a way, the basic idea is simple (?) -- I wonder why it wasn't thought up of much earlier than it was. Maybe it's a little bit like https://en.wikipedia.org/wiki/Egg_of_Columbus
Not only is the basic idea simple, it's a sort of generalization of two other things that were already well known but before Conway were thought of as completely independent.
First: the construction of the real numbers from (traditionally) the rational numbers by means of "Dedekind cuts" (sometimes called "Dedekind sections"). The idea is that if you're trying to build up the machinery of mathematics from scratch, it's not too hard to go step by step from (say) sets to nonnegative integers to integers to rational numbers, but it's harder to get from there to the real numbers, and Dedekind's idea is to say that e.g. the square root of 2 is the way of chopping the rational numbers into "things less than the square root of 2" and "things greater than the square root of 2".
Second: the construction of the ordinal numbers (a sort of generalization of the notion of "nonnegative integer" that allows the numbers to get very infinite) due to von Neumann: you start off saying that zero "is" the empty set, and then you repeatedly say: the next ordinal "is" the set of all the ordinals you've constructed so far. So, e.g., 1 = {0}, and then 2 = {0,1}, etc. -- but once you've constructed all the nonnegative integers you can then look at {0,1,2,...} and that's a new ordinal typically called ω, and then you can take {0,1,2,...,ω} and call it ω+1, and so on and so forth.
Both of these are special cases of what Conway does: Dedekind's is the case where all the numbers are rational numbers and you don't allow either set to be empty, and von Neumann's is where you _require_ the right-hand set to be empty.
There's a further connection, which I believe is how Conway found these things in the first place: if in the definition of surreal numbers you delete the requirement that everything in L has to be less than everything in R, then what you've got is (more or less) the definition of a position in a two-player game. L is the set of positions one player can move to, R is the set of positions the other player can move to. (I say "more or less" because e.g. in many games you're allowed to repeat positions, and games may have complicated winning conditions or involve chance or whatever.) And there's a whole rather nice thing called "combinatorial game theory" that's all about these, and from that perspective numbers are just one particular kind of (position in a) game. (Specifically, a number is a game in which at no point in the subsequent gameplay can it ever make your position better for you to make a move: you'd always rather pass if you could.)
Thank you for writing a detailed explanation! I've slightly edited mine to explain the infinity jump. Yours is, of course, much more detailed.
For the infinitesimal number, I think it makes more sense to use {0}|{1,1/2,1/4,1/8,...} since it gets born at the same day as say 1/3. So it is easier to understand how it arises without "waiting" for all reals.
Oops, that was an oversight: indeed you don't get all the rationals I need for what I wrote until "one day later" (in Knuth's terminology). Regrettably I'm too late to edit what I wrote above.
> On the second day, there are two gaps: “between nothing and zero” and “between zero and nothing”. Two numbers spawn in those two gaps. Call them –1 and 1.
That's a mistake. They should've written "empty set of surreal numbers" and not "nothing".
It is a constructive theory, like sets/ordinals. For ordinals you can use ∅, { }, ∪ and you construct
∅, {∅}, {{∅},∅}, ... (von Neumann ordinals).
For surreal numbers you use the form { A | B } where A and B are sets of surreal numbers. Some restrictions apply so not all of these forms will be surreal numbers.
What is the problem with saying “nothing” to mean “empty set” in an informal explanation? If you put apples between two bags, and the right bag is empty, it’s reasonable to say “nothing” accurately describes the contents of the right bag.
I’m slightly stretching the metaphor here because the number lines gives me enough structure (order expressed visually) and I only deal with at most one set item at a time (since we construct in the order of simplicity and can use the already constructed numbers), so it (IMO) unnecessarily complicates things to even talk about sets when we’re sort of just making cuts on the line. But in either case I don’t see the problem with colloquially saying “nothing” here.
He seems genuinely interested in Surreal numbers. Seems like he found value in exploring them and the Lean process, devoting time and interest to it and understanding what it's like to be a mathematician. I think a lot of people who go into Computer Science may have been mathematicians in the 30s before they became separate majors at the university level.
Every human has to go through this in modern times.
I got quite frustrated and disappointed when taking pictures because everyone was doing it and my picture of x was similiar to others taking picture of x.
Either you learn from it and accept that and still do it, or you don't.
"Given infinite thinking time a finite number of humans will solve all theorems"
I also love the angle that this was not intelligence just brute force. As if the mathematicians didn't reeaaally want to solve this they were just too lazy to give it a good try.
What does AI have to actually do before you realize these things are actually smart?
There certainly are such proofs. Even for simple decidable theories we have very large lower bounds on decision complexity (like double exponential), which implies large lower bounds on the function from "length of theorem statement" to "length of shortest proof".
It's impossible for finite number of LLMs to solve all theorems. This would imply that the busy beaver sequence is computable which implies the halting problem is decidable.
Even if the busy beaver sequence were computable and the halting problem were decidable, Gödel's incompleteness theorems would still prevent all theorems from being solved, regardless of if one used LLMs or not.
I think there's a really important sense in which Godel's argument is not the full story.
IIUC, Godel's incompleteness is less about theorems and more about axiomatic systems. Given an axiomatic system, there are statements within it which cannot be proven or disproven. It's relatively unrelated to the platonic ideal of the theorem itself. The statements it considers are axiomatic-system-specific.
Another way to view it is, who cares if we can't prove or disprove "This statement is false". There are more interesting theorems, I want to know whether we can prove or disprove other more interesting theorems.
The busy beaver computability argument addresses these issues. The problem format is always "For Turing machine T with no input, does T halt?". We know already that BB(432) is independent of ZF, aka, there is a 432-state TMs which ZF can't prove or disprove the halting behaviour of.
The core issue is that any fixed LLM can only encode so many axiomatic systems in its states, and the fixed systems implies an upper bound in terms of the BB number which it can solve. Godel is only looking at one system at a time, while BB is a way to use a common problem format to rank every axiomatic system on an infinite number line.
But a 432-state TM is a problem that we would like to "prove" is it not? It's not even a particularly complex one to begin with, my smartwatch has orders of magnitude more state then that and yet here we see that all of our math "fails" at it.
I'm no mathematician, but this is also the crux of Gödel's theorem, he just showed it in a more "hacky" and clever way - but BB(432)'s relation to ZF is also a consequence of Gödel's more general idea, is it not?
Even more concretely, the halting problem for turing machines with halting problem oracle would be undecidable for them. And if you could solve that you won't believe what problem would be undecidable. It's turtles all the way up.
The problem with what you're saying is that any old random true proposition about the integers is not necessarily interesting enough to be called a theorem. GIT (or the uncomputability of the Busy Beaver problem) does not establish a limitation on proving theorems, but rather on determining whether a proposition is true or not. Most propositions are ugly and irrelevant. So GIT/Busy Beaver is irrelevant.
-----
Oh, and your statement is wrong for another reason: All proofs are conditional on axioms. If those axioms are computably enumerable, then all of their consequences are computably enumerable too.
Most propositions may be ugly and irrelevant, but how do you know how many are not so and we just can't prove it? Also, what about stuff like Continuum Hypothesis, would you add it or not?
We are talking about the same thing, but I would actually put this the other way around.
Computation and computability is "the final frontier". Math is a "subset" of that. Doesn't matter if we choose ZFC or in the future discover some "better" subset of core axioms, we will always hit limits where BB will trivially skip over whatever we could prove (let alone Gödel's theorems).
> given fixed input of the statement with no other information sources
Also, this is just trivially avoidable, so not sure if we really should be concerned about this limitation. An LLM in a loop where it can write on a tape can be Turing complete, ergo it can compute anything computable and is "bigger" than math at that point.
> Computation and computability is "the final frontier". Math is a "subset" of that.
Maybe I'm misunderstanding you point, but I don't know how widely this would be held as true. Are you defining "math" as _only_ what can be proven under some particular formal system?
Well, I only know how to define computability in terms of Turing machines.
For math I don't have a fix definition, but it's surely a bit more specific than that (e.g. I wouldn't consider the computation that prints a 0 at the same place for infinity math) - but of course I do see the circularity in my argument: a Turing machine is a mathematical object in and of itself. Though being able to talk about something doesn't necessarily change which is "bigger".
As for the other direction, this gets a bit more into the philosophy behind math itself. Constructive math's territory is "easy" - but I am on the opinion that if humans (or any intelligent physical entity) are at most Turing-complete [1], then any non-constructive math "steps" or thoughts must also be at most computable. Well, unfortunately I can't prove whether math done by transcendent entities are also computable, though.
In any case, I am no mathematician, so whatever I think regarding this topic may not have much relevance to anyone, only done CS course with quite a bit of math, but that's obviously not the same.
[1] I believe religion is an escape hatch here from an argument perspective
> if humans (or any intelligent physical entity) are at most Turing-complete
This is a bit of a strange assumption to make. I do agree that a human, if it had infinite memory, would be an universal machine, i.e. capable of computing any given Turing machine [0]. But would that be the limits of its capabilities? It's far from certain.
You'll get into the philosophy of free will (funnily enough, a sort of inverted Turing test), i.e. for a given human with infinite memory, is there a Turing machine that exactly replicates the behavior of that human? Is our behavior governed entirely by rules? Would that imply that a human themselves is a kind of Chinese room [1]?
> any non-constructive math "steps" or thoughts must also be at most computable.
What does it mean for a "thought" to be computable? Compare to Gödel's incompleteness theorem. Clearly the act of stating the thought, or writing down the theorem, is computable. But proving it to be true or false may very well be impossible.
Ur computer is a physical system and some aspects of it uncomputable. You cant approximate or predict everything. Picture it as billiard balls modeling a circuit, you can’t tell whether it halts, meaning you don’t know where the balls will be.
Or a program that knocks out a bottle when it finds a counter example for whatever . U can’t tell whether it will spill the liquid.
And you have as well the problems of approximating the continuous with bits, you’ll always lose information
A human can't tell if it halts either, friend. A simulation of that human will follow the same infinite step calculation and they will behave identically.
I hear how passionately you want to believe these things. Unfortunately they're not true. I suggest you look into it.
> What does it mean for a "thought" to be computable?
Well, given our scientific knowledge it's a molecule-level (only important to disregard quantum physics to make the case easier) physical/chemical process, that we should in principle be able to simulate on any other medium, including a Turing machine.
Nonetheless, I can accept the definition of math where it's about "truths" and truths can obviously exist without being computable.
Does that mean that humans could produce mathematical proofs that are entirely logical and verifiable by other humans, but that cannot be formalised in any automatically verifiable language such as lean?
> Computation and computability is "the final frontier". Math is a "subset" of that.
In what sense? BB(n) is a prime example of an object that can be mathematically defined, yet is not computable. Or see BBB(n) for an "even more" uncomputable function. [0]
> An LLM in a loop where it can write on a tape can be Turing complete
What does this mean? A given LLM, like a given C program, can't really be Turing complete or not in a meaningful sense. The C programming language, or the concept of LLMs in general can be said to be Turning complete or not. Do you mean to state that LLMs in general are not Turing complete, but being "in a loop" somehow makes a difference?
> it can compute anything computable and is "bigger" than math at that point
Again, in what sense is it "bigger" than math? Lots of things are Turing complete, I wouldn't classify lambda calculus as "bigger" than math.
Because then you would actually learn something. What else?
I don’t know what correction to make because you are not even wrong. You are _kinda_ wrong in comparing math and computing via a subset of relation, but it also doesn’t make much sense. If you consider computing as constructive math it should be a subset, but those are not sets, so it doesn’t really help.
> It's impossible for finite number of LLMs to solve all theorems. This would imply that the busy beaver sequence is computable which implies the halting problem is decidable
LLMs use RNG for sampling, so they are not pure computers.
> Instead, I have a more complicated view, which I actually expressed in my essay The Two Cultures of Mathematics a quarter of a century ago, and which can be summarized by saying that there is a spectrum of attitudes in mathematics to the relationship between problem-solving and conceptual understanding. At one end of the spectrum you have mathematicians who are primarily motivated by the wish to solve problems, who see conceptual understanding as a very important means to that end. At the other you have mathematicians who are primarily motivated by the wish to attain conceptual understanding, who see problem-solving as a very important means to that end.
> Instead, I have a more complicated view, which I actually expressed in my essay The Two Cultures of Mathematics a quarter of a century ago, and which can be summarized by saying that there is a spectrum of attitudes in mathematics to the relationship between problem-solving and conceptual understanding. At one end of the spectrum you have mathematicians who are primarily motivated by the wish to solve problems, who see conceptual understanding as a very important means to that end. At the other you have mathematicians who are primarily motivated by the wish to attain conceptual understanding, who see problem-solving as a very important means to that end.
Before, understand and problem-solving-ability were so interdependent that distinguishing between the two was practically very difficult and probably wouldn’t have changed anyone’s research agenda. Now, they’re not connected, and this guy just did the ultimate meta-experiment of seriously undertaking a project that is intentionally 100% problem-solving and 0% understanding to prove it (maybe 99% and 1% but pretty close. In his transcripts, he never asks ChatGPT about the math, only about its opinions of the math).
As we (as a society) sit around asking ourselves what mathematicians (and software engineers, and anyone in deep technical fields) should be doing all day, we now have this case study to show us how wide our range of options has become.
> So, assuming my proof doesn’t rely on a Lean kernel bug, it’s likely to be legit too.
He lacks the understanding to verify his solution properly, and has to lean on those who do have the understanding to verify it, only being able to say himself that it's "likely" to be correct. (And what do those mathematicians get for laboriously checking the generated proof? 40 grand?)
Seems to me problem solving is as dependent on understanding as ever.
Moverover, the version I linked above is intentionally paranoid so it doesn't use any third-party code except Mathlib. If you allow usage of CombinatorialGames and trust its definitions, the part that needs to be checked narrows down to exactly 20 lines of code: https://github.com/gaearon/conway-refinement/blob/264445c93b...
Finally, you might be wondering about the token cost. I wasn’t running this project in a particularly token-efficient way and have repeatedly maxed out my 20x Pro subscriptions for both Claude and ChatGPT every week. I also briefly had access to a prerelease model in the last few days, which did not have a usage cap. I was not tracking my actual token usage consistently. Some AI analysis from the recovered logs roughly estimates that we’re totaling around 40 billion tokens, of which around 210 million were output tokens. Over 95% were cache reads.
Who can pay for a 20x Pro subscriptions and also get prerelease models? something weird is going on here.
> Who can pay for a 20x Pro subscriptions and also get prerelease models? something weird is going on here.
This is usual. A model before it is released will often show up in place of the current model. It's quite obvious as it has a bit of a different 'voice' and sometimes before accompanied by an A/B 'which is best?', but otherwise be labelled as the old model. 'Trusted partners' get it first, but so do some paid users, especially those that have long been pro users. GPT 6 Sol is in this phase now.
I don't know why the author could claim this is "their" proof, and they kept saying "they" did this, "they" built that. but in reality everything is done by the LLM and the author is merely asking it to do things. i guess they did contribute money at least...
Author here! My impression is that it's customary in the mathematical community to take responsibility for the result with your name, regardless of whether it came from LLM etc (as long as you disclose LLM usage). I am perfectly fine calling it "LLM's proof" or somehow else, but it's "my" in the sense that "if there is a mistake in it, it is my mistake".
I apologize to Dan Abramov for venting my frustrations about things outside of either of our control and unfairly using him as a punching bag. He seems to be an intelligent person and I hope he continues learning mathematics using whatever tools he sees fit, including AI. It was wrong of me to do this and I will take a break from this website for one week.
When you use a drill to put a hole in the wall, do you take credit for it, or do you credit the drill? Without intent, a tool, whether it be a drill or an LLM, is just an inert object.
Someone had to choose the problem, steer the model, and check the output - it's clearly taken a lot of time. That's authorship with a powerful tool, same as it's always been.
They still needed to invest time and other resources into this. It's listed clearly in the 2nd paragraph. Mathematicians, or anyone for that matter, don't figure out everything from scratch. They lean on the work that others have done before them to save time. How is this any different?
I don't understand your comment. At first it seems like you think the LLM should get credit for the work. But then you mock the author for asking about the LLM's mood, which makes me think you believe the LLM is just a tool and not capable of receiving credit (FWIW I would agree.)
Just saying (as an author) I don't believe that LLMs have conscious experiences, but the word "mood" was a good languagespace anchor for the kind of information I wanted to get out of the LLM at the time.
author provided nearly no intellectual input into solving the problem, so they IMO don't deserve credit. and it doesn't make sense to anthropomorphize LLMs and talking about their "mood". these are two unrelated statements.
as to if you want to give the credit to the LLM, or if you believe nobody gets the credit, is another separate question.
If there is consensus on how to attribute credit for LLM-solved human-steered (with no mathematical human input) proofs, I am happy to follow that consensus. Do you have a concrete alternative recommendation? What should I change?
You’re conflating two ways of understanding “credit”. One version is what the tool gets, an honest description that the tool solved it. The other is a concept used in the math community to divvy up job opportunities.
There’s not going to be anyone to understand the pursued knowledge when this job gets killed off, which means you’re supporting the reduction of knowledge. That is what’s “unbecoming”.
LLMs need a lot of help to get to any kind of complicated proof, really. And yes, they get in moods. I spent 3 weeks trying to prove something and frequently had to try and convince Claude that it wasn't impossible and that it could really do it.
That makes perfect sense. Using language in unorthodox ways to convey very specific concepts that only make sense to you and sound like bullshit to others.
I never expected a machine to be better at articulating complex thoughts with a spare number of semantic coordinates, but then I never expected to find out that my poetry was golfing in the latent space
I had a manic friend in college who later became a Emmy-winning television writer. One night over a quarter century ago, he stayed up about 24 hours straight doing nothing but writing, completely free form, some of it prose, some structured rhyme, some of it dialogue with stage directions. He pinned it to his dorm walls like it was wallpaper for a week, then we took it out to the field and burned it. The surviving paper that didn't burn made up bizarre strings of words that sounded much like this, which he retyped and called it poetry. It totally worked.
This sort of thing is why STEM students need more humanities classes. The idea that poetry is semantically denser than prose is, like, obvious, to anybody who cares about poetry.
I never got the point of poetry, even after giving it an honest shot many times. It felt far too compressed to express any thing. I could not separate it from how I would appreciate music. Maybe its because I don't start from the same base as others.
You are right, maybe some humanities classes would've helped or I'm just wired this way.
It's pretty similar to music, yeah. Or perhaps music can be similar to poetry. Just this morning I was re-reading the lyrics for "Pale Green Things" & "Woke Up New" by The Mountain Goats. There's a sort of specificity in intention that the form tends to end up dictating, that can really carry a rich emotional context or metaphor more directly into the listener's brain.
(Of course, prose is sort of like a superset of poetry - it's not a hard dividing line. You may find especially poetic lines in your favorite longform works, especially in good fiction books.)
I do think that many English teachers do a poor job of encouraging a love, or even understanding, of poetry. One of my highschool teachers was in love almost with categorizing the forms of poetry - sonnets and sestets and villanelles, and seemed to think that if we learned the rules about what lines had to rhyme or which syllables to stress, we'd enjoy poetry. I hated it! But then the next year, even against this backdrop of learned avoidance, my teacher was so in love with the ability of poetry to communicate - the unfolding of a few words into meaning like a flower in bloom - something clicked. He focused almost not at all on the structure of poetry, but rather on finding works that spoke to you. I'm still not a lover of poetry, even now, but I have poems I appreciate.
Nit, I know, but I don't think they are trained on too much pretentious writing so much as they are RLHF'd into it because that writing impresses people.
Here's my conjecture. Large Language Models are the great filter. They represent a local maximum in the technological advancement of a species from which we will not escape.
People will just limit publishing valid works to avoid becoming a hapless plagiarism victim class. Same thing happened to tech bloggers ripped off by low-effort you-tube content makers.
Isomorphic plagiarism makes people feel 23% smarter, but it also provably degrades core skills by 17%.
LLM are great at context search, but are also trivially proven degenerative under recursive self improvement scenarios. We look forwards to stripping their assets at a heavy discount.
Also, we shouldn't kink shame peoples cognitive dildo choices. =3
A wonderfully made introduction to the surreal numbers and their surrounding game theoretic concepts is this video on Hackenbush[0], a winner in 3Blue1Brown's Summer of Math competition.
>I’ve emailed some of the mathematicians with a few proposed typo fixes, and I got confirmation that at least a few of those fixes seemed real. However, some of the problems that weren’t backed by Lean also turned out to be misunderstandings.
I think this project is really neat, but is it appropriate to cold email specialists before you've put in enough hours of effort to describe yourself as more than an "amateur"? OP's emails may have been helpful, but billions of people use these LLMs to wade into new areas and email is already low signal-to-noise.
Yeah it's a pretty tough question! I've resisted doing that until I had a relatively high certainty that their published results contained minor mistakes, which I assumed they would want to know about. I've also been explicitly apologetic and tried to keep it super brief.
A counterpoint - I was told a story by one of my professors in the late 1990s, about one of his professors -- he'd written a thesis, gotten hired somewhere like Princeton, and taught there for a few years as Dr. <Somebody>. One day he received a letter pointing out a construction flaw in his thesis. He brought it to the department head who read the letter, and said "Well, Mr. Somebody, ..." Ultimately he fixed the proof.
Upshot, if there are real errors in published work, I think most mathematicians want to know about them.
Yea but that was a person who actually put in work and had to think about and understand the problem. They didn't just generate something with a magic box.
As a software engineer, I could not care less about how a bug was found or by whom, as long as I can quickly verify it is correct, I always appreciate being able to improve my work. I don't see why it should be different for mathematicians (the ones I knew would think similarly, I would assume.)
If I may offer an analogy, what I tried to do is essentially reporting a bug after having a failing unit test that exercises the public API, without looking into the black box of internals.
This issue really separates the wheat from the chaff. The dirty secret is that a lot of academic published work contains errors but the authors also have fragile egos. It reminds me of when Data Colada exposed someone for fraud and they accused the exposers of "methodological terrorism" (something in psychology or social science). Just imagine what happens once papers get exposed at scale.
Now here there was no fraud just genuine error, but it will annoy people nonetheless and scrape their ego that someone uninitiated can just type some stuff in a magic box and conclude that they, the established published, tenured mathematician with awards and medals can be wrong.
(Background: trained, published, but still amateur mathematician.)
This is a cool blog post and I think you're going the right way, and beginning to get an understanding of the proof as you go.
I'd recommend continuing on the simplification and understanding route, until you yourself can follow the proof. Some suggestions, as I did something similar:
1. See if (or ask the AIs) if individual parts of the proof can be found elsewhere, i.e., is an argument just a copy of something else? If so, it's important to attribute this, but also this usually allows simplification ("by Theorem X", etc.)
2. Look for redundant patterns and try to combine them.
3. Ask the AI to be a critical reviewer from some journal, and try to fix its criticisms.
4. Continue simplifying! Assume that the final result may actually be relatively short.
OP has reportedly been in contact with Prof. Mantova, who actually worked (jointly with S. L'Innocente) on the key human-authored results behind this AI proof and is arguably in the best position to understand exactly what the AI added that wasn't known before. (See the OP's thread on the Lean Zulip.) So this is happening, and we might see an actual paper publication of this result down the line (possibly encompassing multiple roughly self-contained papers, building up to the final result). The current AI-written version is way too obscure for that, and the AI-written human-targeted "summaries" are not really helpful. Again the OP is quite aware of this.
Vincenzo (Mantova) here: yes, I have been reading bits and pieces of the proof and I can say for sure that the method is sound, at least for the first half (power series with real exponents). I haven't even tried reading the part that mentions the Cantor-Bendixson rank yet, although given how the rest went, I'd be really surprised if there's a problem there.
As with most interesting proofs, the number of core ideas is actually small, I'd say two for the real exponents, and presumably a third idea for lifting up to omnific integers. I have been redoing the real exponents part of the proof going on the ideas only, and with a few smarter choices, I am converging on something very short. And I mean very short, which is amazing. I didn't think the answer would be this close: it 'just' needs looking at the problem from the right angle, and also make a fairly bold guess at the outcome.
Dan's current proof is of course much longer. Between the fossilized ideas that Dan mentions in the post and the formalisation of previous results, there's a lot of cruft that inflates the proof but does not really help understanding what is going on. Luckily the word 'derivation' pops up early, otherwise it would have been very challenging to wade through the lemmas to find the important points.
Needless to say, I disagree that what Prof. Mantova is planning to do (digesting the proof and making it human-understandable) represents the "end of [mathematicians'] career". Systematizing has always been a key part of human mathematical work, and tidying up a raw proof can be viewed as a kind of systematizing.
My hope is also that Mantova and very possibly L'Innocente will get a substantial share of credit for their role in the resolution of this conjecture by Conway: the AI would not have embarked on this were it not for their prior work. So even human mathematicians with an inclination for more exploratory "problem solving" will have plenty to do in the future. (The story is actually not that different for the recent Navier-Stokes forced blowup result, which also built on key conceptual work from 2023 by Córdoba and Martinez-Zoroa.)
Luckily for these guys the problem is famous enough that giving some kind of credit for its resolution even makes sense at all. The vast majority of published work is not like this. There’s not going to be any credit divvied up to the thousands of people who’s work was probably involved in the recent formalization of FLT, which involved formalizing 300 thousand theorems.
Kevin Buzzard has reportedly been working on a more systematized (i.e. leveraging a more modern approach) and human-targeted formalization of FLT. I certainly hope that his work continues and he gets the deserved credit. Of course there is also some possibility that it won't, and that would mean you have a point after all.
I appreciate the sentiment, especially after the escalation of the last few weeks. But I am hoping this story can become an example of why mathematicians are still very much needed and LLMs are still severely lacking when it comes to displacing scientists. Conway's conjecture has no application whatsoever, even within pure maths, and the only point in pursuing it is what you can learn in the process, and whether you can make something beautiful. LLMs are consistently unable to do the latter (and yes, some mathematicians are also not very good at it... this is an old topic of discussion, just amplified by current events). To me it feels like the technology is still where it was in 2015 when DeepDream images came out: increasingly good at pattern matching, but still a lot more like dreaming than thinking. So our job is still there somewhere.
The problem is rather how quickly we can change our ways of working to make sure the training and hiring pipeline does not collapse. That's the disastrous scenario, for both the individuals affected and the discipline, that we must avert somehow. I wish we had an easy answer to that. I certainly don't. But I like to think that at least engaging with the public in a constructive way will have a net positive effect.
I’m not actually upset with your actions I was just worked up at the time. You’re in a dilemma and graciously handling it the way you are is the only sensible path.
The read was very interesting, and I think you're right, mathematicians are still very much needed, in some sense now more than ever.
But the effect is the same across other professions. We need mathematicians, we need professional grounding but we only "need" experts.
Every step AI takes feels like it slices people off the bottom of a profession, making them less relevant, while simultaneously increasing demand for the top.
the vicious cycle I see is it will "Eat the middle", you need people with juuust enough acumen in a subject to drive the AI, to set a goal and nudge to a direction, and you need a real expert to look at the results with a critical eye but you don't need the middle of the curve. I think over time this will depress hiring and wages of new people, and stunt their progress towards expertise by destroying the middle ground. Then when our current experts retire we'll be left in a lurch.
Do you buy stuff made in factories of do you open your wallet for everything handmade craft products? Or it's fine as long as craftsmen's jobs got replaced, just not when yours? Do you ever use a self-checkout? An ATM? Or do you pay extra to get cash from a human cashier at the bank?
Do you actually think this is a good argument? I had literally zero say in what happened in the past. I did not support the Midwest getting gutted. I wasn’t even able to vote when that was happening? Would it shock you that I generally think capital is misaligned to humanity?
> Would it shock you that I generally think capital is misaligned to humanity?
You still prefer to get cheaper options yourself. I know this argument gets caricatured in the "yet you participate in society" meme, but the point is that this is the aggregate result of individual humans making decisions on where to allocate their resources. You can attack this using various ideological and religious frameworks, but if it's just some stoner college freshman's communism, I'm not interested (neither if it's the more potent version that dispossessed my ancestors in Eastern Europe).
Also is your position really that nobody can point to problems or criticize anything without a fully fleshed political system to replace the USA with? I don’t support the excesses of the system of the USSR or 1950s-1980s China.
You can criticize things of course, like you can shake your fist at a cloud too when you'd rather want a sunny day, but the results may vary. You're asking people to refrain from using a cost-saving technology and instead spend more money on things that can be obtained easier with the tech. This means going against one's own rational interest. Such things usually happen willfully when the person believes in a religion like the Amish or Hasidic Jews. So having a fully fleshed political/ideological system on as similar level will be necessary here.
For some reason, this approach makes me think of the difference between “wizardry” and “sorcery” in some fantasy magic systems. The magic of “wizards” is fundamentally based on a deep study and understanding of arcane things, perhaps assisted by some (necessary or helpful) tools of great power. “Sorcerers” summon supernatural beings and are able to control them, cajole them, and protect themselves and others against them (with more or less success)... but the actual desired magical effect is performed by those beings.
Computing has historically been a field of wizardry. It's... interesting (?) to see so many people pushing so hard in the direction of sorcery, and in fact applying that sorcery to other fields, in which they themselves aren't quite able to validate whether the spell worked or not.
Differently than wizards that lock their knowledge in towers and in sects, software development has a tradition of being open for the most part, so the sorcery and wizardry analogy works more like a spectrum. It just depends on how close to the metal the apprentice would like their consciousness.
That’s fair! I think what struck me, though, is that what we’re seeing is large numbers of “wizards” jump ship to and actively promote “sorcery” instead, in this sense. That is, it’s interesting to me to see Dan Abramov, whose blog primarily consists of painstaking explanations of React internals based on the deep knowledge he developed over years as the most visible member of the core team, switch over to “do a breakthrough.”
I try to address this in the post explicitly in a few places.
Primarily I thought of this as a sort of "epistemic performance art project", maybe similar to playing Elden Ring blindfolded having never played it before, or speedrunning a game by opening a box a thousand times and overflowing some counter. It's funny and absurd to do knowledge work without the knowledge.
I think it's also a stress test of meta skills. Like, how much can we do without knowing? What kind of processes can we set up around these demons that would constrain them into our requirements? How can we know when things are going wrong? In some sense, this isn't too different from engineering management.
Naturally, I'm also interested in how much of my role in this could've been automated away. Can there be a skill for that? Then "do a breakthrough" is an irrelevant implementation detail of that skill.
Note that "do a breakthrough" actually produced the worst results over the runs. The best results were from more directed runs like searching for first obstacle towards the next milestone.
The wizards don’t become sourcerers themselves - they become enthusiastic users of someone else’s sourcery. Their years of learning don’t protect them from mistaking access to power for mastery of it.
I’ve felt like a warlock for about half a year now - talking to demons which summon code from the abyss. Exhilarating and terrifying, especially when you can tell the demons get better faster.
It's a truly wonderful read, made better by the fact the author doesn't quite understand what's going on.
The usual format that fun mathematics is presented (being talked at by someone who is very well versed in the subject) comes with a heavy cognitive burden - and often I just can't really make it through.
When the author is not an expert the writing is just so much more accessible - it's easier to understand and making it through feels more of an adventure and less of a lecture.
I've never thought previously how much I would enjoy this format though. I'm here to see more amateurs stumbling through mathematics.
Also, wasn't expecting this sort of side-quest from the guy who got me into React.
Agreed! I've always been interested in the field of mathematics, only to be let down by my lack of ability to comprehend it. I can usually follow an article up until the point that it starts using formulae.
I love this approachable prose.
If anyone is aware of any other "mathematics for people who don't know mathematics" resources I'd greatly appreciate any links.
OK this is probably not quite what you meant but I'll shoot: I highly recommend Terence Tao's Analysis textbook (which now also has a Lean counterpart on GitHub). You can skip Chapter 1 (it sets up the motivation but I couldn't answer most questions, which is part of the point). From Chapter 2, it builds up in a somewhat "dry" but actually very accessible and methodical way. It is "mathematical" but it is "for people who don't know mathematics" in the sense that it forces you to build the entire mathematics from scratch, including proving things like `a + b = b + a` as exercises. This is actually how I got into proofs in the first place, with later picking up Lean by doing Natural Number Game.
Since you respect Terence Tao, but not the general population of mathematicians, maybe you’ll read his blog posts which describe the ways your actions are detrimental to human striving.
Are you talking about the posted article? I agree that it was a fun read, but it did not present any mathematics at all. Like, none. Its not that the author not being an expert made it easy to understand, it's that there was nothing mathematical to understand presented.
> in which they themselves aren't quite able to validate whether the spell worked or not
Knowledge is of 2 kinds: know-that and know-how. Know-that is what LLMs are enabling such as the proof here, while know-how is more useful as that constitutes understanding and puts that knowledge to use.
Or like the difference between chemistry and alchemy? Understanding and reasoning with the building blocks as opposed to throwing random stuff together, trying different things and hoping it somehow produces gold.
I thought you were going to talk about the difference between D&D wizards and sorcerers: the former are the same as you describe, whereas the latter are born with some sort of innate talent for casting spells without needing to learn it or necessarily practice any discipline. It honestly also kind of fits; there's a difference between "I worked hard to learn the skills I have so I can explicitly craft the solution to the problem I have" and "idk man I just kinda point and think 'go magic spell' and the magic happens".
Sorcerers are the vibe coders of D&D magic, which perfectly describes how wizards in-universe feel about them.
> Computing has historically been a field of wizardry.
Counter argument, "historically" is not last year but closer to 2 decades ago.
modern computing has sat atop a mountain of sorcery for ages. You may be able to squint and call a good compiler a "tool of power" more than sorcery but there are plenty of other tech stacks that simply sit upon one opaque box after another.
And it's not unusual for sorcery to produce crap, even if it's production worth crap. Dreamweaver had a WYSIWYG editor ages ago and as someone who was hand crafting HTML in that era it's code was typically a mess.
Now that's the norm, almost nobody makes HTML by hand, some js framework does. And it's often shit, I've seen entire sources of nothing but <div> nested ad-nauseam, conjured up from the depths of "I-don't-care-as-long-as-it-works"
I find the way the author communicates with the LLM fascinating. For example:
> However, I didn’t just want any result; I wanted something that pulls me.
> Initially, I asked Claude:
> Me: which unsolved problems in the Surreal Numbers research program pull you the most and why?
Note the switch from "pulls me" to "pull[s] you". What is the author's perception of the relationship/boundary between them and the LLM here?
1. Are they using it to find things it flags as interesting in hopes they might also find it interesting?
2. Do they consider "interesting" to be a universal (observer-independent) trait and are using the LLM to find things that are interesting?
3. Have they delegated their desire to find something interesting to the LLM so that it can instead find something that it flags as interesting, regardless of how the author feels?
4. Do they see it as a part of their thought process, and so do not distinguish "you" from "me"?
5. Do they see it as part of them, and are referring to the combined entity in the second person?
Let me first clarify my relationship with mathematics. I think of myself as "an awestruck observer from a distance". I find some parts that I understand beautiful, and I have also tried to understand some of the basics rigorously. However, I generally just can't make my way through any serious paper, as I both lack the prerequisites and struggle with the amount of inference mathematics tends to place on the reader. That's the "from a distance" part.
Now, about picking the problem. I am genuinely "pulled by" surreal numbers themselves. I find them irresistibly beautiful. There is also a bit of bitterness around how they haven't fulfilled their promise (yet?) as Conway hoped they would be able to become a better foundation for some mathematics. But they are a bit too difficult to prove things about so far, and we know too little about them. So what "pulls me" also is a possibility of making enough dents in this that we would be able to use them more broadly, and learn even more things about them.
However, I do not know the details of the latest research. I don't know which problems have actually been solved, which pursue Conway's original vision vs narrower approaches, and which are elegant enough to feel "awestruck" enough about. So this is an invitation from me to LLM to share what it "feels pulled by" (for whatever definition; I think of it as just navigating the languagespace) , and then sifting through that list to see if something it lists makes me feel something. I would assume that with the field currently being so small (serious mathematicians mostly don't care about surreals), it's easy to get the LLM "excited" (again, just a vector in the languagespace) enough that it would give me genuinely interesting candidates. Then it's up to me to sift through them and see if they "speak" to me.
It's like asking a mathrock nerd to share their favorite mathrock albums. Niche enough that you'd likely get good results. Then you can listen and form an opinion.
In this particular example, the "ONAG birthday" and "maybe last Conway's unsolved conjecture about surreals" part spoke to me emotionally, the statement itself amazed me with its simplicity, and I felt "blood in the water" related to the recent results bringing the conjecture closer. So I felt the pull myself and went with it.
This year, LLMs have been involved in a number of interesting proofs of conjectures. But that is not even half of mathematics. Has anyone tried to use an LLM to generate a mathematically interesting conjecture, on the level of Conway's refinement conjecture? If so, what happened?
With all the talk of mathematicians possibly being obsolete, I'm wondering where the future conjectures that future LLMs would prove might come from.
I would not be surprised if an LLM could have generated this conjecture, since it's such a natural extension of the integers, does it hold for surreal integers is not a big leap. It's totally predictable / probabilistic and thats what they do at a high level.
My read on the current sitch is that the drama is more around the humans behind the LLMs, like the OpenAi *people*, who are dishonest, thieving, technocrats, stealing human mathematicians work and claiming credit for it. Since the LLMs are only trained on finite amounts of data on the internet I don't think anyone expects them to replace mathematicians in a serious way. But surely the field is changing dramatically, people will adapt.
My experience has been similar; I find ChatGPT to be much stronger and more precise at math and in communication. I also can not do better with a multiple agent flow than I can with a single agent.
My main thought is that he was performing something general here that is actually valuable and hard for a large proportion of humanity. It's like when Google search was a difficult thing, or troubleshooting a PC. what he is able to do here is actually a rare skill, called intelligence and he may think it's nothing, but it's actually very rare and hard for most people. The kind of judgment and interpretation of output without deep expertise is actually a very rare ability.
I think most people could not get this conjecture proven if given infinite time at the keyboard with the same chatbot. He demonstrated much more initiative and problem solving instinct than what a large majority of people are capable of. Have you seen people trying to trouble shoot a printer or a software issue? Often the answer is just to search Google and read some forum post and execute the steps and deal with any arising minimal obstacles. Still insurmountable to most.
I disagree. I see nothing creative about this guy’s efforts. The models will continue improving and soon his creative leaps of asking it to double check won’t be necessary.
this is a great blog post, documenting a very real process of what it's like to create large results with fallible models
though I am an expert at coding, the author's process sounds very similar. constantly double checking, asking for explanations, having AI adversarially check its own work, trying to detect bullshit
210 comments
[ 4.8 ms ] story [ 265 ms ] threadGot lost here. I think I'm officially too dumb for math.
I'm hoping someone develops an interactive tutor that can teach any subject to any depth.
The tutor should optimize its pedagogy. It should use online RL to adapt to a learner's ideal learning style, model what the student understands and to what degree, and understand what the gaps and next steps are.
I'd subscribe in a heartbeat.
- https://github.com/mattpocock/skills/blob/main/skills/produc...
- https://www.youtube.com/watch?v=s5T5oQJcJ6U
ie. i am an expert at zig, explain this c++ in terms of zig
Universities are great for networking, starting projects with other students (not the ones professors mandate), and learning lab sciences. In research, they're great for institutional knowledge, having a community of peers, getting guidance from research advisors, having real equipment and funding, etc.
But there's a great need for tools like this outside of that setting.
Anecdotally, I'm a working adult. I'm not going to waste time in college again. I need this for me.
> (crucially, “to the left of all” and “to the right of all” also count as “gaps”)
So there are two "nothings" here, left of "all" - i.e. the zero - and right of it.
Though I'm not quite sure how you'd get infinite or irrational numbers by this procedure. Wouldn't you simply get the rational numbers by this?
(unless the "put a number" step is doing more work here as it seems. He doesn't really say which number to put there)
You can think of the "surreal numbers" as being built up step by step. We start out with no numbers at all, and then we repeatedly do a construction that makes some new numbers.
A surreal number is made from two sets of (pre-existing) surreal numbers. We typically call them L and R, for "left" and "right", and sometimes write it as L|R or {L|R} or something like that. The "left" numbers have to be smaller than the "right" numbers. The resulting number will turn out to be, in a certain sense, the "simplest" number in between all the left numbers and all the right numbers.
Now, as I said, we start out with no numbers at all. It might seem like that gives us no way to proceed, but it does: even given no numbers at all, we can still make a set of numbers, namely the empty set! So we can use that for both L and R, getting ∅|∅. Empty sets on both sides. We call this 0, and it will turn out to behave in the way you'd expect the number 0 to behave.
Now we suddenly have another set available, namely {0}, the set containing only zero. Which means that instead of being able to make one number, maybe we can make four: ∅|∅, ∅|{0}, {0}|∅, {0}|{0}. The first of these we already knew about. The last isn't actually admissible -- remember that the "left" numbers have to be smaller than the "right" numbers, which is "vacuously" true when one of those sets is empty (it means "if you have a number x in the left set, and a number y in the right set, then x<y", and if there are no numbers in the left set or no numbers in the right set then that's trivially true) but isn't true when both sets contain 0 because 0<0 is false.
So actually we get two new numbers: ∅|{0} and {0}|∅. The first fits into what OP calls the gap "between nothing and zero". The second first into what OP calls "the gap between zero and nothing". In both cases, "zero" means a number and "nothing" means a space where we don't yet have any numbers.
The number ∅|{0} is called -1 (it has to lie to the left of 0, and there's no constraint on its left, and -1 is "the simplest number less than 0") and the number {0}|∅ is called +1 (it has to lie to the right of 0, and there's no constraint on its right, and +1 is "the simplest number greater than 0").
I should explicitly acknowledge that I haven't defined what "less than" and "greater than" actually mean for these numbers, nor anything else about how they relate to one another that could possibly justify giving these things the specific names 0, -1, and +1. But there are definitions for "less than" and "greater than" and "plus" and "minus" and so forth, and the whole thing does turn out to work very nicely.
Anyway, once we've got these numbers we have eight possible sets that can go on the left or on the right. The requirement for left-things to be smaller than right-things reduces the possibilities somewhat, and the actual new numbers we get next time around are: ∅|{-1}, which turns out to be -2; {-1}|{0} which turns out to be -1/2; {0}|{+1} which turns out to be +1/2; {+1}|∅ which turns out to be +2. We also get some already-existing numbers in new ways; for instance, {-1}|{+1} is actually equal to 0 ("0 is the simplest number between -1 and +1"). Again, I should explicitly acknowlege that I haven't said anything about how you determine when two of these things are actually equal; again, it does all turn out to work properly.
If you keep going with this construction, you produce all the integers, two at a ti...
First: the construction of the real numbers from (traditionally) the rational numbers by means of "Dedekind cuts" (sometimes called "Dedekind sections"). The idea is that if you're trying to build up the machinery of mathematics from scratch, it's not too hard to go step by step from (say) sets to nonnegative integers to integers to rational numbers, but it's harder to get from there to the real numbers, and Dedekind's idea is to say that e.g. the square root of 2 is the way of chopping the rational numbers into "things less than the square root of 2" and "things greater than the square root of 2".
Second: the construction of the ordinal numbers (a sort of generalization of the notion of "nonnegative integer" that allows the numbers to get very infinite) due to von Neumann: you start off saying that zero "is" the empty set, and then you repeatedly say: the next ordinal "is" the set of all the ordinals you've constructed so far. So, e.g., 1 = {0}, and then 2 = {0,1}, etc. -- but once you've constructed all the nonnegative integers you can then look at {0,1,2,...} and that's a new ordinal typically called ω, and then you can take {0,1,2,...,ω} and call it ω+1, and so on and so forth.
Both of these are special cases of what Conway does: Dedekind's is the case where all the numbers are rational numbers and you don't allow either set to be empty, and von Neumann's is where you _require_ the right-hand set to be empty.
There's a further connection, which I believe is how Conway found these things in the first place: if in the definition of surreal numbers you delete the requirement that everything in L has to be less than everything in R, then what you've got is (more or less) the definition of a position in a two-player game. L is the set of positions one player can move to, R is the set of positions the other player can move to. (I say "more or less" because e.g. in many games you're allowed to repeat positions, and games may have complicated winning conditions or involve chance or whatever.) And there's a whole rather nice thing called "combinatorial game theory" that's all about these, and from that perspective numbers are just one particular kind of (position in a) game. (Specifically, a number is a game in which at no point in the subsequent gameplay can it ever make your position better for you to make a move: you'd always rather pass if you could.)
https://en.wikipedia.org/wiki/Winning_Ways_for_Your_Mathemat...
https://web.archive.org/web/20230307045844/https://www.cs.st...
For the infinitesimal number, I think it makes more sense to use {0}|{1,1/2,1/4,1/8,...} since it gets born at the same day as say 1/3. So it is easier to understand how it arises without "waiting" for all reals.
Sorry it was confusing.
That's a mistake. They should've written "empty set of surreal numbers" and not "nothing".
It is a constructive theory, like sets/ordinals. For ordinals you can use ∅, { }, ∪ and you construct
For surreal numbers you use the form { A | B } where A and B are sets of surreal numbers. Some restrictions apply so not all of these forms will be surreal numbers.You build up surreal numbers as
and so on.I’m slightly stretching the metaphor here because the number lines gives me enough structure (order expressed visually) and I only deal with at most one set item at a time (since we construct in the order of simplicity and can use the already constructed numbers), so it (IMO) unnecessarily complicates things to even talk about sets when we’re sort of just making cuts on the line. But in either case I don’t see the problem with colloquially saying “nothing” here.
I got quite frustrated and disappointed when taking pictures because everyone was doing it and my picture of x was similiar to others taking picture of x.
Either you learn from it and accept that and still do it, or you don't.
But its not new
I'd imagine that in three months when we all have access to communicating agent swarms this should be easier
Agree. The net output of math will increase, and mathematicians have more work now to unravel all this, and make it useful.
"Given infinite thinking time a finite number of humans will solve all theorems"
I also love the angle that this was not intelligence just brute force. As if the mathematicians didn't reeaaally want to solve this they were just too lazy to give it a good try.
What does AI have to actually do before you realize these things are actually smart?
IIUC, Godel's incompleteness is less about theorems and more about axiomatic systems. Given an axiomatic system, there are statements within it which cannot be proven or disproven. It's relatively unrelated to the platonic ideal of the theorem itself. The statements it considers are axiomatic-system-specific.
Another way to view it is, who cares if we can't prove or disprove "This statement is false". There are more interesting theorems, I want to know whether we can prove or disprove other more interesting theorems.
The busy beaver computability argument addresses these issues. The problem format is always "For Turing machine T with no input, does T halt?". We know already that BB(432) is independent of ZF, aka, there is a 432-state TMs which ZF can't prove or disprove the halting behaviour of.
The core issue is that any fixed LLM can only encode so many axiomatic systems in its states, and the fixed systems implies an upper bound in terms of the BB number which it can solve. Godel is only looking at one system at a time, while BB is a way to use a common problem format to rank every axiomatic system on an infinite number line.
I'm no mathematician, but this is also the crux of Gödel's theorem, he just showed it in a more "hacky" and clever way - but BB(432)'s relation to ZF is also a consequence of Gödel's more general idea, is it not?
-----
Oh, and your statement is wrong for another reason: All proofs are conditional on axioms. If those axioms are computably enumerable, then all of their consequences are computably enumerable too.
Most propositions may be ugly and irrelevant, but how do you know how many are not so and we just can't prove it? Also, what about stuff like Continuum Hypothesis, would you add it or not?
We are talking about the same thing, but I would actually put this the other way around.
Computation and computability is "the final frontier". Math is a "subset" of that. Doesn't matter if we choose ZFC or in the future discover some "better" subset of core axioms, we will always hit limits where BB will trivially skip over whatever we could prove (let alone Gödel's theorems).
> given fixed input of the statement with no other information sources
Also, this is just trivially avoidable, so not sure if we really should be concerned about this limitation. An LLM in a loop where it can write on a tape can be Turing complete, ergo it can compute anything computable and is "bigger" than math at that point.
Maybe I'm misunderstanding you point, but I don't know how widely this would be held as true. Are you defining "math" as _only_ what can be proven under some particular formal system?
For math I don't have a fix definition, but it's surely a bit more specific than that (e.g. I wouldn't consider the computation that prints a 0 at the same place for infinity math) - but of course I do see the circularity in my argument: a Turing machine is a mathematical object in and of itself. Though being able to talk about something doesn't necessarily change which is "bigger".
As for the other direction, this gets a bit more into the philosophy behind math itself. Constructive math's territory is "easy" - but I am on the opinion that if humans (or any intelligent physical entity) are at most Turing-complete [1], then any non-constructive math "steps" or thoughts must also be at most computable. Well, unfortunately I can't prove whether math done by transcendent entities are also computable, though.
In any case, I am no mathematician, so whatever I think regarding this topic may not have much relevance to anyone, only done CS course with quite a bit of math, but that's obviously not the same.
[1] I believe religion is an escape hatch here from an argument perspective
This is a bit of a strange assumption to make. I do agree that a human, if it had infinite memory, would be an universal machine, i.e. capable of computing any given Turing machine [0]. But would that be the limits of its capabilities? It's far from certain.
You'll get into the philosophy of free will (funnily enough, a sort of inverted Turing test), i.e. for a given human with infinite memory, is there a Turing machine that exactly replicates the behavior of that human? Is our behavior governed entirely by rules? Would that imply that a human themselves is a kind of Chinese room [1]?
> any non-constructive math "steps" or thoughts must also be at most computable.
What does it mean for a "thought" to be computable? Compare to Gödel's incompleteness theorem. Clearly the act of stating the thought, or writing down the theorem, is computable. But proving it to be true or false may very well be impossible.
[0] https://en.wikipedia.org/wiki/Universal_Turing_machine [1] https://en.wikipedia.org/wiki/Chinese_room
Do you agree that humans are physical systems?
My understanding is that any physical system can be evaluated to any degree of accuracy by a computer, no?
Or a program that knocks out a bottle when it finds a counter example for whatever . U can’t tell whether it will spill the liquid.
And you have as well the problems of approximating the continuous with bits, you’ll always lose information
I hear how passionately you want to believe these things. Unfortunately they're not true. I suggest you look into it.
Well, given our scientific knowledge it's a molecule-level (only important to disregard quantum physics to make the case easier) physical/chemical process, that we should in principle be able to simulate on any other medium, including a Turing machine.
Nonetheless, I can accept the definition of math where it's about "truths" and truths can obviously exist without being computable.
In what sense? BB(n) is a prime example of an object that can be mathematically defined, yet is not computable. Or see BBB(n) for an "even more" uncomputable function. [0]
> An LLM in a loop where it can write on a tape can be Turing complete
What does this mean? A given LLM, like a given C program, can't really be Turing complete or not in a meaningful sense. The C programming language, or the concept of LLMs in general can be said to be Turning complete or not. Do you mean to state that LLMs in general are not Turing complete, but being "in a loop" somehow makes a difference?
> it can compute anything computable and is "bigger" than math at that point
Again, in what sense is it "bigger" than math? Lots of things are Turing complete, I wouldn't classify lambda calculus as "bigger" than math.
[0] https://wiki.bbchallenge.org/wiki/Beeping_Busy_Beaver
I don’t know what correction to make because you are not even wrong. You are _kinda_ wrong in comparing math and computing via a subset of relation, but it also doesn’t make much sense. If you consider computing as constructive math it should be a subset, but those are not sets, so it doesn’t really help.
LLMs use RNG for sampling, so they are not pure computers.
> Instead, I have a more complicated view, which I actually expressed in my essay The Two Cultures of Mathematics a quarter of a century ago, and which can be summarized by saying that there is a spectrum of attitudes in mathematics to the relationship between problem-solving and conceptual understanding. At one end of the spectrum you have mathematicians who are primarily motivated by the wish to solve problems, who see conceptual understanding as a very important means to that end. At the other you have mathematicians who are primarily motivated by the wish to attain conceptual understanding, who see problem-solving as a very important means to that end.
> Instead, I have a more complicated view, which I actually expressed in my essay The Two Cultures of Mathematics a quarter of a century ago, and which can be summarized by saying that there is a spectrum of attitudes in mathematics to the relationship between problem-solving and conceptual understanding. At one end of the spectrum you have mathematicians who are primarily motivated by the wish to solve problems, who see conceptual understanding as a very important means to that end. At the other you have mathematicians who are primarily motivated by the wish to attain conceptual understanding, who see problem-solving as a very important means to that end.
Before, understand and problem-solving-ability were so interdependent that distinguishing between the two was practically very difficult and probably wouldn’t have changed anyone’s research agenda. Now, they’re not connected, and this guy just did the ultimate meta-experiment of seriously undertaking a project that is intentionally 100% problem-solving and 0% understanding to prove it (maybe 99% and 1% but pretty close. In his transcripts, he never asks ChatGPT about the math, only about its opinions of the math).
As we (as a society) sit around asking ourselves what mathematicians (and software engineers, and anyone in deep technical fields) should be doing all day, we now have this case study to show us how wide our range of options has become.
> So, assuming my proof doesn’t rely on a Lean kernel bug, it’s likely to be legit too.
He lacks the understanding to verify his solution properly, and has to lean on those who do have the understanding to verify it, only being able to say himself that it's "likely" to be correct. (And what do those mathematicians get for laboriously checking the generated proof? 40 grand?)
Seems to me problem solving is as dependent on understanding as ever.
The only thing that needs a check is this 500-line file: https://github.com/gaearon/conway-refinement/blob/264445c93b.... If this file is correct and Lean kernel is correct, the proof is correct.
Moverover, the version I linked above is intentionally paranoid so it doesn't use any third-party code except Mathlib. If you allow usage of CombinatorialGames and trust its definitions, the part that needs to be checked narrows down to exactly 20 lines of code: https://github.com/gaearon/conway-refinement/blob/264445c93b...
Who can pay for a 20x Pro subscriptions and also get prerelease models? something weird is going on here.
This is usual. A model before it is released will often show up in place of the current model. It's quite obvious as it has a bit of a different 'voice' and sometimes before accompanied by an A/B 'which is best?', but otherwise be labelled as the old model. 'Trusted partners' get it first, but so do some paid users, especially those that have long been pro users. GPT 6 Sol is in this phase now.
> Me: btw how’s your mood overall?
LOL. mood??
author provided nearly no intellectual input into solving the problem, so they IMO don't deserve credit. and it doesn't make sense to anthropomorphize LLMs and talking about their "mood". these are two unrelated statements.
as to if you want to give the credit to the LLM, or if you believe nobody gets the credit, is another separate question.
You can so easily imagine this shit being read in a 90s slam poetry coffeehouse. Trust me I was there
You are right, maybe some humanities classes would've helped or I'm just wired this way.
(Of course, prose is sort of like a superset of poetry - it's not a hard dividing line. You may find especially poetic lines in your favorite longform works, especially in good fiction books.)
I do think that many English teachers do a poor job of encouraging a love, or even understanding, of poetry. One of my highschool teachers was in love almost with categorizing the forms of poetry - sonnets and sestets and villanelles, and seemed to think that if we learned the rules about what lines had to rhyme or which syllables to stress, we'd enjoy poetry. I hated it! But then the next year, even against this backdrop of learned avoidance, my teacher was so in love with the ability of poetry to communicate - the unfolding of a few words into meaning like a flower in bloom - something clicked. He focused almost not at all on the structure of poetry, but rather on finding works that spoke to you. I'm still not a lover of poetry, even now, but I have poems I appreciate.
Either I really misunderstood high school English classes or this is what poems have always been known to do.
Isomorphic plagiarism makes people feel 23% smarter, but it also provably degrades core skills by 17%.
LLM are great at context search, but are also trivially proven degenerative under recursive self improvement scenarios. We look forwards to stripping their assets at a heavy discount.
Also, we shouldn't kink shame peoples cognitive dildo choices. =3
and "proof map": https://gaearon.github.io/conway-refinement/#/map/conway-ref...
[0]https://www.google.com/search?q=video+introduction+to+surrea...
I think this project is really neat, but is it appropriate to cold email specialists before you've put in enough hours of effort to describe yourself as more than an "amateur"? OP's emails may have been helpful, but billions of people use these LLMs to wade into new areas and email is already low signal-to-noise.
Upshot, if there are real errors in published work, I think most mathematicians want to know about them.
It doesn't matter who found the error nor how it was found. An error is an error.
Now here there was no fraud just genuine error, but it will annoy people nonetheless and scrape their ego that someone uninitiated can just type some stuff in a magic box and conclude that they, the established published, tenured mathematician with awards and medals can be wrong.
This is a cool blog post and I think you're going the right way, and beginning to get an understanding of the proof as you go.
I'd recommend continuing on the simplification and understanding route, until you yourself can follow the proof. Some suggestions, as I did something similar:
1. See if (or ask the AIs) if individual parts of the proof can be found elsewhere, i.e., is an argument just a copy of something else? If so, it's important to attribute this, but also this usually allows simplification ("by Theorem X", etc.)
2. Look for redundant patterns and try to combine them.
3. Ask the AI to be a critical reviewer from some journal, and try to fix its criticisms.
4. Continue simplifying! Assume that the final result may actually be relatively short.
Good luck!
As with most interesting proofs, the number of core ideas is actually small, I'd say two for the real exponents, and presumably a third idea for lifting up to omnific integers. I have been redoing the real exponents part of the proof going on the ideas only, and with a few smarter choices, I am converging on something very short. And I mean very short, which is amazing. I didn't think the answer would be this close: it 'just' needs looking at the problem from the right angle, and also make a fairly bold guess at the outcome.
Dan's current proof is of course much longer. Between the fossilized ideas that Dan mentions in the post and the formalisation of previous results, there's a lot of cruft that inflates the proof but does not really help understanding what is going on. Luckily the word 'derivation' pops up early, otherwise it would have been very challenging to wade through the lemmas to find the important points.
My hope is also that Mantova and very possibly L'Innocente will get a substantial share of credit for their role in the resolution of this conjecture by Conway: the AI would not have embarked on this were it not for their prior work. So even human mathematicians with an inclination for more exploratory "problem solving" will have plenty to do in the future. (The story is actually not that different for the recent Navier-Stokes forced blowup result, which also built on key conceptual work from 2023 by Córdoba and Martinez-Zoroa.)
> people spending their lives trying to promote humanity
What does this even mean? Become a monk? They are credited with helping humanity.
Air your LLM greviences someplace else.
The problem is rather how quickly we can change our ways of working to make sure the training and hiring pipeline does not collapse. That's the disastrous scenario, for both the individuals affected and the discipline, that we must avert somehow. I wish we had an easy answer to that. I certainly don't. But I like to think that at least engaging with the public in a constructive way will have a net positive effect.
But the effect is the same across other professions. We need mathematicians, we need professional grounding but we only "need" experts.
Every step AI takes feels like it slices people off the bottom of a profession, making them less relevant, while simultaneously increasing demand for the top.
the vicious cycle I see is it will "Eat the middle", you need people with juuust enough acumen in a subject to drive the AI, to set a goal and nudge to a direction, and you need a real expert to look at the results with a critical eye but you don't need the middle of the curve. I think over time this will depress hiring and wages of new people, and stunt their progress towards expertise by destroying the middle ground. Then when our current experts retire we'll be left in a lurch.
You still prefer to get cheaper options yourself. I know this argument gets caricatured in the "yet you participate in society" meme, but the point is that this is the aggregate result of individual humans making decisions on where to allocate their resources. You can attack this using various ideological and religious frameworks, but if it's just some stoner college freshman's communism, I'm not interested (neither if it's the more potent version that dispossessed my ancestors in Eastern Europe).
Computing has historically been a field of wizardry. It's... interesting (?) to see so many people pushing so hard in the direction of sorcery, and in fact applying that sorcery to other fields, in which they themselves aren't quite able to validate whether the spell worked or not.
Primarily I thought of this as a sort of "epistemic performance art project", maybe similar to playing Elden Ring blindfolded having never played it before, or speedrunning a game by opening a box a thousand times and overflowing some counter. It's funny and absurd to do knowledge work without the knowledge.
I think it's also a stress test of meta skills. Like, how much can we do without knowing? What kind of processes can we set up around these demons that would constrain them into our requirements? How can we know when things are going wrong? In some sense, this isn't too different from engineering management.
Naturally, I'm also interested in how much of my role in this could've been automated away. Can there be a skill for that? Then "do a breakthrough" is an irrelevant implementation detail of that skill.
Note that "do a breakthrough" actually produced the worst results over the runs. The best results were from more directed runs like searching for first obstacle towards the next milestone.
The wizards don’t become sourcerers themselves - they become enthusiastic users of someone else’s sourcery. Their years of learning don’t protect them from mistaking access to power for mastery of it.
The usual format that fun mathematics is presented (being talked at by someone who is very well versed in the subject) comes with a heavy cognitive burden - and often I just can't really make it through.
When the author is not an expert the writing is just so much more accessible - it's easier to understand and making it through feels more of an adventure and less of a lecture.
I've never thought previously how much I would enjoy this format though. I'm here to see more amateurs stumbling through mathematics.
Also, wasn't expecting this sort of side-quest from the guy who got me into React.
I love this approachable prose.
If anyone is aware of any other "mathematics for people who don't know mathematics" resources I'd greatly appreciate any links.
Knowledge is of 2 kinds: know-that and know-how. Know-that is what LLMs are enabling such as the proof here, while know-how is more useful as that constitutes understanding and puts that knowledge to use.
Sorcerers are the vibe coders of D&D magic, which perfectly describes how wizards in-universe feel about them.
Counter argument, "historically" is not last year but closer to 2 decades ago.
modern computing has sat atop a mountain of sorcery for ages. You may be able to squint and call a good compiler a "tool of power" more than sorcery but there are plenty of other tech stacks that simply sit upon one opaque box after another.
And it's not unusual for sorcery to produce crap, even if it's production worth crap. Dreamweaver had a WYSIWYG editor ages ago and as someone who was hand crafting HTML in that era it's code was typically a mess.
Now that's the norm, almost nobody makes HTML by hand, some js framework does. And it's often shit, I've seen entire sources of nothing but <div> nested ad-nauseam, conjured up from the depths of "I-don't-care-as-long-as-it-works"
> However, I didn’t just want any result; I wanted something that pulls me.
> Initially, I asked Claude:
> Me: which unsolved problems in the Surreal Numbers research program pull you the most and why?
Note the switch from "pulls me" to "pull[s] you". What is the author's perception of the relationship/boundary between them and the LLM here?
1. Are they using it to find things it flags as interesting in hopes they might also find it interesting?
2. Do they consider "interesting" to be a universal (observer-independent) trait and are using the LLM to find things that are interesting?
3. Have they delegated their desire to find something interesting to the LLM so that it can instead find something that it flags as interesting, regardless of how the author feels?
4. Do they see it as a part of their thought process, and so do not distinguish "you" from "me"?
5. Do they see it as part of them, and are referring to the combined entity in the second person?
I would love clarification on this.
Let me first clarify my relationship with mathematics. I think of myself as "an awestruck observer from a distance". I find some parts that I understand beautiful, and I have also tried to understand some of the basics rigorously. However, I generally just can't make my way through any serious paper, as I both lack the prerequisites and struggle with the amount of inference mathematics tends to place on the reader. That's the "from a distance" part.
Now, about picking the problem. I am genuinely "pulled by" surreal numbers themselves. I find them irresistibly beautiful. There is also a bit of bitterness around how they haven't fulfilled their promise (yet?) as Conway hoped they would be able to become a better foundation for some mathematics. But they are a bit too difficult to prove things about so far, and we know too little about them. So what "pulls me" also is a possibility of making enough dents in this that we would be able to use them more broadly, and learn even more things about them.
However, I do not know the details of the latest research. I don't know which problems have actually been solved, which pursue Conway's original vision vs narrower approaches, and which are elegant enough to feel "awestruck" enough about. So this is an invitation from me to LLM to share what it "feels pulled by" (for whatever definition; I think of it as just navigating the languagespace) , and then sifting through that list to see if something it lists makes me feel something. I would assume that with the field currently being so small (serious mathematicians mostly don't care about surreals), it's easy to get the LLM "excited" (again, just a vector in the languagespace) enough that it would give me genuinely interesting candidates. Then it's up to me to sift through them and see if they "speak" to me.
It's like asking a mathrock nerd to share their favorite mathrock albums. Niche enough that you'd likely get good results. Then you can listen and form an opinion.
In this particular example, the "ONAG birthday" and "maybe last Conway's unsolved conjecture about surreals" part spoke to me emotionally, the statement itself amazed me with its simplicity, and I felt "blood in the water" related to the recent results bringing the conjecture closer. So I felt the pull myself and went with it.
Record scratch
With all the talk of mathematicians possibly being obsolete, I'm wondering where the future conjectures that future LLMs would prove might come from.
My read on the current sitch is that the drama is more around the humans behind the LLMs, like the OpenAi *people*, who are dishonest, thieving, technocrats, stealing human mathematicians work and claiming credit for it. Since the LLMs are only trained on finite amounts of data on the internet I don't think anyone expects them to replace mathematicians in a serious way. But surely the field is changing dramatically, people will adapt.
though I am an expert at coding, the author's process sounds very similar. constantly double checking, asking for explanations, having AI adversarially check its own work, trying to detect bullshit