Google DeepMind’s AlphaProof Nexus solves 9 Erdős problems and proves 44 sequence conjectures

[Bob Lyons]

https://cryptobriefing.com/deepmind-alphaproof-nexus-erdos-problems/

The article mentions the OEIS.

Here's a link to the "Advancing Mathematics Research with AI-Driven Formal Proof Search" paper that the article references:

https://arxiv.org/html/2605.22763v1

Bob

[Antti Karttunen]

On Sat, May 23, 2026 at 5:46 PM Bob Lyons <bobly...@gmail.com> wrote:

https://cryptobriefing.com/deepmind-alphaproof-nexus-erdos-problems/

The article mentions the OEIS.

It says that it proved 44/492 OEIS conjectures, but then later mentions only those involving

https://oeis.org/A051293 and https://oeis.org/A228143

What were the others?

Best,

Antti

 

Here's a link to the "Advancing Mathematics Research with AI-Driven Formal Proof Search" paper that the article references:

https://arxiv.org/html/2605.22763v1

Bob

--
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/CAJ%3DEaLRfOTpF%2BX4xdxcL1LbdA2Ni8bD2qQFnZM%2BxBQU8aq%2Bwow%40mail.gmail.com.

[D. S. McNeil]

You can see the Lean outputs here, I think:

https://github.com/google-deepmind/alphaproof-nexus-results/tree/main/APNOutputs/OEIS

Doug

To view this discussion visit https://groups.google.com/d/msgid/seqfan/CAB%2B0_%3Dm8uxtYs94ZWz1hdtbyJixFdhYwipJV9mnWN_%3DC%3DT_Oiw%40mail.gmail.com.

[brad klee]

The paper is here: https://arxiv.org/pdf/2605.22763v1 . I don't know if the two mentioned 

are a pair of cherries or what, as neither of the sequences appeal to me. 

The conjecture for A108 is almost a poorly stated tautology, or more fairly a special 

case of a theorem that applies to all strong enough exponential growth. 

Harm.On.ica claims to have improved the proof working from a suggestion of mine: 

https://github.com/bradleyklee/Artifacts/tree/main/05-lean-conjectures

Unfortunately I think you're making each other look bad on that one, but hey, at 

least I also look bad using these methods and not checking that much. 

If I had more time we would go after A2897 as well. The theorem itself doesn't look 

very surprising, but the labor would be more involved. 

All the best, 

--Brad