10 ms·

I vibed a proof of Conway's conjecture

269 points by m-hodges 15d ago

https://github.com/gaearon/conway-refinement#why-i-think-its-correct https://github.com/gaearon/conway-refinement#why-i-think-its...

alikatyc 15d ago
free time spent talking to llm, what an achievement!
howunfortunate 15d ago
> 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.
- jdw64 15d ago
  I feel the same way. Want to become a dumb and dumber duo? I believe you could be my friend.
  - howunfortunate 15d ago
    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.
    - DrewADesign 15d ago
      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.
- dubcanada 15d ago
  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.
  - xg15 15d ago
    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.
    - danabramov 15d ago
      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.
  - skeledrew 15d ago
    > position does matter Only as a mental abstraction that's based on our experience/concept of space+time.
  - howunfortunate 15d ago
    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?
    - danabramov 15d ago
      Exactly.
  - deleted 15d ago
    [deleted]
- Smaug123 15d ago
  (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.
  - kdisndjwjdje 15d ago
    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.
    - Smaug123 15d ago
      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.
  - skeledrew 15d ago
    ... wut? :/
  - danabramov 15d ago
    LLM didn't write anything in my post; these are all my words and my choices. Conway himself described surreal generation in short like this in ONAG: > We may say that Cantor was only interested in moving ever rightwards, whereas Dedekind stopped to fill in the gaps, so that R was always empty for Cantor, never empty for Dedekind. It is remarkable that by dropping these restrictions we obtain a theory that is both more general and more easy to work with. This is precisely the intuition I present to the reader of the article. I am relying on visual aid (concretely, the ordered number line) to imply the machinery explicit in the actual recursive definition. The intended reader of this article is not a mathematician, and I think intuition is vastly more important here. And I don't think I'm conflating 0 with {0} as you claim. When I say zero is "between nothing and nothing", I mean 0 := {|}. When I say one is "between zero and nothing", I mean 1 := {0|}. When I say 1/2 is "between 0 and 1", I mean 1/2 := {0|1}. And so on. I elide "the simplest number" because I am already going in the order of simplicity. I do not need to explain that alternative spellings like 1/2 = {0.2 | 1} are valid because it is not relevant to establishing the mental model of birthdays. For the finite cases in my explanation, I do not need to explain that the left and the right parts form sets because I only ever need at most one surreal on either side to define the next generation. I also do not need to state the left/right order condition because it is already visually implied by the picture. For the same reason, I do not need to explicitly quantify over the set of earlier-born surreals, since in these finite cases, if we go birthday by birthday, each next day's surreals are definable via the numbers already constructed by the previous day. I agree that these finite examples don't spell out how to handle infinitely many bounds at the omega-th day, which is where I believe the illustration embedded below is more helpful. I still think "a gap beyond 0, 1, 2, 3, ... with nothing on the right" is a useful intuition when we get there. For a more precise but accessible treatment, I think https://www.infinitelymore.xyz/p/surreal-numbers https://www.infinitelymore.xyz/p/surreal-numbers is much clearer than Wikipedia.
- echelon 15d ago
  > 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.
  - skeledrew 15d ago
    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/productivity/teach/SKILL.md https://github.com/mattpocock/skills/blob/main/skills/produc... - https://www.youtube.com/watch?v=s5T5oQJcJ6U https://www.youtube.com/watch?v=s5T5oQJcJ6U
  - pyrolistical 15d ago
    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
  - mrguyorama 15d ago
    This is called college.
    - echelon 15d ago
      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.
- svachalek 15d ago
  The image helped for me at least.
- xg15 15d ago
  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.)
  - gf000 15d ago
    You have infinite steps. Pi is just taking the correct turn an infinite number of times.
- skeledrew 15d ago
  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.
  - danabramov 15d ago
    Hope the newly added picture helps see each step.
- gjm11 15d ago
  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.
- danabramov 15d ago
  I made a picture, hope this helps: https://excalidraw.com/#json=zfKWWn1h7GzdFca6RDdXl,plr_WeaCtvFxbjULFjq6zw https://excalidraw.com/#json=zfKWWn1h7GzdFca6RDdXl,plr_WeaCt... Sorry it was confusing. Edit: the picture is now edited into the article.
  - howunfortunate 15d ago
    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).
    - danabramov 15d ago
      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 https://www.infinitelymore.xyz/p/surreal-numbers, but it is behind a registration wall.
    - mcintyre1994 15d ago
      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.
      - danabramov 15d ago
        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.
- bmacho 14d ago
  > 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. You build up surreal numbers as {∅|∅}, {∅|{∅|∅}}, {{∅|∅}|∅} and so on. --- Edit: A happy accident: I denoted the "empty set of surreal numbers" with the symbol ∅. It works, and it gives you the surreal numbers. But if you think of ∅ as the empty set in set theory, then the same construction (using an ordered-pair construction) gives you the surreal numbers as sets!
  - danabramov 14d ago
    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.
GPerson 15d ago
[flagged]
- dcre 15d ago
  What is stopping anyone from finding the value they would have found before?
- nbulka 15d ago
  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.
  - GPerson 14d ago
    The blog literally says he had no idea what was going on for the entire time.
