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.
Heh, I like this. but it should be pointed out that from the other point of view, software developers were the supernatural beings (dare I say demons), which the sorcery of a good project manager could tame (with more or less success) to perform the desired magical effect
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?
(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.
> In either case I believe people who can put AI to the most value are the mathematicians themselves
The net output of math will increase, and mathematicians have more work now to unravel all this, and make it useful. AI plays the role of a monkey in the infinite monkey theorem [1]. We now need an LLM corollary - Something like: A finite number of LLM agents will almost surely find all theorems given an infinite token budget.
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.
For any finite program (eg some LLMs), there is a true math theorem which they cannot prove or disprove (given fixed input of the statement with no other information sources). If that weren’t true, BB would be computable.
Math is beyond computation. Since AI is just bits in bits out, it has this fundamental limitation.
Any magic of AI systems comes from the transformed meaning of its input data. With fixed weights any LLM is just an artifact. For example a human prompting an LLM constitutes an extra information source, which removes the above limitations. In theory any input from the natural world would remove the limitations too. The natural world is a black box and we don't know what kind of meaning or intelligence could underly it.
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". Ok, the axiomatic system is incomplete; fine. What's important is can the system prove a real theorem that I care about.
The busy beaver computability argument addresses these issues. The problem format is always "For Turing machine T with no input, does T halt?". This format can encode many math problems. And 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.
So BB looks at real theorems, ranks them, and we can ask what axiomatic systems can solve them or not. Godel looks at 1 axiomatic system and produces a toy theorem which the system can't solve. That's an extremely important difference!
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.
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.
"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?
Machines have a much higher capacity for work than human beings. Saying that these proofs did not require equivelant intelligence, but benefitted from sheer volume, does not strike me as unreasonable.
It feels goalpost-movey to downplay exploring a large search space efficiently in regards to "intelligence". If we dug into a human genius's brain and found it was somehow trying out a million ways to solve a a problem at once, no one would seriously suggest the person isn't actually intelligent.
And our brains must something like that at some physical level. You can't have a "turtles all the way down" of reasoning - the building blocks must be simpler. It must reduce to something like pathfinding and brute force at some point, weighted by factors in the system and maybe some randomness.
We have a romantic view of intelligence, perhaps stemming from intuition within the context of scientific discovery. Given enough intelligence, and enough context, a brilliant person can have a stroke of inspiration that allows them to make a major leap (a-la General Relativity or Fermats last theorem). We haven't seen THAT same capacity from a machine, but we see the more ordinary, unsexy grinding type of progress that represents 99.9% of scientific reality.
Is there truly anything new under the sun? Hasn't all of existence alway been here? All math, all physics? We could have merely discovered it. Intuition might be nothing more than combinations of what already exists rather than some sort of divine insight that unlocks previously unknowable mysteries.
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".
For undecidable theories, there is no computable function bounding this blowup from theorem length to proof length (otherwise, the theory would be decidable.)
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.)
> 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 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 time, and also all the "dyadic rationals", meaning fractions where the denominator is a power of 2. And then, once you've got all those, at the next stage of construction you abruptly get all the real numbers -- e.g., the square root of 2 is L|R where L = {dyadic rational numbers that are negative or have a square smaller than 2} and R = {dyadic rational numbers that are positive and have a square larger than 2} -- and you also get {0,1,2,3,4,...}|∅, conventionally written as a lower-case Greek letter omega, which is an infinite number, larger than all the integers. (And its negation.) And {0}|{1,1/2,1/3,1/4,...} which is an infinitesimal number, positive but smaller than any ratio of positive integers. And you can then proceed further and construct a vast infinitude of numbers, including all the real numbers (which we've already made) and all of the so-called infinite ordinals (which you can kinda think of as being a sort of "infinite positive integer", though there's more to them than that) and much more, all in a system that lets you do arithmetic and suchlike. It's very elegant, if your brain has been twisted into the mathematician-y shape that finds such things elegant.
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
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.
This would make a lot more sense to me if "nothing" and "nothing" were instead "-inf" and "+inf"
Some other comments clarify that "nothing" is more accurately "the empty set". This is helpful because at first I wrongly synonomized "nothing" with zero. But now I get tripped up on the "between" language. Maybe it's a lack of background in sets, but I don't know what "between" implies for an integer (zero) and a set (the empty set).
I didn't want to introduce the notion of infinity because there are actual "infinite numbers" on the surreal number line. I've kind of tried to have both the simplicity of set-theoretic definition and the intuition of the number line, and slightly bungled the exposition. I hope the newly added diagram helps.
I'm not a mathematician and "nothing" doesn't really make sense for me either. But I guess the problem with inf might be that it'd be strange to get +2 as the next thing between +1 and +inf, while getting +1.5 between +1 and +2.
It's more that surreal numbers already include infinities like ω, ω + 1, and so on, so "inf" felt like a concept I want to avoid. The actual description is set-theoretic and uses empty sets there ("nothing to the left", "nothing to the right") so I took that a bit too literally.
Wow thanks. I'm a mathematician and also got lost at the step. This illustration makes the construction much more clear. The text isn't really describing this process well
I think it's just we don't have a way to say/write these numbers. So you make up a way to write them (-1 and 1) and continue.
The numbers don't matter and you could replace -1 and 1 with anything. It's just easier to begin your new fake number at - 1 and 1. Because position does matter.
Basically what I take away is that we're inventing a new number system from scratch. So we're not "proving" that 1 is a number between 0 and the empty set. We're defining it as such, and it just so happens that a number system defined this way works out in convergent ways with other mathematics.
There has to be some procedure how to come up with "new" numbers though, if you want to have more in the end than just a fancy binary tree - in particular if you want to map your "fake numbers" to the reals, infinity, etc.
This procedure is enough. If you define addition and other operations in a certain way (as Conway did), it turns out that on the omega-th day (i.e. after initial infinite steps), all reals will be born.
I think he just wrote it in a confusing way. The quote before says:
> (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 than it seems. He doesn't really say which number to put there. In the examples, he mostly did "new number = (left number + right number) / 2", with special cases if any number is "nothing" - but he never actually wrote what the rules are here.)
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.
(Apparently I was extremely unclear with this text. For clarity: if you want to actually understand surreal numbers, go and read On Numbers and Games, by Conway, which is a delightful book; or get an LLM to talk you through Wikipedia. Original text follows.)
It’s a terrible explanation. A surreal number is defined as a pair of sets of surreal numbers (where you fiddle around the recursion in that definition by defining them in waves, so strictly speaking you’re defining “the surreal numbers born at time T” for each individual T given access to the surreal numbers born at all earlier times, and then you “take the union across all times”, scare quotes because there are too many times for this to result in a set). Zero is a surreal number but the LLM is using the word “zero” to mean “the set containing just the surreal number 0”; “nothing” here is the LLM’s obtuse word for the empty set. Wikipedia may actually be easier to follow.
I mean, I was intending to supply the words that would link the LLM’s explanation to a more normal one, not to explain it; apparently that was extremely unclear. An actual explanation is much longer, as indeed I attempted to indicate by pointing to Wikipedia and saying that it might be more clear.
“Doing better than a totally useless explanation in fewer characters” is in general impossible, of course, eg if the first explanation has only one character.
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, and slow. There's a huge amount of room for improvement.
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 AI tools to accelerate learning 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.
Plot twist: they were both sold on early investment in companies that survived the .com bust. Now they’re VCs that everybody worships as business geniuses even though they’re just lucky idiots, and the sycophantic chatbots finally let them feel as smart as everyone says they are, and a whole bunch of hype-drunk fans are feeding into it.
The Claude output in the first one-shot counterexample attempt is hilarious. I hate its writing most of the time but this stuff is next level deep-fried slop.
> And the control column confirms the resonance-necessity conjecture empirically: break the skeleton alignment and the joint kernel dies at the constrained window, exactly as the transversality heuristic predicted.
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 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.
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
> 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, understanding 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...
What is your point, exactly? Increasing number of people working in and around mathematics are relying on Lean kernel's correctness. That's kind of the point of tools like Lean. Why is it a problem for me to publish a result that relies on it? How do you think other Lean proofs work?
My point is what I said. Without understanding you are only able to say your proof is "likely" to be correct. It's clear from your writing that you understand that your proof will only be accepted once thoroughly reviewed by human mathematicians, who will certainly not be just verifying the definition. Bugs in Lean exist (you're a programmer and it's a program, why would you assume they don't?) and reward hacking and finding bugs are both well established LLM behaviours.
> Why is it a problem for me to publish a result that relies on it?
Bit over-sensitive here. I never said it was a problem for you to publish a result. You can do what you like on your blog and spend your tokens however you choose, just as I'm free to have my own opinions on the value of such an effort. I was responding to, and disputing, a commenter's assertion that understanding and problem-solving ability are "now ... not connected".
While Lean is tightening things up after the recent LLM-driven hacks, I agree that bugs are possible. Although usually code that exploits them is obviously aggressive and is deliberately using the more obscure features related to metaprogramming. Also note that my solution has passed the nanoda kernel as well (https://palomar-registry.org/entry?id=PALOMAR-2026-09-03-000...).
That said, again, I never implied that I'm asking mathematicians to "laboriously checking the generated proof" which is what your parent comment says. The value to mathematicians is knowing that the conjecture is probably right, and knowing the rough path the LLM has taken to it. Instead of checking the Lean proof line by line, what mathematicians are interested in doing (at least, the ones I've been in contact with) is finding a shorter and more direct proof now that they're aware of the outline and main intermediate claims. As for how much value they find in that, I presume they would be able to speak to that when/if they would like to make their research public.
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
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 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.
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?
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.
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.
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.
Several of my coworkers — it’s not that unusual that if you can max out a couple accounts, the companies will obviously notice you (as a high cost customer), and sometimes offer more
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.
Heh, I like this. but it should be pointed out that from the other point of view, software developers were the supernatural beings (dare I say demons), which the sorcery of a good project manager could tame (with more or less success) to perform the desired magical effect
All this time, I've been considering myself the warlock. When, in fact, I've simply been the Imp. Dastardly news.
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?
I would love clarification on this.
(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.
Good luck!
> In either case I believe people who can put AI to the most value are the mathematicians themselves
The net output of math will increase, and mathematicians have more work now to unravel all this, and make it useful. AI plays the role of a monkey in the infinite monkey theorem [1]. We now need an LLM corollary - Something like: A finite number of LLM agents will almost surely find all theorems given an infinite token budget.
[1] https://en.wikipedia.org/wiki/Infinite_monkey_theorem
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.
For any finite program (eg some LLMs), there is a true math theorem which they cannot prove or disprove (given fixed input of the statement with no other information sources). If that weren’t true, BB would be computable.
Math is beyond computation. Since AI is just bits in bits out, it has this fundamental limitation.
Any magic of AI systems comes from the transformed meaning of its input data. With fixed weights any LLM is just an artifact. For example a human prompting an LLM constitutes an extra information source, which removes the above limitations. In theory any input from the natural world would remove the limitations too. The natural world is a black box and we don't know what kind of meaning or intelligence could underly it.
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". Ok, the axiomatic system is incomplete; fine. What's important is can the system prove a real theorem that I care about.
The busy beaver computability argument addresses these issues. The problem format is always "For Turing machine T with no input, does T halt?". This format can encode many math problems. And 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.
So BB looks at real theorems, ranks them, and we can ask what axiomatic systems can solve them or not. Godel looks at 1 axiomatic system and produces a toy theorem which the system can't solve. That's an extremely important difference!
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.
Pretty sure Gödel’s theorems imply the halting problem if you squint hard enough.
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.
lol same with people.
"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?
Machines have a much higher capacity for work than human beings. Saying that these proofs did not require equivelant intelligence, but benefitted from sheer volume, does not strike me as unreasonable.
It feels goalpost-movey to downplay exploring a large search space efficiently in regards to "intelligence". If we dug into a human genius's brain and found it was somehow trying out a million ways to solve a a problem at once, no one would seriously suggest the person isn't actually intelligent.
And our brains must something like that at some physical level. You can't have a "turtles all the way down" of reasoning - the building blocks must be simpler. It must reduce to something like pathfinding and brute force at some point, weighted by factors in the system and maybe some randomness.
We have a romantic view of intelligence, perhaps stemming from intuition within the context of scientific discovery. Given enough intelligence, and enough context, a brilliant person can have a stroke of inspiration that allows them to make a major leap (a-la General Relativity or Fermats last theorem). We haven't seen THAT same capacity from a machine, but we see the more ordinary, unsexy grinding type of progress that represents 99.9% of scientific reality.
Is there truly anything new under the sun? Hasn't all of existence alway been here? All math, all physics? We could have merely discovered it. Intuition might be nothing more than combinations of what already exists rather than some sort of divine insight that unlocks previously unknowable mysteries.
This isn't necessarily true. There may be proofs so complex, they could exceed the limit of human cognition.
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".
For undecidable theories, there is no computable function bounding this blowup from theorem length to proof length (otherwise, the theory would be decidable.)
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.
[0]https://www.google.com/search?q=video+introduction+to+surrea...
https://www.youtube.com/watch?v=ZYj4NkeGPdM
>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.)
> 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 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 time, and also all the "dyadic rationals", meaning fractions where the denominator is a power of 2. And then, once you've got all those, at the next stage of construction you abruptly get all the real numbers -- e.g., the square root of 2 is L|R where L = {dyadic rational numbers that are negative or have a square smaller than 2} and R = {dyadic rational numbers that are positive and have a square larger than 2} -- and you also get {0,1,2,3,4,...}|∅, conventionally written as a lower-case Greek letter omega, which is an infinite number, larger than all the integers. (And its negation.) And {0}|{1,1/2,1/3,1/4,...} which is an infinitesimal number, positive but smaller than any ratio of positive integers. And you can then proceed further and construct a vast infinitude of numbers, including all the real numbers (which we've already made) and all of the so-called infinite ordinals (which you can kinda think of as being a sort of "infinite positive integer", though there's more to them than that) and much more, all in a system that lets you do arithmetic and suchlike. It's very elegant, if your brain has been twisted into the mathematician-y shape that finds such things elegant.
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
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 this was very well explained
I made a picture, hope this helps: https://excalidraw.com/#json=zfKWWn1h7GzdFca6RDdXl,plr_WeaCt...
Sorry it was confusing.
Edit: the picture is now edited into the article.
This would make a lot more sense to me if "nothing" and "nothing" were instead "-inf" and "+inf"
Some other comments clarify that "nothing" is more accurately "the empty set". This is helpful because at first I wrongly synonomized "nothing" with zero. But now I get tripped up on the "between" language. Maybe it's a lack of background in sets, but I don't know what "between" implies for an integer (zero) and a set (the empty set).
I didn't want to introduce the notion of infinity because there are actual "infinite numbers" on the surreal number line. I've kind of tried to have both the simplicity of set-theoretic definition and the intuition of the number line, and slightly bungled the exposition. I hope the newly added diagram helps.
My favorite intro to surreal numbers is https://www.infinitelymore.xyz/p/surreal-numbers, but it is behind a registration wall.
I'm not a mathematician and "nothing" doesn't really make sense for me either. But I guess the problem with inf might be that it'd be strange to get +2 as the next thing between +1 and +inf, while getting +1.5 between +1 and +2.
It's more that surreal numbers already include infinities like ω, ω + 1, and so on, so "inf" felt like a concept I want to avoid. The actual description is set-theoretic and uses empty sets there ("nothing to the left", "nothing to the right") so I took that a bit too literally.
Wow thanks. I'm a mathematician and also got lost at the step. This illustration makes the construction much more clear. The text isn't really describing this process well
No problem! I've added it to the article, appreciate the feedback.
I think it's just we don't have a way to say/write these numbers. So you make up a way to write them (-1 and 1) and continue.
The numbers don't matter and you could replace -1 and 1 with anything. It's just easier to begin your new fake number at - 1 and 1. Because position does matter.
This is very helpful!
Basically what I take away is that we're inventing a new number system from scratch. So we're not "proving" that 1 is a number between 0 and the empty set. We're defining it as such, and it just so happens that a number system defined this way works out in convergent ways with other mathematics.
Is that roughly right?
Exactly.
There has to be some procedure how to come up with "new" numbers though, if you want to have more in the end than just a fancy binary tree - in particular if you want to map your "fake numbers" to the reals, infinity, etc.
This procedure is enough. If you define addition and other operations in a certain way (as Conway did), it turns out that on the omega-th day (i.e. after initial infinite steps), all reals will be born.
> position does matter
Only as a mental abstraction that's based on our experience/concept of space+time.
I think he just wrote it in a confusing way. The quote before says:
> (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 than it seems. He doesn't really say which number to put there. In the examples, he mostly did "new number = (left number + right number) / 2", with special cases if any number is "nothing" - but he never actually wrote what the rules are here.)
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.
Hope the newly added picture helps see each step.
The image helped for me at least.
(Apparently I was extremely unclear with this text. For clarity: if you want to actually understand surreal numbers, go and read On Numbers and Games, by Conway, which is a delightful book; or get an LLM to talk you through Wikipedia. Original text follows.)
It’s a terrible explanation. A surreal number is defined as a pair of sets of surreal numbers (where you fiddle around the recursion in that definition by defining them in waves, so strictly speaking you’re defining “the surreal numbers born at time T” for each individual T given access to the surreal numbers born at all earlier times, and then you “take the union across all times”, scare quotes because there are too many times for this to result in a set). Zero is a surreal number but the LLM is using the word “zero” to mean “the set containing just the surreal number 0”; “nothing” here is the LLM’s obtuse word for the empty set. Wikipedia may actually be easier to follow.
If you can’t explain it better in the same amount of characters (or fewer), then I don’t think you’re qualified to “nuh-uh!!!” anyone. Sorry buddy.
I mean, I was intending to supply the words that would link the LLM’s explanation to a more normal one, not to explain it; apparently that was extremely unclear. An actual explanation is much longer, as indeed I attempted to indicate by pointing to Wikipedia and saying that it might be more clear.
“Doing better than a totally useless explanation in fewer characters” is in general impossible, of course, eg if the first explanation has only one character.
... wut? :/
> 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.
There's a skill for that (haven't tried myself but intend to; other of author's skills I've used have been a game changer).
- https://github.com/mattpocock/skills/blob/main/skills/produc...
- https://www.youtube.com/watch?v=s5T5oQJcJ6U
Ask for analogy in terms of a thing you are an expert in.
ie. i am an expert at zig, explain this c++ in terms of zig
This is called college.
Broadly, universities are too expensive, inequitable, suboptimal, not portable, and slow. There's a huge amount of room for improvement.
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 AI tools to accelerate learning 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.
I feel the same way. Want to become a dumb and dumber duo? I believe you could be my friend.
Pitch: a mini-series where a Dumb and Dumber duo get access to unlimited tokens via a roommates's account (who is an intern at a frontier lab).
In each episode they make a major science-fiction style breakthrough and grapple with the consequences without revealing themselves.
Plot twist: they were both sold on early investment in companies that survived the .com bust. Now they’re VCs that everybody worships as business geniuses even though they’re just lucky idiots, and the sycophantic chatbots finally let them feel as smart as everyone says they are, and a whole bunch of hype-drunk fans are feeding into it.
The Claude output in the first one-shot counterexample attempt is hilarious. I hate its writing most of the time but this stuff is next level deep-fried slop.
> And the control column confirms the resonance-necessity conjecture empirically: break the skeleton alignment and the joint kernel dies at the constrained window, exactly as the transversality heuristic predicted.
> The den has air in it.
> Drift fuel exists.
Discovering that poetry was cognitive compression is alone one of the latent findings LLMs unlocked.
You can so easily imagine this shit being read in a 90s slam poetry coffeehouse. Trust me I was there
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 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.
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 find this whole post fascinating in the context of https://news.ycombinator.com/item?id=49738091 and particularly this excerpt from Gowers:
> 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, understanding 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.
> I genuinely invite a refutation.
> 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.
Author here. No one's asking mathematicians to check the generated proof. I explain it in this part: https://overreacted.io/how-i-vibed-a-proof-of-conways-conjec...
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...
> If this file is correct and Lean kernel is correct, the proof is correct
There are two ifs in this sentence.
What is your point, exactly? Increasing number of people working in and around mathematics are relying on Lean kernel's correctness. That's kind of the point of tools like Lean. Why is it a problem for me to publish a result that relies on it? How do you think other Lean proofs work?
My point is what I said. Without understanding you are only able to say your proof is "likely" to be correct. It's clear from your writing that you understand that your proof will only be accepted once thoroughly reviewed by human mathematicians, who will certainly not be just verifying the definition. Bugs in Lean exist (you're a programmer and it's a program, why would you assume they don't?) and reward hacking and finding bugs are both well established LLM behaviours.
> Why is it a problem for me to publish a result that relies on it?
Bit over-sensitive here. I never said it was a problem for you to publish a result. You can do what you like on your blog and spend your tokens however you choose, just as I'm free to have my own opinions on the value of such an effort. I was responding to, and disputing, a commenter's assertion that understanding and problem-solving ability are "now ... not connected".
I see, we don't seem to disagree much.
While Lean is tightening things up after the recent LLM-driven hacks, I agree that bugs are possible. Although usually code that exploits them is obviously aggressive and is deliberately using the more obscure features related to metaprogramming. Also note that my solution has passed the nanoda kernel as well (https://palomar-registry.org/entry?id=PALOMAR-2026-09-03-000...).
That said, again, I never implied that I'm asking mathematicians to "laboriously checking the generated proof" which is what your parent comment says. The value to mathematicians is knowing that the conjecture is probably right, and knowing the rough path the LLM has taken to it. Instead of checking the Lean proof line by line, what mathematicians are interested in doing (at least, the ones I've been in contact with) is finding a shorter and more direct proof now that they're aware of the outline and main intermediate claims. As for how much value they find in that, I presume they would be able to speak to that when/if they would like to make their research public.
What is your point? Please don't be obtuse, it is more constructive to make your points clearly.
Yes, the timing of this post just after Gowers' post is fascinating. It is almost as if the marketing machine is well oiled.
What marketing machine? You think someone's paying me to do this?
When you descend into conspiracy theorizing to defend your prejudices, it's time to stop and reconsider.
You can see by who entered the discussion (not you) and immediately sank certain comments that this is a protected submission. One wonders why.
Or perhaps the criticisms are objectively unhinged and are so down voted without having to invent a conspiracy.
Really nice "proof guide": https://gaearon.github.io/conway-refinement/#/highlights
and "proof map": https://gaearon.github.io/conway-refinement/#/map/conway-ref...
My god, that proof map has so many parts O.O
Someone please vibe-prove that ZFC is inconsistent.
That's awesome! Congratulations!
I'd imagine that in three months when we all have access to communicating agent swarms this should be easier
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.
On the other hand here we have an amateur that could accelerate their learning and experimentation faster than ever possible before.
I don't know if this necessarily qualifies as "accelerating their learning". The user appears to know what the proof is doing, but not how or why.
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
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...
> Me: btw how’s your mood overall?
LOL. mood??
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 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.
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?
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.
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.
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.
Several of my coworkers — it’s not that unusual that if you can max out a couple accounts, the companies will obviously notice you (as a high cost customer), and sometimes offer more
I don't see why that's weird
ah, if it's anyone it'd be dan abramov
free time spent talking to llm, what an achievement!