Recently (May 13, 2024), OpenAI released the new version of GPT called GPT-4o; I tested it on math problems and I must say I was impressed. I asked for:

  1. a proof that in an isosceles triangle the angles at the base are equal (good, although the use of triangle congruence criteria can be discussed)
  2. the solution to the brachistochrone problem using the Euler-Lagrange equation (the approach seemed correct, but I didn't verify all calculations)
  3. a proof of Bernoulli's inequality (perfect)
  4. a proof of the Schroeder-Bernstein theorem (incomplete)
  5. multiplication of two numbers with 5 digits using the elementary school method (wrong!)

I also tested its knowledge of proof assistants by asking it to prove the Schroeder-Bernstein theorem in various systems including Isabelle, Hol Light, Lean, Mizar, Metamath, ACL2. It knew all the ones I asked about. Particularly, it seemed to have good knowledge of Mizar and Lean, but that's just my impression.

Overall, GPT's mathematical capabilities have significantly improved. I wonder about two things:

  1. does his knowledge of the various proof assistants correlate with his current mathematical ability?
  2. how is it possible that it is still unable to multiply two 5-digit numbers, since the symbolic manipulation required should be no greater than writing numerous lines of code (I suppose)?
  • 2
    $\begingroup$ Are you asking us (the folks on a proof assistants site) to explain how neural networks work? $\endgroup$ Commented May 17 at 22:47
  • $\begingroup$ @AndrejBauer yes! I wanted to know if you know if the libraries of the proof assistants were used to improve the mathematical skills of the LLMs (GPT in particular) and possibly how much of the improvement that occurred is attributable to that; however, it is a known fact that OpenAI is not transparent about where the training data comes from, so I wouldn't be surprised if no one knows anything; anyway, I don't think that neural networks and proof assistants are two worlds so distant, since there is IMO Grand Challenge $\endgroup$
    – M. Lonardi
    Commented May 18 at 0:47
  • $\begingroup$ There are some people where who might know these things. $\endgroup$ Commented May 18 at 8:37
  • $\begingroup$ @AndrejBauer your observation made me realize that I could ask GPT-4o directly (I copied the question and it actually gave me an interesting answer); you have helped me in your own way, thank you $\endgroup$
    – M. Lonardi
    Commented May 18 at 19:32

2 Answers 2


We don't actually know how GPT-4o works under the hood, but lets assume for now it is more or less a standard transformer model like GPT-2 or GPT-3 was. Then we have a pretty good idea of what is going on with multiplication in transformers. There are too many 5-digit pairs for a transformer to just memorize, so it has to generalize to all pairs, and only certain types of information is a transformer good at generalizing over. A lot of this relates to how a transformer decodes information. For example, one observation is that a transformer requires O(n^2) steps to do a task where n is the size of the input plus output. Now this doesn't directly tell us about multiplication since that has an O(n^2) algorithm (I think) but it gives you an idea about the complexity here. Moreover, transformers compute information in a very particular way which further constrains the types of algorithms they can learn in a length-invariant way. A good paper on this is What Algorithms can Transformers Learn? A Study in Length Generalization? I think multiplication with the more common multiplication algorithms wouldn't fit these criteria.

Now as for your first question, are you asking if the ability of these models to do general math reasoning and write ITP code go hand-in-hand? That is a difficult question to answer for a lot of reasons. There certainly is reason to believe that all the information used to train a LLM is also useful for a lot of related (and unrelated tasks). There are papers for example suggesting that the ability to learn programming (in say Python) also helps with natural language reasoning abilities, and it would also probably help with ITP as well if for no other reason than the model would better manipulate code.

Now, as for benchmarking models there are a number of standard benchmarks used for math reasoning and for code generation, there aren't as many standard benchmarks for ITP use, so we don't have as much measurement on how ITP use has improved with the models. While the Llemma paper for example does have a lot of decent experiments for LLMs on ITPs, those are not included in the standard LLM benchmark suite and I assume no one has run them on GPT-4o. Also, the GPT trainers probably have tried to avoid contaminating GPT-4o's training data with standard benchmarks, they likely haven't taken that care with the benchmarks used for ITPs, so there is a large probably GPT-4o has already seen say all Lean theorems, and likely many solutions to benchmarks like MiniF2F. (I'm also not convinced that, even with OpenAI's efforts, the standard benchmarks are also not tainted. There are just too many ways to accidentally ingest the test problems.)

Also, the creators of these models are not just sucking in data, but trying to get the models to be better at certain types of problems including many of the types of problems you've mentioned (like coding, math reasoning, and (maybe) ITP use). So they probably specifically put effort into making the model better at these things.

Finally, you say "symbolic manipulation [for multiplication] required should be no greater than writing numerous lines of code". This is hard to confirm. Coding, like natural language, can be accomplished with a lot of intuition. When I code, I don't go through some algorithm. I think very high level and only when I need to do I get into complicated details. For multiplication, I don't have strong intuition except for certain common times of numbers. Otherwise, I'm just following an algorithm with no shortcuts. It might be that there are a lot more shortcuts to common reasoning and coding problems than we realize.

  • $\begingroup$ Thank you so much, your observation on the computational complexity of transformers has been illuminating for me. Sherlock Holmes tells Watson "Every problem becomes very childish when once it is explained to you". Moreover, I was wondering why they didn't use a system very close to natural language like Mizar for the IMO Grand Challenge and now I realize that tactics are inevitable, so the most suitable systems turn out to be those that combine human readability and tactics (Isabelle/Isar, Lean, Coq). I will study "What Algorithms can Transformers Learn?" carefully. Thanks again. $\endgroup$
    – M. Lonardi
    Commented May 20 at 16:36

In my experience trying to use GPT3 for math, even though language models might be able to regurgitate well known proofs or outline proofs at a high level, when you try to probe further and ask the LLM to specify details of a proof you will find it is completely unable to.

As far as I know the only successful use of LLMs for theorem proving is AlphaGeometry, but even then the LLM is only used to generate lemmas in a highly constrained setting, not to actually prove them.

Considering GPT4o's main innovation is in its input and output abilities (human computer interaction) it is highly unlikely that its reasoning abilities are any different from GPT3's.

  • $\begingroup$ It's true that the main innovation of GPT-4o is on the front of human-machine interaction, but it has also improved a lot in terms of reasoning. You need to try it, trust me. In the meantime, OpenAI declined my card and I can no longer buy tokens. Sigh, just when I had decided to spend some money... $\endgroup$
    – M. Lonardi
    Commented May 22 at 10:19
  • $\begingroup$ When you say GPT-3 do you mean the 2020 model? I think a lot of improvement has happened since then with Codex, GPT-3.5, ChatGPT, GPT-4, and GPT-4o. And even if by GPT-3, you mean the current free version of ChatGPT, I have still heard from others that ChatGPT-4 (and ChatGPT-4o) is much better at a lot of things including various math tasks. I’m not saying these models “understand”, but they do have their uses. $\endgroup$
    – Jason Rute
    Commented May 22 at 10:58
  • $\begingroup$ AlphaGeometry isn’t the only successful use of LMs in theorem proving. For LMs trained from scratch, there is AlphaGeometry, FOL theorem provers (arxiv.org/pdf/2112.10664), and ITP theorem provers (arxiv.org/pdf/2009.03393). For pre-trained LLMs (at least GPT-3 size) there is autoformalization, the best results on the MiniF2F benchmark, and (probably) the best results on the AIMO first progress prize (kaggle.com/competitions/ai-mathematical-olympiad-prize/…) (score out of 50). I think we still have a long way to go but this isn’t nothing. $\endgroup$
    – Jason Rute
    Commented May 22 at 11:14
  • $\begingroup$ The one I tried was GPT 3.5, to be precise. Performant FOL theorem provers have existed for decades, and AIME problem sets are not particularly difficult mathematics. The point is that none of these systems are plain LLMs. This question was about a pure LLM's ability to understand mathematics. $\endgroup$
    – Couchy
    Commented May 23 at 4:32

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.