- addlatt 15d ago
  Nihilistic view
  - idjeicjejdjej 15d ago
    Idiotic view, more like. Let’s not infuse good faith into what is clearly meant as a derogatory comment.
    - GPerson 14d ago
      Being derogatory is not incompatible with good faith, idiot.
  - GPerson 14d ago
    It’s not nihilism to see the death of my career.
- 15d ago
cyclopeanutopia 15d ago
Someone please vibe-prove that ZFC is inconsistent.
vatsachak 15d ago
That's awesome! Congratulations! I'd imagine that in three months when we all have access to communicating agent swarms this should be easier
tonetheman 15d ago
[dead]
bwfan123 15d ago
> 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 https://en.wikipedia.org/wiki/Infinite_monkey_theorem
- deleted 15d ago
  [deleted]
- johnsmith1840 15d ago
  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?
  - alansaber 15d ago
    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.
    - jimmaswell 15d ago
      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.
msteffen 15d ago
I find this whole post fascinating in the context of https://news.ycombinator.com/item?id=49738091 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.
- 31276ahq 15d ago
  Yes, the timing of this post just after Gowers' post is fascinating. It is almost as if the marketing machine is well oiled.
  - danabramov 15d ago
    What marketing machine? You think someone's paying me to do this?
  - pfdietz 15d ago
    When you descend into conspiracy theorizing to defend your prejudices, it's time to stop and reconsider.
31276ahq 15d ago
[flagged]
- memonkey 15d ago
  ah, if it's anyone it'd be dan abramov
  - deleted 15d ago
    [deleted]
- manwe150 15d ago
  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
- Retr0id 15d ago
  I don't see why that's weird
- deleted 15d ago
  [deleted]
- dcre 15d ago
  $200 a month is what people pay for morning coffee in the Bay Area.
nialv7 15d ago
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??
- danabramov 15d ago
  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".
  - GPerson 14d ago
    Dude you’re so far removed from understanding anything about what the math community thinks. Just stop this nonsense. This is not “your” result.
    - danabramov 14d ago
      What do you want me to call it? I'm fine calling it your result if you want.
      - GPerson 14d ago
        It’s nobody’s result what is wrong with you?
    - GPerson 14d ago
      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.
renyicircle 15d ago
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.
- 1attice 15d ago
  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
  - renyicircle 15d ago
    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.
    - 1attice 15d ago
      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
  - nonameiguess 15d ago
    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.
  - 15d ago
makerofthings 15d ago
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.
- Joel_Mckay 15d ago
  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
- zerotolerance 15d ago
  On the other hand here we have an amateur that could accelerate their learning and experimentation faster than ever possible before.
  - Feathercrown 15d ago
    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.
  - GPerson 14d ago
    They accelerated zero learning. Read the blog.
- deleted 15d ago
  [deleted]
mihau 15d ago
Really nice "proof guide": https://gaearon.github.io/conway-refinement/#/highlights https://gaearon.github.io/conway-refinement/#/highlights and "proof map": https://gaearon.github.io/conway-refinement/#/map/conway-refinement https://gaearon.github.io/conway-refinement/#/map/conway-ref...
- kevinwang 15d ago
  My god, that proof map has so many parts O.O
unholiness 15d ago
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+surreal+numbers+hackingbush+summer+of+math&oq=video+introduction+to+surreal+numbers+hackingbush+summer+of+math+&gs_lcrp=EgZjaHJvbWUyBggAEEUYOTIHCAEQIRiPAjIHCAIQIRiPAtIBCTE2NzgxajBqN6gCALACAA&sourceid=chrome&source=chrome.ob&ie=UTF-8#fpstate=ive&vld=cid:7a30ab7b,vid:ZYj4NkeGPdM,st:0 https://www.google.com/search?q=video+introduction+to+surrea...
- WithinReason 15d ago
  https://www.youtube.com/watch?v=ZYj4NkeGPdM https://www.youtube.com/watch?v=ZYj4NkeGPdM
sigmar 15d ago
>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.
- deleted 15d ago
  [deleted]
- danabramov 15d ago
  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.
- vessenes 15d ago
  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.
  - stevemk14ebr 15d ago
    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.
    - dev_dan_2 15d ago
