marcuschong•21d
Claim: GPT-5-pro can prove new interesting mathematicstwitter.com
161 comments
  • whymauri•18d

    I used to work at a drug discovery startup. A simple model generating directly from latent space 'discovered' some novel interactions that none of our medicinal chemists noticed e.g. it started biasing for a distribution of molecules that was totally unexpected for us.

    Our chemists were split: some argued it was an artifact, others dug deep and provided some reasoning as to why the generations were sound. Keep in mind, that was a non-reasoning, very early stage model with simple feedback mechanisms for structure and molecular properties.

    In the wet lab, the model turned out to be right. That was five years ago. My point is, the same moment that arrived for our chemists will be arriving soon for theoreticians.

    • wenc•17d

      A lot of interesting possibilities lie in latent space. For those unfamiliar, this means the underlying set of variables that drive everything else.

      For instance, you can put a thousand temperature sensors in a room, which give you 1000 temperature readouts. But all these temperature sensors are correlated, and if you project them down to latent space (using PCA or PLS if linear, projection to manifolds if nonlinear) you’ll create maybe 4 new latent variables (which are usually linear combinations of all other variables) that describe all the sensor readings (it’s a kind of compression). All you have to do then is control those 4 variables, not 1000.

      In the chemical space, there are thousands of possible combinations of process conditions and mixtures that produce certain characteristics, but when you project them down to latent variables, there are usually less than 10 variables that give you the properties you want. So if you want to create a new chemical, all you have to do is target those few variables. You want a new product with particular characteristics? Figure out how to get < 10 variables (not 1000s) to their targets, and you have a new product.

      • whymauri•17d

        At the end of the generative funnel we had a filter and it used (roughly) the mechanism you're describing.

        https://www.pnas.org/doi/10.1073/pnas.1611138113

        You summarized it very well!

        • adastra22•17d

          What do you do now? We are doing similar things to explore the surface chemistry involved in bootstrapping nanotechnology.

      • timClicks•17d

        It's been a while since I've played in the area, but is PCA still the go to method for dimensionality reduction?

        • wenc•17d

          PCA (essentially SVD) the one that makes the fewest assumptions. It still works really well if your data is (locally) linear and more or less Gaussian. PLS is the regression version of PCA.

          There are also nonlinear techniques. I’ve used UMAP and it’s excellent (particularly if your data approximately lies on a manifold).

          https://umap-learn.readthedocs.io/en/latest/

          The most general purpose deep learning dimensionality reduction technique is of course the autoencoder (easy to code in PyTorch). Unlike the above, it makes very few assumptions, but this also means you need a ton more data to train it.

          • ChadNauseam•17d

            > PCA (essentially SVD) the one that makes the fewest assumptions

            Do you mean it makes the *strongest* assumptions? "your data is (locally) linear and more or less Gaussian" seems like a fairly strong assumption. Sorry for the newb question as I'm not very familiar with this space.

            • wenc•17d

              You’re correct in a mathematical sense: linearity and Gaussian are restrictive assumptions.

              However I meant it colloquially in that those assumptions are trivially satisfied by many generating processes in the physical and engineering world, and there aren’t a whole lot of other requirements that need to be met.

        • Lerc•17d

          From 2019 but a decent overview by Leland McInnes https://www.youtube.com/watch?v=9iol3Lk6kyU

          There's a newer thing called PacMap which is an interesting thing that handles difference cases better. Not as robustly tested as UMAP but that could be said of any new thing. I'm a little wary that it might be overfitted to common test cases. To my mind it feels like PacMap seems like a partial solution of a better way of doing it.

          The three stage process of PacMap is either asking to be developed into either a continuous system or finding a analytical reason/way to conduct a phase change.

          • wenc•16d

            Leland McInnes is amazing. He's also the author of UMAP.

        • baq•17d

          PCA is nice if you know relationships are linear. You also want to be aware of TSNE and UMAP.

          • wenc•17d

            A lot of relationships are (locally) linear so this isn’t as restrictive as it might seem. Many real-life productionized applications are based on it. Like linear regression, it has its place.

            T-SNE is good for visualization and for seeing class separation, but in my experience, I haven’t found it to work for me for dimensionality reduction per se (maybe I’m missing something). For me, it’s more of a visualization tool.

            On that note, there’s a new algorithm that improves on T-SNE called PaCMAP which preserves local and global structures better. https://github.com/YingfanWang/PaCMAP

            • a_bonobo•17d

              There's also Bonsai, it's parameter-free and supposedly 'better' than t-SNE, but it's clearly aimed at visualisation purposes (except that in Bonsai trees, distances between nodes are 'real' which is usually not the case in t-SNE)

              https://www.biorxiv.org/content/10.1101/2025.05.08.652944v1....

            • energy123•17d

              I'd add that PCA/OLS is linear in the functional form (linear combination), but the input variables can be non-linear (X_new := X_{old,1}*X_{old,2}^2), so if the non-linearities are simple, then basic feature engineering to strip out the non-linearities before fitting PCA/OLS may be acceptable.

      • siavosh•17d

        In terms of terminology, is it accurate to interpret the latent variables as the “world model” of the neural network?

        • wenc•16d

          Not quite.

          Embeddings are a form of latent variables.

          Attention query/key/value vectors are latent variables.

          More generally, a latent variable is any internal, not-directly-observed representation that compresses or restructures information from inputs into a form useful for producing outputs.

          They usually capture some underlying behavior in either lower dimensional or otherwise compressed space.

        • pk-protect-ai•17d

          How about "bias vector space"?

    • svantana•17d

      Interesting! Depending on your definition, "automated invention" has been a thing since at least the 1990's. An early success was the evolved antenna [1].

      1. https://en.wikipedia.org/wiki/Evolved_antenna

      • hhh•17d

        IBM has done this with pharmaceuticals for ages no? That’s why they have patents on what would be the next generation of ADHD medications e.g. 4F-MPH?

        • johnisgood•17d

          4F-* are mainly research chemicals (still?), still being sold widely, especially where there is not a blanket ban on them.

          I remember 3-FPM, that was what I imagined stimulants should be doing. It did everything just right. I got it back when it was legal. Any other stimulants come nowhere as close, maybe similar ones, but 4FA or whatever is for example, mostly euphoric, which is not what I want.

          No clue about IBM's part in it.

    • kmarc•17d

      Reminds me of this story on the Babbage podcast a month ago:

      https://www.economist.com/science-and-technology/2025/07/02/...

      My understanding is, iterating on possible sequences (of codons, base pairs, etc) is exactly what LLMs, these feedback-looped predictor machines, are especially great at. With the newest models, those that "reason about" (check) their own output, are even better at it.

    • apimade•17d

      Warning the below comment comes from someone who has no formal science degree, and just enjoys reading articles on the topic.

      Similar for physicists, I think there’s a very confusing/unconventional antenna called the “evolved antenna” which was used on a NASA spacecraft. The idea behind it was supported from genetic programming. The science or understanding “why” the way the antenna bends at different areas supporting increased gain is not well understood by us today.

      This all boils down to empirical reasoning, which underlies the vast majority of science (or science adjacent fields like software engineering, social sciences etc).

      The question I guess is; does LLMs, “AI”, ML give us better hypothesis or tests to run to support empirical evidence-based science breakthroughs? The answer is yes.

      Will these be substantial, meaningful or create significant improvements on today’s approaches?

      I can’t wait to find out!

    • pojzon•17d

      If AI comes up with new drugs or treatments - does it mean its a public knowledge and cant be copyrighted ?

      Wouldnt that mean a fall of US pharmaceutical conglomate based on current laws about copyright and AI content?

      • jillesvangurp•17d

        You are confusing copyright and patents, which are two very different things. And yes, companies or people wielding AIs can patent anything that hasn't been claimed by others before.

        • pojzon•17d

          But how can you patent something that was created by AI that cannot take ownership of anything and different AIs can produce the same result.

          Is achieving the same result using different engines the same as designing combustion engine in different ways?

          How public domain translate to that?

          I really hope it kills any ways to claim patents on anything.

      • selkin•17d

        Drugs discovered by humans are not under the protections of copyright as well.

    • ACCount37•17d

      Hallucinations or inhuman intuition? An obvious mistake made by a flawed machine that doesn't know the limits of its knowledge? Or a subtle pattern, a hundred scattered dots that were never connected by a human mind?

      You never quite know.

      Right now, it's mostly the former. I fully expect the latter to become more and more common as the performance of AI systems improves.

    • brandonb•17d

      This is really cool. Have you (or your colleagues) written anything about what you learned about ML for drug discovery?

    • lukev•17d

      Ok but I have to point out something important here. Presumably, the model you're talking about was trained on chemical/drug inputs. So it models a space of chemical interactions, which means insights could be plausible.

      GPT-5 (and other LLMs) are by definition language models and though they will happily spew tokens about whatever you ask, they don't necessarily have the training data to properly encode the latent space of (e.g) drug interactions.

      Confusing these two concepts could be deadly.

      • Difwif•17d

        Seems short sighted to me. LLMs could have any data in their training set encoded as tokens. Either new specialized tokens are explicitly included (e.g: Vision models) or the language encoded version of everything that usually exists (e.g: the research paper and the csv with the data).

        To improve next token prediction performance on these datasets and generalize requires a much richer latent space. I think it could theoretically lead to better results from cross-domain connections (ex: being fluent in a specific area of advanced mathematics, quantum mechanics, and materials engineering is key to a particular breakthrough)

        • anthk•16d

          Then you are now implementing a parser.

  • freshtake•18d

    An interesting debate!

    A few things to consider:

    1. This is one example. How many other attempts did the person try that failed to be useful, accurate, coherent? The author is an OpenAI employee IIUC, so it begs this question. Sora's demos were amazing until you tried it, and realized it took 50 attempts to get a usable clip.

    2. The author noted that humans had updated their own research in April 2025 with an improved solution. For cases where we detect signs of superior behavior, we need to start publishing the thought process (reasoning steps, inference cycles, tools used, etc.). Otherwise it's impossible to know whether this used a specialty model, had access to the more recent paper, or in other ways got lucky. Without detailed proof it's becoming harder to separate legitimate findings from marketing posts (not suggesting this specific case was a pure marketing post)

    3. Points 1 and 2 would help with reproducibility, which is important for scientific rigor. If we give Claude the same tools and inputs, will it perform just as well? This would help the community understand if GPT-5 is novel, or if the novelty is in how the user is prompting it

    • hodgehog11•17d

      I don't mean to be cynical, but I don't think these points matter as much as you think, at least not in practice. The hardest part of a proof is working out the intermediate steps; joining them up is often trivial, even for a student. So even if it works out a few good steps or finds an effective theorem to apply, and does so only every one in a hundred prompts, the time savings can be significant.

      I should know, I've been using LLM thinking models to help brainstorm ideas for stickier proofs. It's been more successful at discovering esoteric entry points than I would like to admit.

    • bawolff•17d

      > This is one example. How many other attempts did the person try that failed to be useful, accurate, coherent? The author is an OpenAI employee IIUC, so it begs this question. Sora's demos were amazing until you tried it, and realized it took 50 attempts to get a usable clip.

      If you could combine this with automated theorem proving, it wouldn't matter if it was right only 1 out of a 1000 times.

      • hto2i34334324•17d

        The most difficult part of automated theorem proving is not the "tactic" part, but actually in the formulation.

        (Theory building is quite hard in math; the computation side is only hard after a point).

      • tshaddox•17d

        Perhaps 1/1000 would be a useful rate, but numbers go a lot smaller than 1/1000.

    • foobarqux•17d

      > This is one example. How many other attempts did the person try that failed to be useful, accurate, coherent?

      High chance given that this is the same guy that came up with SVG unicorn (sparks of AGI) which raises the same question even more obviously.

    • energy123•18d

      4. How many times has this happened already but the human took credit for the output because they don't have the incentive to give credit to the LLM

      • sothatsit•17d

        I'd say a lot of people even have an incentive to not give credit to the LLMs, because there is a social stigma associated with using AI, due to its association with low-quality work.

        • qingcharles•17d

          I'm guessing the music business right now is absolutely awash with unreported and uncredited AI lyrics and backing tracks. It's an area where you can get away with it a lot easier than in the visual arts.

        • ninetyninenine•17d

          People are delusional. There’s a large cohort of folks on HN who still think AI is just a stochastic parrot. Depending on the topic or the thread you’ll find more of those people and get voted down if you even imply that LLMs can reason.

          • hnfong•17d

            I think many humans are stochastic parrots, so in a sense those parrots are damn right.

            • throwawaymaths•17d

              why "many" why not "all"?

              • hnfong•17d

                Obviously I'm not a stochastic parrot :P

                • throwawaymaths•16d

                  sounds like something a stochastic parrot like me would say

            • ninetyninenine•17d

              My claim is the LLM is not a stochastic parrot. So technically they're wrong. But of course I understand your point.

              • sothatsit•16d

                They are to some extent though. The bigger point is that they are not just a stochastic parrot. But examples like the modified riddles where they just answer the original riddle shows that they have the behaviour of stochastic parrots at least some of the time.

                • ninetyninenine•16d

                  Yeah you're right. I guess that's the spirit of my intent, to say they are more than stochastic parrots... a behavior they, like humans, exhibit sometimes

      • ds-slope•17d

        I don’t think it’s that they don’t have the incentive. I think it’s because it’s unclear if you give credit to the LLM if that means that OpenAI or similar would be considered an author in which case that could really screw up intellectual property and make using LLMs much less attractive. If the LLM wants attribution then it’s sentient, and if it’s sentient, it may be given personhood (Johnny-five scenario) and get rights, and then it would be a writer, and it could influence the license and intellectual property may belong partially to it unless it willingly became and employee of a ton of companies and organizations or contracted with them.

      • OtomotO•18d

        [flagged]

  • aabhay•18d

    I don’t get why so many people are resistant to the concept that AI can prove new mathematical theorems.

    The entire field of math is fractal-like. There are many, many low hanging fruits everywhere. Much of it is rote and not life changing. A big part of doing “interesting” math is picking what to work on.

    A more important test is to give an AI access to the entire history of math and have it _decide_ what to work on, and then judge it for both picking an interesting problem and finding a novel solution.

    • trueismywork•17d

      People are not resistant to that concept. People are resistant to OpenAI making ehse claims without proper science practices.

      https://mathstodon.xyz/@tao/114881418225852441

      https://mashable.com/article/openai-claims-gold-medal-perfor...

      Note that no one expressed skepticism of what google said when they claimed they achieved gold medal. But no one is willing to believe OpenAI.

    • ComplexSystems•17d

      People are resistant because:

      1. There's this huge misconception that LLMs are literally just memorizing stuff and repeating patterns from their training data 2. People glamorize math and feel like advancements in it would "be AGI"

      They don't realize that having it generate "new math" is not much harder than having it generate "new programs." Instead of writing something in Python, it's writing something in Lean.

      • 0points•16d

        > 1. There's this huge misconception that LLMs are literally just memorizing stuff and repeating patterns from their training data

        So then, what are they doing?

        I'm seeing people creating full apps with GPT-5-pro, but nothing is novel.

        Just discussed the "impressiveness" of it creating a gameboy emulator from scratch.

        (There's over 3500 gameboy emulators on github. I would be suprised if it failed to produce a solution with that much training data).

        Where's the novel break-throughs?

        As it stands today, I'm sure it can produce a new ssl implementation or whatever it has been trained on, but to what benefit???

      • marliechiller•17d

        >1. There's this huge misconception that LLMs are literally just memorizing stuff and repeating patterns from their training data

        For a lay person, what are they actually doing instead?

        • nearbuy•16d

          They can learn to generalize patterns during training and develop some model of the world. So for example, if you were to train an LLM on chess games, it would likely develop an internal model of the chess board. Then when someone plays chess with it and gives a move like Nf3, it can use that internal model to help it reason about its next move.

          Or if you ask it, "what is the capital of the state that has the city Dallas?", it understands the relations and can internally reason through the two step process of Dallas is in Texas -> the capital of Texas is Austin. A simple n-gram model may occasionally get questions like that right by a lucky guess (though usually not) while we can see experimentally the LLM is actually applying the proper reasoning to the question.

          You can say this is all just advanced applications of memorizing and predicting patterns, but you would have to use a broad definition of "predicting patterns" that would likely include human learning. People who declare LLMs are just glorified auto-complete are usually trying to imply they are unable to "truly" reason at all.

        • dcre•17d

          I don't think anyone really knows, but I also don't think it's quite an either/or. To me a more interesting way to put the question is to ask what it would mean to say that GPT-5 is just applying patterns from its training data when it finds bugs in 1000 lines of new Rust code that were missed by multiple human reviewers. "Applying a memorized pattern" seems well-defined because it is an everyday concept but I don't think it really is well-defined. If the bug "fits a pattern" but is expressed in a different programming language, with different variable names, different context, etc., recognizing that and applying the pattern doesn't seem to me like a merely mechanical process.

          Kant has an argument in the Critique of Pure Reason that reason cannot be reducible to the application of rules, because in order to apply rule A to a situation, you would need a rule B to follow for applying rule A, and a rule C for applying rule B, and this is an infinite regress. I think the same is true here: any reasonable characterization of "applying a pattern" that would succeed at reducing what LLMs do to something mechanical is vulnerable to the regress argument.

          In short: even if you want to say it's pattern matching, retrieving a pattern and applying it requires something a lot closer to intelligence than the phrase makes it sound.

        • ComplexSystems•15d

          First: while it's not technically incorrect to say that they're learning "patterns" in the training data, the word "pattern" here is extremely deep and hides a ton of detail. These aren't simple n-grams like "if the last N tokens were ___, then ___ follows." To generate fluent conversation, new code, or poetry, the model must learn highly abstract structures that start to resemble reasoning, inference, and world-modeling. You can't predict tokens well without starting to build these higher-level capabilities on some level.

          Second: Generative AI is about approximating an unknown data distribution. Every dataset - text, images, video - is treated as a sample from such a distribution. Success depends entirely on the model's ability to generalize outside the training set. For example, "This Person Does Not Exist" (https://this-person-does-not-exist.com/en) was trained on a data set of 1024x1024 RGB images. Each image can be thought of as a vector in a 1024x1024x3 = 3145728-dimensional space, and since all coefficients are in [0,1], these vectors are all in the interior of a 3145728-dimensional hypercube. But almost all points in that hypercube are going to be random noise that doesn't look like a person. The ones that do will be on a lower-dimensional manifold embedded in the hypercube. The goal of these models is to infer this manifold is from the training data, and generate a random point on it.

          Third: Models do what they're trained to do. Next-token prediction is one of those things, but not the whole story. A model that literally did just memorize exact fragments would not be able to zero-shot new code examples at all. That is, the transformer architecture would have learned some nonlinear transformation that is only good at repeating exact fragments. Instead, they spend a ton of time training it to get good at generalizing to new things, and it learns whatever other nonlinear transformation makes it good at doing that instead.

        • corimaith•17d

          The definition of a language model is literally the probability distribution of the most likely next token given a preceding text. When OP says "memorizing patterns and repeating stuff", it's a strawman of a basic n-gram model, obviously with modern language it's more advanced because we techniques like vector tokenization, but at it's core it's still just probability that's limited to the corpus it was trained on.

          Or at it's core, if you give it question that it's never seen, what's the most likely reply you might get, and it will give you that. But dosen't mean there is a internal world-model or anything, it's ultimately wether you think language is sufficient to model reality, which I probably think not. It obviously would be very convincing, but not necessairly correct.

          • nearbuy•16d

            This isn't true at all. The LLMs absolutely world model and researchers have shown this many times on smaller language models.

            > techniques like vector tokenization

            (I assume you're talking about the input embedding.) This is really not an important part of what gives LLMs their power. The core is that you have a large scale artificial neural net. This is very different than an n-gram model and is probably capable of figuring out anything a human can figure out given sufficient scale and the right weights. We don't have that yet in practice, but it's not due to a theoretical limitation of ANNs.

            > probability distribution of the most likely next token given a preceding text.

            What you're talking about is an autoregressive model. That's more of an implementation detail. There are other kinds of LLMs.

            I think talking about how it's just predicting the next token is misleading. It's implying it's not reasoning, not world-modeling, or is somehow limited. Reasoning is predicting, and predicting well requires world-modeling.

            • corimaith•15d

              >This is really not an important part of what gives LLMs their power. The core is that you have a large scale artificial neural net.

              What seperates transformers from LSTMs is their ability to proccess the entire corpus in parallel rather in-sequence and the inclusion of the more efficient "attention" mechanism that allows them to pick up long range dependencies across a language. We don't actually understand the full nature of the latter, but I suspect that is the basis behind the more "intelligent" actions of the LLM. There's quite a general range of problems that a long-range-dependency was encompass, but that's still ultimately limited by language itself.

              But if you're talking about this being a fundamentally a probability distribution model, I stand by that, because that's literally the mathematical model (softmax for the encoder and decoder) that's being used in transformers here. It very much is generating a probability distribution over the vocabulary and just picking the highest probability (or beam search) as your next output.

              >The LLMs absolutely world model and researchers have shown this many times on smaller language models.

              We don't have a formal semantic definition of a "world model", I would take alot of what these researchers are writing with a grain of salt because something like that crosses more into philosophy (especially in the limits of language and logic) than hard engineering that these researchers are trained on.

        • whalee•17d

          This question becomes difficult whenever a system becomes sufficiently complex. Take any chaotic system, like a double pendulum, and press play at step 100,000. You ask 'what is it doing'? Well, it's just applying it's rule. Step to step.

          Zoom out and look at it's trajectory over those 100,00 steps and ask again.

          The answer is something alien. Probabilistically it is certain the description of its behavior is not going to exist in a space we as humans can understand. Maybe if we were god beings we could say 'No no, you see the behavior of the double pendulum isn't seemingly random, you just have to look at it like this'. Encryption is a decent analogy here.

          We're fooled into thinking we can understand these systems because we forced them to speak English. Under the hood is a different story.

      • martin-t•17d

        1) They absolutely do sometimes repeat training data verbatim.[0]

        2) That's not even the point. The point is being trained on stolen data without permission, pretending that the resulting model of the training data is not a derived work of the training data and that the output of the model plus a prompt is not derived work of the training data.

        Point 1 is just an extreme edge case which is a symptom of point 2 and yet people still have trouble accepting it.

        GPL was about user freedom and now if derived work no longer applies as long as you run code through a sufficiently complex plagiarism automator, plagiarism is unprovable and GPL is broken. Great, we lost another freedom.

        [0]: I recall a study or court document with 100 examples of plagiarising multiple whole paragraphs from the New York Times, don't have time to look for it now

        • fkyoureadthedoc•17d

          > I recall a study or court document with 100 examples of plagiarising multiple whole paragraphs from the New York Times, don't have time to look for it now

          Convenient. Well then, I recall two studies that said the opposite. Unfortunately pressed for time as well.

        • JanisErdmanis•17d

          > trained on stolen data without permission

          My sympathies to academic publishers ;)

        • ComplexSystems•16d

          This all seems totally orthogonal to the statement: "I don't get why people are so resistant to the idea that AI can prove new mathematical theorems."

          I don't necessarily disagree about the copyleft stuff.

          Transformers do sometimes overfit to exact token sequences from training data, but that isn't really what they the architecture does in general.

          • martin-t•16d

            When you say new mathematical theorems, they absolutely can. So can infinite monkeys on typewriters, though LLMs have a much better heuristic to arrive at valid trheorems.

            The same applies to valid new programs.

            The issue I have with this is pretending that the word "new" is sufficient justification for giving all the credit/attribution and subsequent reward (reputational, financial, etc.) to the person who wrote the prompt instead of distributing it to the people in the whole chain of work according to how much work and what quality of work they did.

            How many man-hours did it take to create the training data? How many to create the LLM training algorithm and the electricity to run it? How many to write the prompts?

            The most work by many, many orders of magnitude was put in by the first group. They often did it with altruistic goals in mind and released their work under permissive or copyleft licenses.

            And now somebody found a way to monetize this effort without giving them anything in return. In fact, they will have to pay to access the LLMs which are based on their own work.

            Copyright or plagiarism are perhaps the wrong terms to use when talking about it. I think copyright should absolutely apply but it was designed to protect creative works, not code in the first place.

            Either way it's a form of industrialized exploitation and we should use all available tools to defend against it.

        • danielbarla•17d

          You're completely correct in your two points, however people _do_ regularly assert that LLMs cannot possibly generate anything novel: "they are just regurgitating and recombining the original".

          I mean, sure. But so am I (in what is likely a far more advanced manner, but still). I also find it somewhat funny that I am also partially trained on stolen data without permission. I also jaywalk occasionally (perhaps I am trivializing the topic too much, but show me a researcher who hasn't _once_ downloaded a paper they really needed, in less than perfectly legal ways).

          • martin-t•16d

            Human time is valuable, LLM time is not. If you spend hundreds of hours creating something, nobody should have the right to copy (verbatim or with automatic modifications) it unless you allow them.

            Human rights are valuable. LLMs allow laundering GPL code (removing both attribution and users' rights to inspect and modify the code). Free software cannot compete against proprietary in a world where making a copy is trivial but proving it's a copy is nearly impossible.

    • foobarqux•17d

      As others have said computers already help prove theorems like the four color theorem. It’s not that shocking that LLMs can prove a relative handful of obscure theorems. An alpha-theorem (neural net directed “brute force” search) type system will probably also be able to prove some theorems. There is no evidence today that there will be a massive breakthrough in math due to those systems let alone through LLM type systems.

      If LLMs were already a breakthrough in proving theorems, even for obscure minor theorems, there would be a massive increase in published papers due to publish or perish academic incentives.

    • SkyPuncher•17d

      For me it comes down to signal vs noise.

      I’m absolutely confident that AI/LLM can solve things, but you have to shift through a lot of crap to get there. Even further, it seems AI/LLM tend to solve novel problems in very unconventional ways. It can be very hard to know if an attempt is doomed, or just one step away from magic.

      • teeray•17d

        At that point, is it really solving or is it just monkeys with typewriters?

        • fwip•17d

          "Monkeys with typewriters," is in one sense, a uniform sampling of the probability space. A brute-force search, even when using structured proof assistants, take a very long time to find any hard proof, because the possibility space is roughly (number of terms) raised to the power of (length of the proof).

          But similarly to how a computer plays chess, using heuristics to narrow down a vast search space into tractable options, LLMs have the potential to be a smarter way to narrow that search space to find proofs. The big question is whether these heuristics are useful enough, and the proofs they can find valuable enough, to make it worth the effort.

        • naasking•17d

          I think the signal-to-noise is demonstrably higher with AI than with a legion of monkeys on typewriters. I think an interesting philosophical question is, is there some threshold of signal-to-noise that by itself would qualify a system as "intelligent", or is "intelligence" some specific property of the search process itself? eg. perhaps real intelligence avoids certain pitfalls, like getting stuck in local minima.

        • marmakoide•17d

          It's stochastic monkeys, but enhanced with a really good bias towards coherent prose, built upon a gigantic corpus.

          • 0points•16d

            So, it's monkeys specifically good at typing Shakespeare.

        • myaccountonhn•17d

          Or finding the solution hidden somewhere among the decimals of pi.

      • •17d
        [deleted]
    • hto2i34334324•17d

      That's not the issue. The issue has always been that of knowledge and epistemology.

      This is why the computer-assisted proof of the four-color theorem was such a talking point in math/cs-circles: how do you "really" know what was proven. This is slightly different from say an advisor who trains his students : you can often sketch out a proof, even though the details require quite a bit of work.

    • xenotux•18d

      I think a simple way to take emotion out of this is to ask if a computer can beat humans at math. The answer to that is pretty much "duh". Symbolic solvers and numerical methods outperform humans by a wide margin and allow us to reach fundamentally new frontiers in mathematics.

      But it's a separate question of whether this is a good example of that. I think there is a certain dishonesty in the tagline. "I asked a computer to improve on the state-of-the-art and it did!". With a buried footnote that the benchmark wasn't actually state-of-the-art, and that an improved solution was already known (albeit structured a bit differently).

      When you're solving already-solved problems, it's hard to avoid bias, even just in how you ask the question and otherwise nudge the model. I see it a lot in my field: researchers publish revolutionary results that, upon closer inspection, work only for their known-outcome test cases and not much else.

      Another piece of info we're not getting: why this particular, seemingly obscure problem? Is there something special about it, or is it data dredging (i.e., we tried 1,000 papers and this is the only one where it worked)?

    • _Algernon_•17d

      A monkey hammering gibberish on a keyboard can prove new math given sufficient time. That's a low bar to set. The question is if the signal-to-noise ratio is high enough for it to be worthwhile.

    • tcshit•18d

      I like the idea of letting AI try to formulate new math problems that are interesting, i.e. worthy research level. I guess we are still a number of iterations away till AI get there though..

    • throwawaymaths•17d

      or, just put AI on the collatz conjecture.

    • ninetyninenine•17d

      There are more programmers resistant to the concept of AI because of pride.

      Programmers take pride in their ability to program and to reduce their own abilities into an algorithm reproducible by an LLM is both an attack on their pride and an attack on their livelihood.

      It’s the same reason why artists say AI art is utter crap when in a blind folded test they usually won’t be able to tell the difference.

      • •17d
        [deleted]
  • drudolph914•21d

    interesting if true, but this isn't the first time we heard of something like this

    quanta published an article that talked about a physics lab asking chatGPT to help come up with a way to perform an experiment, and chatGPT _magically_ came up with an answer worth pursuing. but what actually happened was chatGPT was referencing papers that basically went unread from lesser famous labs/researchers

    this is amazing that chatGPT can do something like that, but `referencing data` != `deriving theorems` and the person posting this shouldn't just claim "chatGPT derived a better bound" in a proof, and should first do a really thorough check if it's possible this information could've just ended up in the training data

    • martinpw•18d

      > what actually happened was chatGPT was referencing papers that basically went unread from lesser famous labs/researchers

      Which is actually huge. Reviewing and surfacing all the relevant research out there that we are just not aware of would likely have at least as much impact as some truly novel thing that it can come up with.

      • DennisP•17d

        Maybe we should think of current AIs as not so much artificial intelligence, as collective intelligence. Which itself can be extremely valuable.

        • melagonster•17d

          No, this is not permitted. Until today, the world agreed that the product always belongs to the creator or user of LLMs.

      • xigoi•17d

        It turns out that if you use a fancy search engine to search instead of pretending that it’s intelligent, it will actually be good at its job. Who would have guessed?

    • leeoniya•18d

      > but what actually happened was chatGPT was referencing papers that basically went unread from lesser famous labs/researchers

      now let's invalidate probably 70% of all patents

      • jsw97•17d

        I know this was a throwaway, but finding prior art for a large group of existing patents would be a cool application.

    • mhh__•18d

      How would we know it was referencing an old paper versus almost everything trivial already having a derivation somewhere?

      • fwip•17d

        One signal is to check the journal. Most reputable journals won't publish a paper claiming a new technique if it's actually trivial and well-known.

        • mhh__•17d

          The "trivial" is slightly tongue in cheek. It must be trivial, I've just shown it!

  • krnsll•17d

    If you think of this as a search, retrieval and “application” problem on the space of convex optimization proof techniques, it’s not a particularly striking result to a mathematician. Partly because: the space of results/techniques and crucially applications of those results and proof techniques is very rich (it’s an active field with many follow up papers).

    On the other hand, I have a collection of unpublished results in less active fields that I’ve tested every frontier model on (publicly accessible and otherwise) and each time the models have failed to solve them. Some of these are simply reformulations of results in the literature that the models are unable to find/connect which is what leads me to formulate this as a search problem with the space not being densely populated enough in this case (in terms of activity in these subfields).

  • nybsjytm•21d

    Any mathematicians who have actually called it "new interesting mathematics", or just an OpenAI employee?

    The paper in question is an arxiv preprint whose first author seems to be an undergraduate. The theorem in it which GPT improves upon is perfectly nice, there are thousands of mathematicians who could have proved it had they been inclined to. AI has already solved much harder math problems than this.

    • offnominal•17d

      The OpenAI employee posting this is a well known theoretical computer scientist: https://en.wikipedia.org/wiki/S%C3%A9bastien_Bubeck

      • alkyon•17d

        Yes, he published a paper claiming GPT-4 has "sparks" of AGI. What else is he known for in the field of computer science?

        https://arxiv.org/abs/2303.12712

        • NotOscarWilde•17d

          Hello, TCS assistant professor here: he is legitimately respected among his peers.

          Of course, because I am a selfish person, I'd say I appreciate most his work on convex body chasing (see "Competitively chasing convex bodies" on the Wikipedia link), because it follows up on some of my work.

          Objectively, you should check his conference submission record, it will be a huge number of A*/A CORE rank conferences, which means the best possible in TCS. Or the prizes section on Wikipedia.

          • alkyon•17d

            I don't deny that his output is highly valued among AI researchers.

            Provocative as my question may be, the point I wanted to make is that his most highly cited paper that I already mentioned is suspiciously very in line with the OpenAI narrative. I doubt if any of his GPT research is really independent. With great salary comes great responsibility.

        • offnominal•17d

          Not sure if you're trying to be provocative, but you could just click his name in the link you provided to find a lengthy list of arXiv preprints: https://arxiv.org/search/cs?searchtype=author&query=Bubeck,+...

      • nybsjytm•16d

        Not sure what this has to do with my post.

        • offnominal•16d

          > Any mathematicians who have actually called it "new interesting mathematics", or just an OpenAI employee?

          He is a mathematician. Unless you wanted to say "any other mathematicians..."

  • marcuschong•21d

    More comments from another mathematician:

    https://x.com/ErnestRyu/status/1958408925864403068?t=QmTqOcx...

  • hodgehog11•17d

    I'm not sure why this is surprising or newsworthy; it has been this way ever since o3. I guess few people noticed.

    There are a few masters-level publishable research problems that I have tried with LLMs on thinking mode, and it had produced a nearly complete proof before we had a chance to publish it. Like the problem stated here, these won't set the world on fire, but they do chip away at more meaningful things.

    It often doesn't produce a completely correct proof (it's a matter of luck whether it nails a perfect proof), but it very often does enough that even a less competent student can fill in the blanks and fix up the errors. After all, the hardest part of a proof is knowing which tools to employ, especially when those tools can be esoteric.

  • shaldengeki•17d

    Further in the thread, the guy notes that this isn't "new" mathematics - a better proof with tighter bounds was published in April:

    https://xcancel.com/SebastienBubeck/status/19581986678373298...

  • poulpy123•17d

    Claim: publish a paper in one of the best mathematical journal instead of a twitter thread

  • lewhoo•17d

    "Now the only reason why I won't post this as an arxiv note, is that the humans actually beat gpt-5 to the punch :-). Namely the arxiv paper has a v2 arxiv.org/pdf/2503.10138v2 with an additional author and they closed the gap completely, showing that 1.75/L is the tight bound."

    I really don't know what to make of this. The conclusion is that a model could still do this without the paper containing the exact info on how to do this ?

  • dinobones•21d

    Are we sure this guy is not someone being mirrored by a recursive non-governmental system?

    Context: https://x.com/GeoffLewisOrg/status/1945864963374887401

    • internet_points•17d

      https://knowyourmeme.com/memes/geoff-lewis-scp-foundation-cy...

    • aeve890•18d

      What does this even mean? This read like a SCP thing.

      • semi-extrinsic•18d

        It is exactly SCP regurgitated by the LLM, and this guy thinks it's all true.

      • IceDane•18d

        This is either satire that's over my head or mental illness.

        • StilesCrisis•18d

          This is one of 4o’s biggest flaws. If you are a conspiracy theorist, it’ll confirm any outlandish theory you can come up with, and provide invented receipts to go with it. Of course, it’s just model hallucinations, but for those who are already primed to believe that secrets are being kept, it gives the “evidence” they were always looking for.

          • the_sleaze_•17d

            "Your correction is correct! Jet fuel can "melt" steel beams because steel is a solid metal that requires heating to its melting point (around -30°C) to transform into a liquid..."

    • ofjcihen•17d

      Lmao, I love it. Is this the new Q-Anon?

  • phoenixhaber•17d

    So this looks like a useful use case for a mcp pipeline. You have a set of agents that are designed to look through the mathematics to discover what is useful, you then pipeline over to a set of agents that are distinguished by having training data on sets of mathematical fields, you have cross check proof agents, and then you have connections between fields agents. You see if you can use connections across mathematics through Wikipedia to crawl through the math and see if there's a correspondence between citations or links between proofs and their mathematical interdependence. Then you can start building trees and see if you can make righter linkages between set theory and number theory or topology or something.then see if you can get closer to a total theory or universal theory of mathematics (or prove it doesn't exist). If you can do that by just throwing money at it why not? It might be able to come up with all sorts of applications in the real world just byd default.

  • osti•21d

    In here https://blog.google/products/gemini/gemini-2-5-deep-think/, the professor google worked with also claimed proving some previously unproven conjecture.

  • 42lux•18d

    I guess arithmetic is just harder for an LLM than higher math.

    • bubblyworld•18d

      Arithmetic is harder for mathematicians than higher maths too =P not even joking. It was a meme in my university's maths dept for a reason.

      • pessimizer•17d

        I was pretty famous in college for getting the problems right on exams while I was working symbolically, and right before the final answer failing at integer division or subtraction. Professors/TAs would still give you full credit though, maybe penalize you a point or something.

      • emmelaich•17d

        https://en.wikipedia.org/wiki/57_(number)

        aka the Grothendieck prime!

      • PartiallyTyped•18d

        In a group, you’d usually let the freshest handle splitting the bill because everyone else forgot arithmetic.

      • therobots927•18d

        it might take a while but their answer would always be correct. the same cannot be said for LLMs.

        • soulofmischief•18d

          Mathematicians make calculations in their errors all the time.

        • bubblyworld•18d

          Yeah, of course I agree with that =)

    • stevenhuang•17d

      Relevant post here that demonstrates this idea, 2022

      Bad at arithmetic, promising at math: https://www.lesswrong.com/posts/qy5dF7bQcFjSKaW58/bad-at-ari...

  • corford•17d

    If you want a great book on the history of financial speculation, Devil Take the Hindmost (https://www.amazon.com/dp/0452281806/) is a strong recommendation.

  • starchild3001•17d

    Hypothesis: If you had ~1M dollar to burn, I think we should try setting up an AI agent to explore and try to invent new mathematics. It turns out agents can get an IMO gold with Gemini 2.5 Pro production model only. Therefore I suspect a swarm of agents burning through tokens like there's no tomorrow can invent new math.

    Reference: https://arxiv.org/abs/2507.15855

    Alternative: If Gemini Deep Think or GPT5-Pro people are listening, I think they should give free access to their models with potential scaffolding (ie. agentic workflow) to say some ~100 researchers to see if any of them can prove new math with their technology.

  • d4rkn0d3z•17d

    "Claim: GPT-5-pro can prove new interesting mathematics"

    s/prove/produce/g

    I'm inclined to regard an LLM as modelling a collection of fuzzy production rules which occur in a hierarchical collection of semi-formal systems; an LLM attempts to produce typographically correct theorems, the proving occurs at the level of semantics. Meaning requires a mind to erect an isomorphic mapping which the LLM is not capable of. In other words, for the LLM the math is just symbols on a page that are arranged according to the typographic rules which it has an imperfect model of. On this view, nothing about what is happening with Gen AI is particularly surprising or novel.

  • eru•17d

    Alas, GPT-5 Pro (and friends) will also happily and confidently give you nonsense proofs of supposed theorems.

    But yes, it's getting better and better.

  • EcommerceFlow•17d

    The coolest part about this IMO is they used the same model we all have access to (GPT5-Pro), and not some secret invite only model.

  • trueismywork•17d

    More nuanced take

    https://x.com/ErnestRyu/status/1958408925864403068?t=dAKXWtt...

  • strangescript•18d

    It can't reason -> It can't make new discoveries -> It can only tie together bespoke missed data -> It can make some basic discoveries -> ??????

    • ACCount37•17d

      It doesn't outsmart the entirety of humankind combined, so it's not actually intelligent. Duh.

  • croes•17d

    I wanted to know how to set the environment variables for CGI in IIS. The GPT 5 thoughts made a totally unrelated picture and then gave the wrong answer.

  • yapyap•17d

    Claim: a randomizer can prove new mathematics as long as you keep checking every single one

  • chiengineer•21d

    [dead]

  • aaron695•21d

    [dead]

  • sachinaag•17d

    [dead]

  • rationalfaith•18d

    [dead]

  • animanoir•21d

    [dead]

  • mikert89•17d

    [flagged]

    • sunrunner•17d

      What are these higher modes? I'm very excited to hear about them.

    • bgwalter•17d

      Yes, that is why the chess world championship allows Stockfish assistance in order to democratize chess.

      • esyir•17d

        The big difference is that chess is a game/sport, and those are about competition between humans. It's a deliberately restricted ruleset to encourage such, thus the (imperfect) banning of assistance.

        The same doesn't really apply to everything outside of that.

        Still, you'd think that status would still remain, it's not like the invention of the car removed the glory of being the world's fastest sprinter.

    • meroes•17d

      Including techbros thinking they have to answer to every question humanity has ever asked?

  • brcmthrowaway•21d

    Gamechanger! And worrisome for us laymen.

    • ac29•21d

      In the thread, they note a human had already come up with (and published) an even better solution.

    • mrcwinn•17d

      Before AI, but while you (and I) were still unable to contribute anything meaningful or novel to discussions of mathematics, did you feel threatened?