I vibed a proof of Conway's conjecture

(overreacted.io)

270 points | by m-hodges 4 days ago ago

57 comments

  • gbjcantab 4 days ago 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.

    • necklesspen 4 days ago ago

      It's a truly wonderful read, made better by the fact the author doesn't quite understand what's going on.

      The usual format that fun mathematics is presented (being talked at by someone who is very well versed in the subject) comes with a heavy cognitive burden - and often I just can't really make it through.

      When the author is not an expert the writing is just so much more accessible - it's easier to understand and making it through feels more of an adventure and less of a lecture.

      I've never thought previously how much I would enjoy this format though. I'm here to see more amateurs stumbling through mathematics.

      Also, wasn't expecting this sort of side-quest from the guy who got me into React.

      • SturgeonsLaw 4 days ago ago

        Agreed! I've always been interested in the field of mathematics, only to be let down by my lack of ability to comprehend it. I can usually follow an article up until the point that it starts using formulae.

        I love this approachable prose.

        If anyone is aware of any other "mathematics for people who don't know mathematics" resources I'd greatly appreciate any links.

        • danabramov 4 days ago ago

          OK this is probably not quite what you meant but I'll shoot: I highly recommend Terence Tao's Analysis textbook (which now also has a Lean counterpart on GitHub). You can skip Chapter 1 (it sets up the motivation but I couldn't answer most questions, which is part of the point). From Chapter 2, it builds up in a somewhat "dry" but actually very accessible and methodical way. It is "mathematical" but it is "for people who don't know mathematics" in the sense that it forces you to build the entire mathematics from scratch, including proving things like `a + b = b + a` as exercises. This is actually how I got into proofs in the first place, with later picking up Lean by doing Natural Number Game.

          • GPerson 4 days ago ago

            Since you respect Terence Tao, but not the general population of mathematicians, maybe you’ll read his blog posts which describe the ways your actions are detrimental to human striving.

            • danabramov 3 days ago ago
              • GPerson 3 days ago ago

                You did not.

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

          • SturgeonsLaw 3 days ago ago

            Thanks, I'll have a read

      • Certhas 4 days ago ago

        Are you talking about the posted article? I agree that it was a fun read, but it did not present any mathematics at all. Like, none. Its not that the author not being an expert made it easy to understand, it's that there was nothing mathematical to understand presented.

    • patcon 4 days ago 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 4 days ago ago

        All this time, I've been considering myself the warlock. When, in fact, I've simply been the Imp. Dastardly news.

        • dodslaser 3 days ago ago

          It's goblins all the way down.

      • gbjcantab 4 days ago ago

        The same corollary occurred to me, as well!

      • dormento 4 days ago 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...)

    • baq 4 days ago ago

      I’ve felt like a warlock for about half a year now - talking to demons which summon code from the abyss. Exhilarating and terrifying, especially when you can tell the demons get better faster.

    • bwfan123 4 days ago ago

      > in which they themselves aren't quite able to validate whether the spell worked or not

      Knowledge is of 2 kinds: know-that and know-how. Know-that is what LLMs are enabling such as the proof here, while know-how is more useful as that constitutes understanding and puts that knowledge to use.

    • Xirdus 4 days ago ago

      The sorcerers have always outnumbered the wizards. Before AI, we called them code monkeys.

      • gbjcantab 4 days ago ago

        That’s fair! I think what struck me, though, is that what we’re seeing is large numbers of “wizards” jump ship to and actively promote “sorcery” instead, in this sense. That is, it’s interesting to me to see Dan Abramov, whose blog primarily consists of painstaking explanations of React internals based on the deep knowledge he developed over years as the most visible member of the core team, switch over to “do a breakthrough.”

        • danabramov 4 days ago ago

          I try to address this in the post explicitly in a few places.

          Primarily I thought of this as a sort of "epistemic performance art project", maybe similar to playing Elden Ring blindfolded having never played it before, or speedrunning a game by opening a box a thousand times and overflowing some counter. It's funny and absurd to do knowledge work without the knowledge.

          I think it's also a stress test of meta skills. Like, how much can we do without knowing? What kind of processes can we set up around these demons that would constrain them into our requirements? How can we know when things are going wrong? In some sense, this isn't too different from engineering management.

          Naturally, I'm also interested in how much of my role in this could've been automated away. Can there be a skill for that? Then "do a breakthrough" is an irrelevant implementation detail of that skill.

          Note that "do a breakthrough" actually produced the worst results over the runs. The best results were from more directed runs like searching for first obstacle towards the next milestone.

        • iamflimflam1 4 days ago ago

          This reminds me of Terry Pratchett’s Sourcery.

          The wizards don’t become sourcerers themselves - they become enthusiastic users of someone else’s sourcery. Their years of learning don’t protect them from mistaking access to power for mastery of it.

      • thesuitonym 4 days ago ago

        And before those code monkeys were making money, we called them skiddies.

        • Xirdus 3 days ago ago

          Script kiddies are hacking sorcerers. Different discipline.

    • adamddev1 4 days ago ago

      Or like the difference between chemistry and alchemy? Understanding and reasoning with the building blocks as opposed to throwing random stuff together, trying different things and hoping it somehow produces gold.

    • gchamonlive 4 days ago ago

      Differently than wizards that lock their knowledge in towers and in sects, software development has a tradition of being open for the most part, so the sorcery and wizardry analogy works more like a spectrum. It just depends on how close to the metal the apprentice would like their consciousness.

  • bwfan123 4 days ago 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

  • pretzellogician 4 days ago 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!

  • unholiness 4 days ago 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+surrea...

  • Feathercrown 4 days ago 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.

  • sigmar 4 days ago 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.

  • howunfortunate 4 days ago 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.

  • bonoboTP 4 days ago 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.

  • mihau 4 days ago ago
  • nphardon 4 days ago 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.

  • renyicircle 4 days ago 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.

  • rlue 4 days ago 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.

  • doctoboggan 4 days ago 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.

  • patcon 4 days ago ago

    Deeplinked reply from Prof Vincenzo Mantova[1], who is reviewing results: https://news.ycombinator.com/item?id=49761718

    [1] https://eps.leeds.ac.uk/maths/staff/4058/dr-vincenzo-l-manto...

  • undefined 4 days ago ago
    [deleted]
  • deiptx 4 days ago 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.

  • bastawhiz 4 days ago 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.

  • cubefox 4 days ago 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/

  • tuesdaynight 4 days ago ago

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

  • FiatLuxDave 4 days ago 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.

  • cyclopeanutopia 4 days ago ago

    Someone please vibe-prove that ZFC is inconsistent.

  • vatsachak 4 days ago 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

  • alikatyc 4 days ago ago

    free time spent talking to llm, what an achievement!

  • j2kun 4 days ago ago

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

  • msteffen 4 days ago ago

    I find this whole post fascinating in the context of https://news.ycombinator.com/item?id=49738091 and particularly this excerpt from Gowers:

    > Instead, I have a more complicated view, which I actually expressed in my essay The Two Cultures of Mathematics a quarter of a century ago, and which can be summarized by saying that there is a spectrum of attitudes in mathematics to the relationship between problem-solving and conceptual understanding. At one end of the spectrum you have mathematicians who are primarily motivated by the wish to solve problems, who see conceptual understanding as a very important means to that end. At the other you have mathematicians who are primarily motivated by the wish to attain conceptual understanding, who see problem-solving as a very important means to that end.

    Before, understanding and problem-solving-ability were so interdependent that distinguishing between the two was practically very difficult and probably wouldn’t have changed anyone’s research agenda. Now, they’re not connected, and this guy just did the ultimate meta-experiment of seriously undertaking a project that is intentionally 100% problem-solving and 0% understanding to prove it (maybe 99% and 1% but pretty close. In his transcripts, he never asks ChatGPT about the math, only about its opinions of the math).

    As we (as a society) sit around asking ourselves what mathematicians (and software engineers, and anyone in deep technical fields) should be doing all day, we now have this case study to show us how wide our range of options has become.

  • GPerson 4 days ago 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.

  • makerofthings 4 days ago 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.

  • fukaiall 4 days ago 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?

  • spongebobstoes 4 days ago 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

  • nialv7 4 days ago 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??

  • math_dandy 4 days ago ago

    [dead]

  • tonetheman 4 days ago ago

    [dead]

  • 31276ahq 4 days ago ago

    [flagged]

  • GPerson 4 days ago ago

    [flagged]