math_dandy 15d ago
[dead]
pretzellogician 15d ago
(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!
- zozbot234 15d ago
  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.
  - xworld21 14d ago
    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.
gbjcantab 15d ago
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.
- patcon 15d ago
  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
  - KyleTheDev 15d ago
    All this time, I've been considering myself the warlock. When, in fact, I've simply been the Imp. Dastardly news.
    - dodslaser 14d ago
      It's goblins all the way down.
  - gbjcantab 15d ago
    The same corollary occurred to me, as well!
  - dormento 15d ago
    And now everyone is a sorcerer: they can trap small demons inside metal boxes and force them to do their bidding. As before, any supernatural effects are performed by those beings (which were willed into existence by siphoning the wisdom from the wizard's own grimoires...)
Feathercrown 15d ago
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.
- danabramov 15d ago
  Hah, very interesting question! 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.
FiatLuxDave 15d ago
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.
- nphardon 14d ago
  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.
nphardon 15d ago
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.
bonoboTP 15d ago
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.
- GPerson 14d ago
  No this guy demonstrated zero intelligence unless the word has already lost all meaning.
  - bonoboTP 14d ago
    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.
    - GPerson 14d ago
      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.
j2kun 15d ago
Perhaps one thing you should devote effort to is ensuring this has not already been proved in the literature.
- danabramov 15d ago
  I've confirmed with the mathematicians working in that field that this is a new result.
  - ianjbutler 15d ago
    Regardless of whether the target result(s) are ultimately correct, isn't it almost guaranteed that supporting infrastructure for surreals-in-lean is a real contribution? Is it a goal to make those polished/reusable, or more like throw-away harness, and just a stepping stone to the proof?
    - danabramov 15d ago
      I'm a little tired from the project so not eager to jump back into it right away. But yes, I'd love for useful pieces to make their way into https://github.com/vihdzp/combinatorial-games https://github.com/vihdzp/combinatorial-games. Violeta, who maintains CG, expressed interest in ultimately integrating the proof in some shape into the repo, but I think more work needs to be done to understand what makes it work.
tuesdaynight 15d ago
Damn, I was not expecting Dan Abramov when I read the title.
spongebobstoes 15d ago
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
rlue 14d ago
> Take all the numbers you have so far. Then, “spawn” a new number in every gap between the numbers you already have (crucially, “to the left of all” and “to the right of all” also count as “gaps”). Apply this step forevermore, and you’ll get surreal numbers. I'm not a mathematician. Can someone explain to me how this approach gets you beyond the rational numbers? Also, this was formatted as a blockquote, but as far as I can see, this blog post is the only instance of this formulation online.
- sebzim4500 14d ago
  You can have an infinite number of numbers on both sides. E.g. you can ask for a number between 0 and 1,1/2,1/3,... (which gives you an infinitesimal)
doctoboggan 14d ago
> a sort of epistemic performance art project. Agreed, and it's a wonderful piece of art. I look forward to seeing the actual publication and reaction from the math community.
deleted 14d ago
[deleted]
fukaiall 14d ago
If this proof is actually valid, this could be a pretty shocking news to the entire academic fields. A software engineer who has never been trained as a professional mathematician, not even having his college degree in numerical field, with pure interest in math, now can solve problems that not even those Fields medalists cannot. Now I feel like all the intellectual hierarchies and reward systems are broken. Who’s gonna waste his or her fucking time and money in degrees and papers when you just mess around Claude?
cubefox 14d ago
It's quite the irony that in the end he says > Although the current generation of models is trained to complete tasks rather than to enrich our understanding, and today’s AI companies are misaligned with the goals of the mathematical community, I hope that with time we’ll find ways to use these tools in harmony with human research. while citing "A Severe Misalignment of AI in Mathematics" [1], which condemns exactly the thing he is doing himself: Mindlessly producing theorems without a corresponding human understanding of the underlying proofs. 1: https://mathandai.org/ https://mathandai.org/
- danabramov 14d ago
  Perhaps you and I read this document differently. This is not a “famous problem”, I am not a “major AI company”, and I am genuinely interested in increasing mathematical understanding. To the last point, here is a comment from a mathematician who co-authored the paper that my proof is largely built upon: https://news.ycombinator.com/item?id=49761718 https://news.ycombinator.com/item?id=49761718 The happy case here is that my obtuse proof leads to a concise and illuminating mathematical proof, which is exactly my hope for the endeavour. I think this could then be a positive example of AI/human and amateur/professional collaboration. What would a positive example look like to you? What do you think the manifesto argues for?
  - GPerson 14d ago
    It is a famous problem!!!!!!!!!! You literally understand nothing about the culture you’re stomping all over.
    - danabramov 14d ago
      I may be wrong here but my impression is that surreal numbers in general are kind of a niche area that hasn’t enjoyed a ton of interest. Additionally, this specific conjecture did not have any “prizes” attached to it and was not on any list of famous problems I could find. It’s even difficult to Google. What precisely do you mean by it being a famous problem?
patcon 14d ago
Deeplinked reply from Prof Vincenzo Mantova[1], who is reviewing results: https://news.ycombinator.com/item?id=49761718 https://news.ycombinator.com/item?id=49761718 [1] https://eps.leeds.ac.uk/maths/staff/4058/dr-vincenzo-l-mantova https://eps.leeds.ac.uk/maths/staff/4058/dr-vincenzo-l-manto...
bastawhiz 14d ago
These are indisputably good results all things considered. But I have to wonder whether a more scientific and hands-on approach to working on the material would have been better. When I vibe code, I don't just hype the LLM up and tell it to keep going. I interrogate it, I ask it to back up and replace its jargon, and I force it to be accountable. It smells to me like a lot of the circling could have been avoided (even without domain expertise) by just enforcing processes. Even just keeping the Lean more up to date would have likely saved tokens: it doesn't matter if it took longer each week, since the total runtime mostly wasn't the bottleneck.
- danabramov 14d ago
  >I interrogate it, I ask it to back up and replace its jargon, and I force it to be accountable I do that too when working on software. Here, I did a little bit of that, but it is much harder when I have almost no domain knowledge (aside from understanding the statement of the conjecture), since at each point the LLM might trick me anyway, and it would probably take me a year to understand the concepts enough to tell when what it's saying doesn't make sense. >Even just keeping the Lean more up to date would have likely saved tokens That's the conclusion I came to by the final week! But don't underestimate how much Lean needed to be written in the first place to even "catch up" with the reference papers. I had no option to keep it up to date when I started.
GPerson 14d ago
This is just an immoral thing to do. If you don’t understand why you should read Terence Tao’s posts about stripmining. This guy isn’t committed to understanding anything. He’s just screwing around and hoping other people who are turn this into something beneficial to others. He’s just extracting value built up by others over a long period, depleting the finite resource of motivation to work on this topic.
- danabramov 14d ago
  Imagine we discover an alien spaceship, and inside it, a codex. Decyphering the codex tells us a bunch of solutions to alien mathematics, which is remarkably similar to ours and has compatible foundations, but way more convoluted in the actual thought process. The codex would contain proofs of some statements equivalent to open statements today. Would you, in this situation, be mad at the aliens? Would you say the aliens have "extracted value"? This is kind of how I see this project.
  - GPerson 14d ago
    You are not the alien. You are the other human being extracting value from labor and efforts of other humans, with nothing but contempt from them. I am not mad at the computer. What a ridiculous analogy.
    - danabramov 14d ago
      What is the value that I am extracting? The alien in the analogy is the corpus of knowledge that’s newly reachable via LLMs.
      - GPerson 14d ago
        No, you’re confused about your own analogy. That corpus of knowledge is the extra mathematics the aliens have. The LLM based AI system and the out of control AI corporations are the aliens. You are some guy inviting the aliens to degrade the possibility of a meaningful existence.
deiptx 14d ago
Is the author suggesting that understanding has no value? because this is what I could gather from reading this. Edit: Another depressing fact is that he generously paid to LLM megacorps while piggy backing on human help for free and in the end calls the proof his or LLM's.
- danabramov 14d ago
  Is a YouTuber speedrunning a game by exploiting an integer overflow bug suggesting that gaming has no value? No, they're just having fun with the medium. To answer directly: I think understanding is the primary value. And I have reasons to hope that my "work" here can ultimately contribute to a better understanding: https://news.ycombinator.com/item?id=49761718 https://news.ycombinator.com/item?id=49761718. However, there are also other reasons to do things than producing value. You can do things for fun, to show they're possible, to ask meta questions about the field. Regarding calling the proof "mine", I've replied to that here: https://news.ycombinator.com/item?id=49755885 https://news.ycombinator.com/item?id=49755885.
  - deiptx 14d ago
    Following your analogy it is not a very fair game if it allows winning for those having access to latest exploits. Playing against skiddies who bought the hack kind of ruins it. I read your comment and my edit was inspired by it. Your article only mentions nameless mathematicians, without really giving credit.
    - danabramov 13d ago
      >Your article only mentions nameless mathematicians, without really giving credit. I explicitly give credit to the papers the proof builds upon. Quoting from the article: >The proof was only possible thanks to the many existing results from [References](https://gaearon.github.io/conway-refinement/#/references https://gaearon.github.io/conway-refinement/#/references). In particular, [A factorisation theory for generalised power series and omnific integers](https://doi.org/10.1016/j.aim.2024.109513 https://doi.org/10.1016/j.aim.2024.109513) by S. L’Innocente and V. Mantova has played a crucial role in the proof. The project README (https://github.com/gaearon/conway-refinement https://github.com/gaearon/conway-refinement) also states: >Over the years, Berarducci, Pitteloud, Pommersheim and Shahriari, and L'Innocente and Mantova developed increasingly strong results about exactly that. This proof builds on all of that work and claims to finish the refinement conjecture. It includes the same list of references: https://github.com/gaearon/conway-refinement#references https://github.com/gaearon/conway-refinement#references Regarding who I've talked to over email, I wasn't sure I want to "out" them explicitly in the article due to the article's likely polarizing nature, but, since he already engaged in this thread, I can confirm that this person was Prof. Mantova (who is a co-author of the primary paper that the result I published rests upon, and who I did explicitly credit in the text of the article and in the references). You can read Prof. Mantova's own reflection here: https://news.ycombinator.com/item?id=49761718 https://news.ycombinator.com/item?id=49761718 I have not had an extended conversation with anyone else. >Following your analogy it is not a very fair game if it allows winning for those having access to latest exploits. Playing against skiddies who bought the hack kind of ruins it. You misunderstood the point of my analogy. The point was not that it is a game in which you "win" or "lose" and thus I have "won" or something like that. The point was that "obtaining a true proof without understanding it" doesn't imply "understanding has no value" any more than "completing a game in an unintended way" implies "playing has no value". You stated a false implication. That false implication is what I am highlighting with the analogy. Understanding has a societal value; doing something weird for the fun of it has value to the person doing it; sometimes people do things with no value at all, and that's okay too. Each individual act is not a statement about what kinds of things have value. Personally, I do not see mathematics as a game of "win" and "lose". If the broad value is primarily in understanding (which I think is correct), then my "contribution" doesn't make much dent in that. However, it might, as Prof. Mantova mentions, help show the way to an actually useful proof that improves collective understanding. That would please me beyond merely having had fun. In any case, I've enjoyed the experience of it in part due to the absurdity of it. Maybe it requires a certain kind of sense of humor. Regarding the models, as far as I know, all of the models I have used are currently broadly available. Yes, they require subscriptions so access is not democratized yet. There's nothing I can do about that. I think it's unreasonable to require that someone playing around with LLM's must use the inferior free models.

269 points by m-hodges 15d ago

https://github.com/gaearon/conway-refinement#why-i-think-its-correct https://github.com/gaearon/conway-refinement#why-i-think-its...

alikatyc 15d ago

free time spent talking to llm, what an achievement!

howunfortunate 15d ago

> 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.

jdw64 15d ago
I feel the same way. Want to become a dumb and dumber duo? I believe you could be my friend.
- howunfortunate 15d ago
  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.
  - DrewADesign 15d ago
    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.
dubcanada 15d ago
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.
- xg15 15d ago
  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.
  - danabramov 15d ago
    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.
- skeledrew 15d ago
  > position does matter Only as a mental abstraction that's based on our experience/concept of space+time.
- howunfortunate 15d ago
  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?
  - danabramov 15d ago
    Exactly.
- deleted 15d ago
  [deleted]
Smaug123 15d ago
(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.
- kdisndjwjdje 15d ago
  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.
  - Smaug123 15d ago
    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.
- skeledrew 15d ago
  ... wut? :/
- danabramov 15d ago
  LLM didn't write anything in my post; these are all my words and my choices. Conway himself described surreal generation in short like this in ONAG: > We may say that Cantor was only interested in moving ever rightwards, whereas Dedekind stopped to fill in the gaps, so that R was always empty for Cantor, never empty for Dedekind. It is remarkable that by dropping these restrictions we obtain a theory that is both more general and more easy to work with. This is precisely the intuition I present to the reader of the article. I am relying on visual aid (concretely, the ordered number line) to imply the machinery explicit in the actual recursive definition. The intended reader of this article is not a mathematician, and I think intuition is vastly more important here. And I don't think I'm conflating 0 with {0} as you claim. When I say zero is "between nothing and nothing", I mean 0 := {|}. When I say one is "between zero and nothing", I mean 1 := {0|}. When I say 1/2 is "between 0 and 1", I mean 1/2 := {0|1}. And so on. I elide "the simplest number" because I am already going in the order of simplicity. I do not need to explain that alternative spellings like 1/2 = {0.2 | 1} are valid because it is not relevant to establishing the mental model of birthdays. For the finite cases in my explanation, I do not need to explain that the left and the right parts form sets because I only ever need at most one surreal on either side to define the next generation. I also do not need to state the left/right order condition because it is already visually implied by the picture. For the same reason, I do not need to explicitly quantify over the set of earlier-born surreals, since in these finite cases, if we go birthday by birthday, each next day's surreals are definable via the numbers already constructed by the previous day. I agree that these finite examples don't spell out how to handle infinitely many bounds at the omega-th day, which is where I believe the illustration embedded below is more helpful. I still think "a gap beyond 0, 1, 2, 3, ... with nothing on the right" is a useful intuition when we get there. For a more precise but accessible treatment, I think https://www.infinitelymore.xyz/p/surreal-numbers https://www.infinitelymore.xyz/p/surreal-numbers is much clearer than Wikipedia.
echelon 15d ago
> 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.
- skeledrew 15d ago
  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/productivity/teach/SKILL.md https://github.com/mattpocock/skills/blob/main/skills/produc... - https://www.youtube.com/watch?v=s5T5oQJcJ6U https://www.youtube.com/watch?v=s5T5oQJcJ6U
- pyrolistical 15d ago
  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
- mrguyorama 15d ago
  This is called college.
  - echelon 15d ago
    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.
svachalek 15d ago
The image helped for me at least.
xg15 15d ago
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.)
- gf000 15d ago
  You have infinite steps. Pi is just taking the correct turn an infinite number of times.
skeledrew 15d ago
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.
- danabramov 15d ago
  Hope the newly added picture helps see each step.
gjm11 15d ago
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.
danabramov 15d ago
I made a picture, hope this helps: https://excalidraw.com/#json=zfKWWn1h7GzdFca6RDdXl,plr_WeaCtvFxbjULFjq6zw https://excalidraw.com/#json=zfKWWn1h7GzdFca6RDdXl,plr_WeaCt... Sorry it was confusing. Edit: the picture is now edited into the article.
- howunfortunate 15d ago
  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).
  - danabramov 15d ago
    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 https://www.infinitelymore.xyz/p/surreal-numbers, but it is behind a registration wall.
  - mcintyre1994 15d ago
    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.
    - danabramov 15d ago
      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.
bmacho 14d ago
> 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. You build up surreal numbers as {∅|∅}, {∅|{∅|∅}}, {{∅|∅}|∅} and so on. --- Edit: A happy accident: I denoted the "empty set of surreal numbers" with the symbol ∅. It works, and it gives you the surreal numbers. But if you think of ∅ as the empty set in set theory, then the same construction (using an ordered-pair construction) gives you the surreal numbers as sets!
- danabramov 14d ago
  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.

GPerson 15d ago

[flagged]

dcre 15d ago
What is stopping anyone from finding the value they would have found before?
nbulka 15d ago
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.
- GPerson 14d ago
  The blog literally says he had no idea what was going on for the entire time.
addlatt 15d ago
Nihilistic view
- idjeicjejdjej 15d ago
  Idiotic view, more like. Let’s not infuse good faith into what is clearly meant as a derogatory comment.
  - GPerson 14d ago
    Being derogatory is not incompatible with good faith, idiot.
- GPerson 14d ago
  It’s not nihilism to see the death of my career.
15d ago

cyclopeanutopia 15d ago

Someone please vibe-prove that ZFC is inconsistent.

vatsachak 15d ago

That's awesome! Congratulations! I'd imagine that in three months when we all have access to communicating agent swarms this should be easier

tonetheman 15d ago

[dead]

bwfan123 15d ago

> 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 https://en.wikipedia.org/wiki/Infinite_monkey_theorem

deleted 15d ago
[deleted]
johnsmith1840 15d ago
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?
- alansaber 15d ago
  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.
  - jimmaswell 15d ago
    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.

msteffen 15d ago

I find this whole post fascinating in the context of https://news.ycombinator.com/item?id=49738091 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.

31276ahq 15d ago
Yes, the timing of this post just after Gowers' post is fascinating. It is almost as if the marketing machine is well oiled.
- danabramov 15d ago
  What marketing machine? You think someone's paying me to do this?
- pfdietz 15d ago
  When you descend into conspiracy theorizing to defend your prejudices, it's time to stop and reconsider.

31276ahq 15d ago

[flagged]

memonkey 15d ago
ah, if it's anyone it'd be dan abramov
- deleted 15d ago
  [deleted]
manwe150 15d ago
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
Retr0id 15d ago
I don't see why that's weird
deleted 15d ago
[deleted]
dcre 15d ago
$200 a month is what people pay for morning coffee in the Bay Area.

nialv7 15d ago

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??

danabramov 15d ago
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".
- GPerson 14d ago
  Dude you’re so far removed from understanding anything about what the math community thinks. Just stop this nonsense. This is not “your” result.
  - danabramov 14d ago
    What do you want me to call it? I'm fine calling it your result if you want.
    - GPerson 14d ago
      It’s nobody’s result what is wrong with you?
  - GPerson 14d ago
    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.

renyicircle 15d ago

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.

1attice 15d ago
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
- renyicircle 15d ago
  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.
  - 1attice 15d ago
    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
- nonameiguess 15d ago
  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.
- 15d ago

makerofthings 15d ago

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.

Joel_Mckay 15d ago
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
zerotolerance 15d ago
On the other hand here we have an amateur that could accelerate their learning and experimentation faster than ever possible before.
- Feathercrown 15d ago
  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.
- GPerson 14d ago
  They accelerated zero learning. Read the blog.
deleted 15d ago
[deleted]

mihau 15d ago

Really nice "proof guide": https://gaearon.github.io/conway-refinement/#/highlights https://gaearon.github.io/conway-refinement/#/highlights and "proof map": https://gaearon.github.io/conway-refinement/#/map/conway-refinement https://gaearon.github.io/conway-refinement/#/map/conway-ref...

kevinwang 15d ago
My god, that proof map has so many parts O.O

unholiness 15d ago

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+surreal+numbers+hackingbush+summer+of+math&oq=video+introduction+to+surreal+numbers+hackingbush+summer+of+math+&gs_lcrp=EgZjaHJvbWUyBggAEEUYOTIHCAEQIRiPAjIHCAIQIRiPAtIBCTE2NzgxajBqN6gCALACAA&sourceid=chrome&source=chrome.ob&ie=UTF-8#fpstate=ive&vld=cid:7a30ab7b,vid:ZYj4NkeGPdM,st:0 https://www.google.com/search?q=video+introduction+to+surrea...

WithinReason 15d ago
https://www.youtube.com/watch?v=ZYj4NkeGPdM https://www.youtube.com/watch?v=ZYj4NkeGPdM

sigmar 15d ago

>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.

deleted 15d ago
[deleted]
danabramov 15d ago
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.
vessenes 15d ago
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.
- stevemk14ebr 15d ago
  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.
  - dev_dan_2 15d ago

math_dandy 15d ago

[dead]

pretzellogician 15d ago

(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!

zozbot234 15d ago
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.
- xworld21 14d ago
  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.

gbjcantab 15d ago

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.

patcon 15d ago
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
- KyleTheDev 15d ago
  All this time, I've been considering myself the warlock. When, in fact, I've simply been the Imp. Dastardly news.
  - dodslaser 14d ago
    It's goblins all the way down.
- gbjcantab 15d ago
  The same corollary occurred to me, as well!
- dormento 15d ago
  And now everyone is a sorcerer: they can trap small demons inside metal boxes and force them to do their bidding. As before, any supernatural effects are performed by those beings (which were willed into existence by siphoning the wisdom from the wizard's own grimoires...)

Feathercrown 15d ago

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.

danabramov 15d ago
Hah, very interesting question! 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.

FiatLuxDave 15d ago

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.

nphardon 14d ago
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.

nphardon 15d ago

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.

bonoboTP 15d ago

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.

GPerson 14d ago
No this guy demonstrated zero intelligence unless the word has already lost all meaning.
- bonoboTP 14d ago
  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.
  - GPerson 14d ago
    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.

j2kun 15d ago

Perhaps one thing you should devote effort to is ensuring this has not already been proved in the literature.

danabramov 15d ago
I've confirmed with the mathematicians working in that field that this is a new result.
- ianjbutler 15d ago
  Regardless of whether the target result(s) are ultimately correct, isn't it almost guaranteed that supporting infrastructure for surreals-in-lean is a real contribution? Is it a goal to make those polished/reusable, or more like throw-away harness, and just a stepping stone to the proof?
  - danabramov 15d ago
    I'm a little tired from the project so not eager to jump back into it right away. But yes, I'd love for useful pieces to make their way into https://github.com/vihdzp/combinatorial-games https://github.com/vihdzp/combinatorial-games. Violeta, who maintains CG, expressed interest in ultimately integrating the proof in some shape into the repo, but I think more work needs to be done to understand what makes it work.

tuesdaynight 15d ago

Damn, I was not expecting Dan Abramov when I read the title.

spongebobstoes 15d ago

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

rlue 14d ago

> Take all the numbers you have so far. Then, “spawn” a new number in every gap between the numbers you already have (crucially, “to the left of all” and “to the right of all” also count as “gaps”). Apply this step forevermore, and you’ll get surreal numbers. I'm not a mathematician. Can someone explain to me how this approach gets you beyond the rational numbers? Also, this was formatted as a blockquote, but as far as I can see, this blog post is the only instance of this formulation online.

sebzim4500 14d ago
You can have an infinite number of numbers on both sides. E.g. you can ask for a number between 0 and 1,1/2,1/3,... (which gives you an infinitesimal)

doctoboggan 14d ago

> a sort of epistemic performance art project. Agreed, and it's a wonderful piece of art. I look forward to seeing the actual publication and reaction from the math community.

deleted 14d ago

[deleted]

fukaiall 14d ago

If this proof is actually valid, this could be a pretty shocking news to the entire academic fields. A software engineer who has never been trained as a professional mathematician, not even having his college degree in numerical field, with pure interest in math, now can solve problems that not even those Fields medalists cannot. Now I feel like all the intellectual hierarchies and reward systems are broken. Who’s gonna waste his or her fucking time and money in degrees and papers when you just mess around Claude?

cubefox 14d ago

It's quite the irony that in the end he says > Although the current generation of models is trained to complete tasks rather than to enrich our understanding, and today’s AI companies are misaligned with the goals of the mathematical community, I hope that with time we’ll find ways to use these tools in harmony with human research. while citing "A Severe Misalignment of AI in Mathematics" [1], which condemns exactly the thing he is doing himself: Mindlessly producing theorems without a corresponding human understanding of the underlying proofs. 1: https://mathandai.org/ https://mathandai.org/

danabramov 14d ago
Perhaps you and I read this document differently. This is not a “famous problem”, I am not a “major AI company”, and I am genuinely interested in increasing mathematical understanding. To the last point, here is a comment from a mathematician who co-authored the paper that my proof is largely built upon: https://news.ycombinator.com/item?id=49761718 https://news.ycombinator.com/item?id=49761718 The happy case here is that my obtuse proof leads to a concise and illuminating mathematical proof, which is exactly my hope for the endeavour. I think this could then be a positive example of AI/human and amateur/professional collaboration. What would a positive example look like to you? What do you think the manifesto argues for?
- GPerson 14d ago
  It is a famous problem!!!!!!!!!! You literally understand nothing about the culture you’re stomping all over.
  - danabramov 14d ago
    I may be wrong here but my impression is that surreal numbers in general are kind of a niche area that hasn’t enjoyed a ton of interest. Additionally, this specific conjecture did not have any “prizes” attached to it and was not on any list of famous problems I could find. It’s even difficult to Google. What precisely do you mean by it being a famous problem?

patcon 14d ago

Deeplinked reply from Prof Vincenzo Mantova[1], who is reviewing results: https://news.ycombinator.com/item?id=49761718 https://news.ycombinator.com/item?id=49761718 [1] https://eps.leeds.ac.uk/maths/staff/4058/dr-vincenzo-l-mantova https://eps.leeds.ac.uk/maths/staff/4058/dr-vincenzo-l-manto...

bastawhiz 14d ago

These are indisputably good results all things considered. But I have to wonder whether a more scientific and hands-on approach to working on the material would have been better. When I vibe code, I don't just hype the LLM up and tell it to keep going. I interrogate it, I ask it to back up and replace its jargon, and I force it to be accountable. It smells to me like a lot of the circling could have been avoided (even without domain expertise) by just enforcing processes. Even just keeping the Lean more up to date would have likely saved tokens: it doesn't matter if it took longer each week, since the total runtime mostly wasn't the bottleneck.

danabramov 14d ago
>I interrogate it, I ask it to back up and replace its jargon, and I force it to be accountable I do that too when working on software. Here, I did a little bit of that, but it is much harder when I have almost no domain knowledge (aside from understanding the statement of the conjecture), since at each point the LLM might trick me anyway, and it would probably take me a year to understand the concepts enough to tell when what it's saying doesn't make sense. >Even just keeping the Lean more up to date would have likely saved tokens That's the conclusion I came to by the final week! But don't underestimate how much Lean needed to be written in the first place to even "catch up" with the reference papers. I had no option to keep it up to date when I started.

GPerson 14d ago

This is just an immoral thing to do. If you don’t understand why you should read Terence Tao’s posts about stripmining. This guy isn’t committed to understanding anything. He’s just screwing around and hoping other people who are turn this into something beneficial to others. He’s just extracting value built up by others over a long period, depleting the finite resource of motivation to work on this topic.

danabramov 14d ago
Imagine we discover an alien spaceship, and inside it, a codex. Decyphering the codex tells us a bunch of solutions to alien mathematics, which is remarkably similar to ours and has compatible foundations, but way more convoluted in the actual thought process. The codex would contain proofs of some statements equivalent to open statements today. Would you, in this situation, be mad at the aliens? Would you say the aliens have "extracted value"? This is kind of how I see this project.
- GPerson 14d ago
  You are not the alien. You are the other human being extracting value from labor and efforts of other humans, with nothing but contempt from them. I am not mad at the computer. What a ridiculous analogy.
  - danabramov 14d ago
    What is the value that I am extracting? The alien in the analogy is the corpus of knowledge that’s newly reachable via LLMs.
    - GPerson 14d ago
      No, you’re confused about your own analogy. That corpus of knowledge is the extra mathematics the aliens have. The LLM based AI system and the out of control AI corporations are the aliens. You are some guy inviting the aliens to degrade the possibility of a meaningful existence.

deiptx 14d ago

Is the author suggesting that understanding has no value? because this is what I could gather from reading this. Edit: Another depressing fact is that he generously paid to LLM megacorps while piggy backing on human help for free and in the end calls the proof his or LLM's.

danabramov 14d ago
Is a YouTuber speedrunning a game by exploiting an integer overflow bug suggesting that gaming has no value? No, they're just having fun with the medium. To answer directly: I think understanding is the primary value. And I have reasons to hope that my "work" here can ultimately contribute to a better understanding: https://news.ycombinator.com/item?id=49761718 https://news.ycombinator.com/item?id=49761718. However, there are also other reasons to do things than producing value. You can do things for fun, to show they're possible, to ask meta questions about the field. Regarding calling the proof "mine", I've replied to that here: https://news.ycombinator.com/item?id=49755885 https://news.ycombinator.com/item?id=49755885.
- deiptx 14d ago
  Following your analogy it is not a very fair game if it allows winning for those having access to latest exploits. Playing against skiddies who bought the hack kind of ruins it. I read your comment and my edit was inspired by it. Your article only mentions nameless mathematicians, without really giving credit.
  - danabramov 13d ago
    >Your article only mentions nameless mathematicians, without really giving credit. I explicitly give credit to the papers the proof builds upon. Quoting from the article: >The proof was only possible thanks to the many existing results from [References](https://gaearon.github.io/conway-refinement/#/references https://gaearon.github.io/conway-refinement/#/references). In particular, [A factorisation theory for generalised power series and omnific integers](https://doi.org/10.1016/j.aim.2024.109513 https://doi.org/10.1016/j.aim.2024.109513) by S. L’Innocente and V. Mantova has played a crucial role in the proof. The project README (https://github.com/gaearon/conway-refinement https://github.com/gaearon/conway-refinement) also states: >Over the years, Berarducci, Pitteloud, Pommersheim and Shahriari, and L'Innocente and Mantova developed increasingly strong results about exactly that. This proof builds on all of that work and claims to finish the refinement conjecture. It includes the same list of references: https://github.com/gaearon/conway-refinement#references https://github.com/gaearon/conway-refinement#references Regarding who I've talked to over email, I wasn't sure I want to "out" them explicitly in the article due to the article's likely polarizing nature, but, since he already engaged in this thread, I can confirm that this person was Prof. Mantova (who is a co-author of the primary paper that the result I published rests upon, and who I did explicitly credit in the text of the article and in the references). You can read Prof. Mantova's own reflection here: https://news.ycombinator.com/item?id=49761718 https://news.ycombinator.com/item?id=49761718 I have not had an extended conversation with anyone else. >Following your analogy it is not a very fair game if it allows winning for those having access to latest exploits. Playing against skiddies who bought the hack kind of ruins it. You misunderstood the point of my analogy. The point was not that it is a game in which you "win" or "lose" and thus I have "won" or something like that. The point was that "obtaining a true proof without understanding it" doesn't imply "understanding has no value" any more than "completing a game in an unintended way" implies "playing has no value". You stated a false implication. That false implication is what I am highlighting with the analogy. Understanding has a societal value; doing something weird for the fun of it has value to the person doing it; sometimes people do things with no value at all, and that's okay too. Each individual act is not a statement about what kinds of things have value. Personally, I do not see mathematics as a game of "win" and "lose". If the broad value is primarily in understanding (which I think is correct), then my "contribution" doesn't make much dent in that. However, it might, as Prof. Mantova mentions, help show the way to an actually useful proof that improves collective understanding. That would please me beyond merely having had fun. In any case, I've enjoyed the experience of it in part due to the absurdity of it. Maybe it requires a certain kind of sense of humor. Regarding the models, as far as I know, all of the models I have used are currently broadly available. Yes, they require subscriptions so access is not democratized yet. There's nothing I can do about that. I think it's unreasonable to require that someone playing around with LLM's must use the inferior free models.