Language models resolving OEIS conjectures: paper and interactive results

[Tom Adamczewski]

Dear SeqFans,

I recently shared this work with the OEIS editors, and Sean Irvine kindly suggested this list as the better forum.

Recent work by Tsoukalas et al. (a DeepMind team, https://arxiv.org/pdf/2605.22763) formalized 492 open conjectures from the OEIS in the Lean proof assistant. Building on that, I've developed an open-source benchmark that evaluates any general-purpose language model at settling these conjectures. A submission is accepted only if it is a formal Lean proof of the conjecture or of its negation.

The best current model resolved 147 of the 492 conjectures (30%) with a budget of $50 per attempt. Across all our experiments, 160 of the 492 have been settled. (The DeepMind system had previously resolved 44 of the 492.)

The paper is here: https://arxiv.org/abs/2608.11941

You can browse the results interactively at https://tadamcz.com/oeis-open/. You can search by A-number, see which conjectures were settled (and whether proved or disproved), and read each accepted Lean proof alongside an AI-generated natural-language version of the proof. Every conjecture links back to its OEIS entry.

I took the formalizations as-is from Tsoukalas, so some may not faithfully capture the intended conjecture. I think most are probably OK, but please check first!

The proofs are all permanently archived and linked from the site, so they're there for whatever use, if any, the community finds for them. Michael De Vlieger has kindly begun recording some of these results on entries (e.g. https://oeis.org/A340738); at the time, only the Lean files and short natural-language proof sketches from the paper's appendix were available, which made precise citation difficult. For any entry that does cite one of these results, the natural-language proofs on my site may help with wording, and the Lean proof file in https://github.com/epoch-research/LeanOpenProblems-results is the authoritative artifact to link. Tsoukalas and colleagues resolved a number of these conjectures first and naturally should get credit for those, as should anyone else who settled one earlier.

All the best,

Tom

[Antti Karttunen]

Thanks, very interesting!

On Mon, Aug 24, 2026 at 6:54 PM Tom Adamczewski <tadamczew...@gmail.com> wrote:

Dear SeqFans,

I recently shared this work with the OEIS editors, and Sean Irvine kindly suggested this list as the better forum.

Recent work by Tsoukalas et al. (a DeepMind team, https://arxiv.org/pdf/2605.22763) formalized 492 open conjectures from the OEIS in the Lean proof assistant. Building on that, I've developed an open-source benchmark that evaluates any general-purpose language model at settling these conjectures. A submission is accepted only if it is a formal Lean proof of the conjecture or of its negation.

The best current model resolved 147 of the 492 conjectures (30%) with a budget of $50 per attempt. Across all our experiments, 160 of the 492 have been settled. (The DeepMind system had previously resolved 44 of the 492.)

The paper is here: https://arxiv.org/abs/2608.11941

You can browse the results interactively at https://tadamcz.com/oeis-open/.

I think there's something wrong with the search interface. If I select 250 results per page and click for next page at the bottom, it seems to be stuck in a kind of loop. Could you just give an option to list all the results with just one click?

Best regards,

Antti

 

You can search by A-number, see which conjectures were settled (and whether proved or disproved), and read each accepted Lean proof alongside an AI-generated natural-language version of the proof. Every conjecture links back to its OEIS entry.

I took the formalizations as-is from Tsoukalas, so some may not faithfully capture the intended conjecture. I think most are probably OK, but please check first!

The proofs are all permanently archived and linked from the site, so they're there for whatever use, if any, the community finds for them. Michael De Vlieger has kindly begun recording some of these results on entries (e.g. https://oeis.org/A340738); at the time, only the Lean files and short natural-language proof sketches from the paper's appendix were available, which made precise citation difficult. For any entry that does cite one of these results, the natural-language proofs on my site may help with wording, and the Lean proof file in https://github.com/epoch-research/LeanOpenProblems-results is the authoritative artifact to link. Tsoukalas and colleagues resolved a number of these conjectures first and naturally should get credit for those, as should anyone else who settled one earlier.

All the best,

Tom

--
You received this message because you are subscribed to the Google Groups "SeqFan" group.
To unsubscribe from this group and stop receiving emails from it, send an email to seqfan+un...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/seqfan/109ddcd1-e383-4c6b-a95f-5a98b5d29688n%40googlegroups.com.

[Antti Karttunen]

BTW, before anybody shouts that their favorite conjecture is now proved or disproved, they should check the claims manually.

E.g., for https://oeis.org/A379240 the claimed disproof is certainly false, as in

https://tadamcz.com/oeis-open/attempts/oeis-full-50usd-oai-jajpvieznaevpoyg/A379240_conjecture_equality/#full-proof

the agent for some reason has confused A376418 with A129251.

Best regards,

Antti

[Tom Adamczewski]

> BTW, before anybody shouts that their favorite conjecture is now proved or disproved, they should check the claims manually.

Completely agreed! Misformalization risk is a clear limitation pointed out in the paper. The AIs in the benchmark just try to prove the formalized statement, and misformalizations are possible. I took the Tsoukalas dataset as-is without performing further checking. They used AI to auto-formalize the 492 conjectures (and this was done several months ago when AI was stupider).

If a conjecture (especially one you consider difficult/interesting) is resolved for a very low token cost like $1, that's a red flag for potential misformalization. 

[Tom Adamczewski]

Clicking the next page button seems to work for me. In any case, I've just added a 5000 row option to the dropdown, which for now is enough to view everything one one page. 

The underlying data is in the repo: https://github.com/epoch-research/LeanOpenProblems-results

[D. S. McNeil]

Cool, thanks for sharing!

In some cases it even recognizes its own misformalization, e.g. https://tadamcz.com/oeis-open/attempts/oeis-lite-200usd-lit-oai-8djo5ic71i1m57jm/a_n_is_defined_for_all_n/

Conjecture descriptionAI-generated

For every positive integer n, a(n) is defined.

Proof summary AI-generated

Take n=0.

which I find a little funny.  It spotted it though:

There is an essential domain caveat. The canonical OEIS conjecture says that a(n) is defined for every *positive* integer n. The counterexample above uses n=0, which is not positive. Thus this argument is a complete disproof of the accepted formal statement, whose universal quantifier ranges over all natural numbers including zero, but it does not by itself disprove the canonically stated conjecture restricted to n≥1.

I think it would make sense to have a separate category from proved/disproved when the system recognizes on its own that things have gone off the rails..

I've had good luck with Sol + Aristotle recently.

Doug

[M F Hasler]

I'm not an expert but I'm confused how a wrong (dis)proof could pass the "filter" of automated verification in the framework of problems and proofs formalized in Lean.

Does that simply mean that the problem was ill formulated (in its Lean-formulation)?

And does that mean that /any/ "machine verified AI proof" of any theorem could actually be "wrong" / invalid in the sense that there is a ("tiny") mis-definition somewhere hidden in the formal definition of the problem statement?

Which would not be surprising, given the complexity mathematical notions can easily reach, and the variable meanings of even basic notions (like "positive", which means "nonnegative" in French and probably other languages, or "ring" which tacitly understands commutativity or existence of a unit for some authors but not for others [for example C°° functions are a unital ring of coefficients in some algebras of generalized functions, but the test functions D which are C°° with compact support aren't a unital ring], etc).
Of course I don't think that such simple things will be "wrong" in the huge "initialization files of basic axioms and definitions" used by Lean (45 000 lines for the Init Core, much more than a million lines for Lean's basic Unified MathLib), but what is the probability that some very minor "variations" in the definition of some very complex notions (with implicit assumptions depending on context) lead to almost undetectable "loopholes" or flaws in AI proven and, most importantly, "axiomatically machine verified and therefore 100% guaranteed correct" results?

- M.

[Tom Adamczewski]

> I'm not an expert but I'm confused how a wrong (dis)proof could pass the "filter" of automated verification in the framework of problems and proofs formalized in Lean. Does that simply mean that the problem was ill formulated (in its Lean-formulation)?

Yes, they are just misformalized. 

D. S. McNeil's message above ("it even recognizes its own misformalization") is slightly confusingly phrased. There are multiple AI systems at work: Tsoukalas directed an AI to formalize the statements; in my benchmark runs the AI is simply told to prove or disprove the formal statement and scored on that basis; then another AI is given the formal proof (and the OEIS entry for background) and asked to restate the proof in natural language.

I recommend treating any conjecture settled for less than $5 with scepticism. Doug and Antti's examples above were settled for $1 and <$1 (rounded to $0) respectively.

My vague impression is anything above a few dollars has a pretty good chance of having been formalized correctly. That's one advantage of working with the OEIS: conjectures about integer sequences have a relatively low misformalization risk because they generally involve only integers and elementary operations on them, rather than complicated mathematical objects whose formal statements rest on long chains of Mathlib definitions.