Two open-source contributors say they have proved OpenAI's "integer multiplication below n log n" result in the Lean theorem prover in six days, while a separate community race keeps shrinking the result's constant. That is the claim, as it is spreading on X. What we could confirm is narrower: the claims exist in public posts, a public Lean repository exists whose README says the proof is complete, we did not build it, and OpenAI's own repository describes the preprint and its Lean status in careful language. This post lays out what is claimed, what is verified, and how to check it yourself.
If you need the background first, our earlier posts cover what is in OpenAI's math repository and eight of its headline results with their Lean status. In that second post, integer multiplication was the one headline result without a Lean entry in the repository's own catalogue. The new claim is aimed at exactly that gap.
Quick reference: claimed vs verified
| Question | Answer |
|---|---|
| Who says the result was proved in Lean? | A contributor posting as platypii, thanking jdb1729, as quoted by an aggregator. Project coordinator Doug Colkitt says the work required building new Lean libraries |
| Is there a public Lean repo? | Yes: platypii/integer-mult-bounds-lean. Its README says the end-to-end Mathlib proof is complete, with an unconditional saving kappa = 2^-35. We read it but did not compile anything |
| Does OpenAI's repo list a Lean entry for this family? | Not in the catalogue as we read it earlier this month. The repo says it will add Lean formalizations as it obtains them |
| Is the constant really improving? | An Oct. 8 post on X by Doug Colkitt reports a tightening from 2 to the minus 182 to 2 to the minus 15, and the Lean repo README states 2 to the minus 35 for its own statement. Different trackers report different values |
| Does it matter for real software? | No. Even the original saving is a factor of about log n to the power 2 to the minus 182 |
| Is every refinement an unconditional theorem? | Per descriptions of the tracker, no: most refinements depend on lemmas from OpenAI's preprints |
What OpenAI actually published
The starting point is the openai/math repository. Its README says the repo "contains mathematical manuscripts and supporting proof artifacts produced by an internal OpenAI model", currently 719 manuscripts in 372 families, with "about 42% top-line results formalized" in Lean. It also warns that "not all have accompanying Lean formalizations" and that "some of the unformalized results could have issues."
The README says most results used an unreleased internal model and, on average, three hours of ChatGPT Pro thinking compute per result, across roughly 4,000 problems posed. Integer multiplication below n log n is one of the families in that collection. Our rumor check on the 400-papers claim shows how quickly the numbers around this release moved in its first days, so treat any count as a snapshot.
For context, the best proven bound before this was Harvey and van der Hoeven's O(n log n) algorithm, published in the Annals of Mathematics in 2021 and itself formalized as a problem on Lean's evaluation site. OpenAI's preprint claims to go below that by a vanishingly small factor.
What the Lean claim says
A puzzle piece locking into a green seal, showing what a Lean proof of integer multiplication would certify
The aggregator page we could open summarizes the claim this way: contributors platypii (identified as Kenny) and jdb1729 formally proved OpenAI's sub-n log n integer multiplication result in Lean in six days. It also quotes Doug Colkitt, who coordinates the community effort, saying comparable formalization work previously took person-years because Lean lacked library coverage for the multitape Turing machine model that the proof needs, so Kenny had to build new libraries across a broad area of mathematics and computer science.
Those are claims by participants, relayed second hand. A few things are worth separating:
- Existence of the post. The quoted line from platypii reads, in the aggregator's rendering, that "6 days later and with huge help from @jdb1729 it looks like we proved in Lean" the result. Note the hedge in "it looks like".
- Scope of the theorem. Our eight-results post found a real example of the Lean statement being weaker than the manuscript: for the Fourier transform family, the Lean doc covers a subsequential statement, not the all-length bound. A Lean proof is only as strong as the theorem it states, so the first thing to read is the final statement.
- The model of computation. Multiplication bounds are stated for a computational model, here multitape Turing machines. If the formalization defines the machine model loosely, the headline can be proved without meaning what a complexity theorist means by it.
- Independence. Proving it in Lean checks the logic, not the choice of statement. Someone other than the authors needs to read the definitions.
The repository itself is public: platypii/integer-mult-bounds-lean. Its README says IntegerMultBounds.MathlibTM2.statement is unconditional: one fixed Turing.FinTM2 machine multiplies every pair of natural numbers, with standard binary encodings, in worst-case time O(n (log n)^(1-kappa)) with kappa = 2^-35. It states that the end-to-end Mathlib proof is complete, that no theorem uses a custom axiom or an admitted proof, and that an axiom audit runs in CI. It also says the stronger target saving of 83/10^12 is still open, and the GitHub description still calls the project a work in progress. These are the repository's own statements. Until independent Lean users build it and read the final statement, the honest label is "claimed by the authors, not yet independently checked." We did not run lake build on anything.
The race on the constant
A figure with a lantern guiding many small shapes, picturing open-source contributors racing to tighten the multiplication constant
Alongside the formalization, there is a public race. A project called Auto Research, described on an aggregator page, tracks pull requests from contributors using Claude, Codex and other agents that tighten the result's conditional exponent saving, written as kappa. It ranks contributors by merged pull requests, commits and time in the lead, and describes its outputs as AI-assisted research drafts. The same page says most refinements are conditional on lemmas from OpenAI's preprints and that maintainer review does not establish a complete unconditional theorem.
OpenAI's original value, in the community's framing, was kappa equal to 2 to the minus 182. On Oct. 8, Doug Colkitt posted that he had validated and merged a pull request from Rohan Arun, tightening it to 2 to the minus 15, which he called a roughly 500,000-fold improvement over the previous community result. Boris Power, listed on the post as Head of Applied Research at OpenAI, quoted it with: "Wow, the rate of progress on this result has been remarkable to observe!" That is an OpenAI researcher publicly welcoming the community work, which is notable on its own.
The Oct. 8 thread also lists the techniques credited for the gains: compact control bits, batching recursive calls, shared circuits and frame reuse, and new geometric approaches. A separate post in the same thread from Ryan Shea announces a research draft on a different family, the exact discrete Fourier transform below n log n, with a claimed delta of 7.3 times 10 to the minus 5.
Here the numbers differ by source. The Oct. 8 post reports 2 to the minus 15, the Lean repository's README reports 2 to the minus 35 for its unconditional statement, and an aggregator summary cited a larger figure that we could not trace to a primary page. Separate community repositories also report their own kappa values, some explicitly conditional on lemmas from the preprints. The figures may differ in what they measure, or the leaderboard may simply have moved. Treat every kappa you see on social media as a snapshot of a live leaderboard, not a result.
Why it matters, and why it does not
It does not change software. A factor of log n to a tiny power is invisible at any input you can store. Our eight-results post made the same point: the saving is indistinguishable from 1 in practice. Nobody should expect faster big-integer libraries from this.
It does change how math may be done. Three things are new at once: a lab-produced manuscript, a community that iterates on it in public within days, and a formal proof effort that claims to catch up with the paper in under a week. If the Lean claim holds, six days against a previous benchmark of person-years is a striking data point about AI-assisted formalization, with the caveat that the contributors reportedly used heavy tooling and had a manuscript to follow. Compare the verification-first approach in our coverage of Lean-based RL environments built from OpenAI's math results.
It sharpens the verification debate. Mathematicians have asked for responsible handling of AI-generated results, see the AGMAI guidance on releasing AI-generated mathematics and the Association for Human Mathematics statement. A race that optimizes a constant, fast, with agents writing most of the pull requests, is exactly the situation that worry is about: speed of claims outrunning speed of review. A fair question to hold alongside the excitement is whether such a race extracts new insight or just lowers a number.
For another example of a headline algorithm result where the details matter, see our explainer on the Tsinghua shortest-path sorting barrier result.
How to check it yourself
- Read OpenAI's own status first. In the repository, open CONTENTS.md and history.md and find the integer multiplication family. See whether a Lean entry has been added since this post.
- Clone the Lean repository. Start with platypii/integer-mult-bounds-lean. It pins Lean and Mathlib to v4.34.1 and states its theorem in the README.
- Read the final theorem statement and the machine model definition. Compare it with the manuscript's claim: same bound, same model, all input lengths, no extra hypotheses.
- Build it. Run
lake buildand look forsorry, new axioms, ornative_decideshortcuts. The openai/math README points to Comparator instructions for its own checking setup. - Check the kappa history. Use the tracker's commit log, not a screenshot, and note whether each record is marked conditional or verified.
What to watch next
- Whether OpenAI adds the contributors' Lean proof to its catalogue or points to a community-hosted repository. Its README says it is exploring community-hosted repositories for these materials.
- Whether independent Lean users build the proof and report the same theorem statement.
- Whether the tracker publishes a verified-versus-unverified split for kappa.
- Whether the Fourier transform draft gets the same treatment.
FAQ
Has OpenAI's integer multiplication result been proved in Lean? Contributors say so and a public repository's README claims a complete proof, but we did not build it, and OpenAI's catalogue had not listed it as of our reading.
What does below n log n mean? Fewer than a constant times n log n bit operations to multiply two n-digit integers, improving on the 2021 O(n log n) algorithm by a tiny factor.
Is the constant improvement real? The posts exist and an OpenAI researcher publicly praised the progress, but the figures differ between sources.
Does it change real software? No.
How do I check? Follow the five steps above.
Related reading
- OpenAI's 722 math manuscripts: what to check
- OpenAI's math repo: eight headline results and their Lean status
- The 400-math-papers rumor, checked
- Lean RL environments from OpenAI's math results
- Guidance on releasing AI-generated mathematics
- Association for Human Mathematics statement on OpenAI
- Simons Foundation's $15M AI math initiative
Details are accurate as of October 15, 2026. The Lean claim, the repository and the tracker numbers may change quickly.