Mathematicians will soon be out of a job

[John Clark]

An AI from Google solved nine out of 353 open Erdős problems it attempted, including two questions that had gone unanswered for 56 years. The system also proved 44 out of 492 open conjectures from the Online Encyclopedia of Integer Sequences (OEIS), settled a 15-year-old question about Hilbert functions in algebraic geometry, and improved a known bound in convex optimization. Inference costs ran just a few hundred dollars per problem:

Advancing Mathematics Research with AI-Driven Formal Proof Search

===

The following is a quote from: 

Fields Medal proof formalized for the first time

"The proofs were verified by the mathematical community and deemed correct, leading to the Fields Medal recognition. But formal verification, the ability of a proof to be verified by a computer, is another beast altogether. Formal verification of a proof is like a rubber stamp. It’s a kind of bona fide certification that you know your statements of reasoning are correct."

John K Clark    See what's on my list at  Extropolis

3xp

[Tomasz Rola]

On Wed, Jun 03, 2026 at 05:53:19AM -0400, John Clark wrote:
> *An AI from Google solved nine out of 353 open Erdős problems it attempted,

> including two questions that had gone unanswered for 56 years. The system
> also proved 44 out of 492 open conjectures from the Online Encyclopedia of
> Integer Sequences (OEIS), settled a 15-year-old question about Hilbert
> functions in algebraic geometry, and improved a known bound in convex

> optimization. Inference costs ran just a few hundred dollars per problem:*
>
> *Advancing Mathematics Research with AI-Driven Formal Proof Search*
> <https://arxiv.org/pdf/2605.22763v1>

Cool. So how many problems had this AI formulated, so far?
Mathematician is able to formulate a problem, put up a hypothesis, it
is not just a guy with mechanical proficiency of calculating
formulae. So far you seem to mistake a mathematician and some kind of
logical-algebraic robot writing on empty paper sheets with unhuman
speed.

This is why I proposed that you set up an AI in such a way that it
knows all that was to know in New Year's Day 1930 (or 1936, I would
have to check) and writes me about Turing machine, and then maybe
invents Turing test. It does not have to call it Turing machine, of
course. I want a definition of it, out of nothing, made by this
machine of yours. A mathematician did it, once.

--
Regards,
Tomasz Rola

--
** A C programmer asked whether computer had Buddha's nature. **
** As the answer, master did "rm -rif" on the programmer's home **
** directory. And then the C programmer became enlightened... **
** **
** Tomasz Rola mailto:tomas...@bigfoot.com **

[John Clark]

On Wed, Jun 3, 2026 at 8:15 AM 'Tomasz Rola' via Everything List <everyth...@googlegroups.com> wrote:

> *An AI from Google solved nine out of 353 open Erdős problems it attempted,
> including two questions that had gone unanswered for 56 years. The system
> also proved 44 out of 492 open conjectures from the Online Encyclopedia of
> Integer Sequences (OEIS), settled a 15-year-old question about Hilbert
> functions in algebraic geometry, and improved a known bound in convex
> optimization. Inference costs ran just a few hundred dollars per problem:*

Cool.

Indeed!  

> So how many problems had this AI formulated, so far?

I don't know what you mean by "formulated", you should've used the word "prove".  The answer to that question is in the very quote from my post that you made in the above; 9  Erdős problems that have gone unsold for decades, and 44 open problems from the Online Encyclopedia of Integer Sequences, and improved a known bound in convex optimization. And today, on June 3, 2026, AI is the stupidest it will ever be. AI keeps getting smarter. Unfortunately human beings do not. 

John K Clark    See what's on my list at  Extropolis

ljk

 

--

[Brent Meeker]

Formulated is what Erdos did for 353 problems.

Brent

--
You received this message because you are subscribed to the Google Groups "Everything List" group.
To unsubscribe from this group and stop receiving emails from it, send an email to everything-li...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/everything-list/CAJPayv1ZX%2B-wg06yYCJe4g6ewcYfnxeW67baeu-v_NDveqEG9w%40mail.gmail.com.

[John Clark]

On Wed, Jun 3, 2026 at 3:53 PM Brent Meeker <meeke...@gmail.com> wrote:

> Formulated is what Erdos did for 353 problems.

In other words Erdos asked 353 questions and an AI answered 9 of them, answers that no Human was able to come up with even though they were decades old.  

John K Clark

> *An AI from Google solved nine out of 353 open Erdős problems it attempted,
> including two questions that had gone unanswered for 56 years. The system
> also proved 44 out of 492 open conjectures from the Online Encyclopedia of
> Integer Sequences (OEIS), settled a 15-year-old question about Hilbert
> functions in algebraic geometry, and improved a known bound in convex
> optimization. Inference costs ran just a few hundred dollars per problem:*

Cool.

Indeed!  

> So how many problems had this AI formulated, so far?

I don't know what you mean by "formulated", you should've used the word "prove".  The answer to that question is in the very quote from my post that you made in the above; 9  Erdős problems that have gone unsold for decades, and 44 open problems from the Online Encyclopedia of Integer Sequences, and improved a known bound in convex optimization. And today, on June 3, 2026, AI is the stupidest it will ever be. AI keeps getting smarter. Unfortunately human beings do not. 

John K Clark    See what's on my list at  Extropolis

ljk

 

--

--
You received this message because you are subscribed to the Google Groups "Everything List" group.
To unsubscribe from this group and stop receiving emails from it, send an email to everything-li...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/everything-list/CAJPayv1ZX%2B-wg06yYCJe4g6ewcYfnxeW67baeu-v_NDveqEG9w%40mail.gmail.com.

--
You received this message because you are subscribed to the Google Groups "Everything List" group.
To unsubscribe from this group and stop receiving emails from it, send an email to everything-li...@googlegroups.com.

To view this discussion visit https://groups.google.com/d/msgid/everything-list/3d2556a5-1462-45a8-be7c-74ffc1198502%40gmail.com.

[Quentin Anciaux]

Don't play dumb. They are asking about formulating new problems... and solve them.

All those moments will be lost in time, like tears in rain. (Roy Batty/Rutger Hauer)

To view this discussion visit https://groups.google.com/d/msgid/everything-list/CAJPayv3wb%2BKxHFPbQwhW3cZLCGR2DBG2SBw3aJUUAYpqFRr58A%40mail.gmail.com.

[Brent Meeker]

Don't act dense.  You wrote, "I don't know what you mean by "formulated", you should've used the word "prove".  So I told you what I meant by "formulated" by pointing to 353 examples.

Brent

To view this discussion visit https://groups.google.com/d/msgid/everything-list/CAJPayv3wb%2BKxHFPbQwhW3cZLCGR2DBG2SBw3aJUUAYpqFRr58A%40mail.gmail.com.

[Stathis Papaioannou]

Stathis Papaioannou

On Wed, 3 Jun 2026 at 22:15, 'Tomasz Rola' via Everything List <everyth...@googlegroups.com> wrote:

On Wed, Jun 03, 2026 at 05:53:19AM -0400, John Clark wrote:
> *An AI from Google solved nine out of 353 open Erdős problems it attempted,
> including two questions that had gone unanswered for 56 years. The system
> also proved 44 out of 492 open conjectures from the Online Encyclopedia of
> Integer Sequences (OEIS), settled a 15-year-old question about Hilbert
> functions in algebraic geometry, and improved a known bound in convex
> optimization. Inference costs ran just a few hundred dollars per problem:*
>
> *Advancing Mathematics Research with AI-Driven Formal Proof Search*
> <https://arxiv.org/pdf/2605.22763v1>

Cool. So how many problems had this AI formulated, so far?
Mathematician is able to formulate a problem, put up a hypothesis, it
is not just a guy with mechanical proficiency of calculating
formulae. So far you seem to mistake a mathematician and some kind of
logical-algebraic robot writing on empty paper sheets with unhuman
speed.

This is why I proposed that you set up an AI in such a way that it
knows all that was to know in New Year's Day 1930 (or 1936, I would
have to check) and writes me about Turing machine, and then maybe
invents Turing test. It does not have to call it Turing machine, of
course. I want a definition of it, out of nothing, made by this
machine of yours. A mathematician did it, once.

It might be possible to do that, but then someone will find some other task that only some humans can do and AI has not yet done. The final thing, when they can beat humans at everything, will be that they are not conscious, because they will never be able to prove that.

[Brent Meeker]

Eventually I think that people will realize that "conscious" means a lot of different things from being aware of internal v. external states to being able to tell yourself stories in your head.  The last has nothing to do with proving math theorems (as noted by Poincare').  It's a useless skill in being able to simulate (imagine) yourself in different situations.  But even as I type this I notice that my finger motions are not controlled at that level of consciousness; it's called "touch typing".

Brent

[Tomasz Rola]

On Thu, Jun 04, 2026 at 08:24:02AM +1000, Stathis Papaioannou wrote:
> Stathis Papaioannou
>
> On Wed, 3 Jun 2026 at 22:15, 'Tomasz Rola' via Everything List <
> everyth...@googlegroups.com> wrote:
>

[...]

> > This is why I proposed that you set up an AI in such a way that it
> > knows all that was to know in New Year's Day 1930 (or 1936, I would
> > have to check) and writes me about Turing machine, and then maybe
> > invents Turing test. It does not have to call it Turing machine, of
> > course. I want a definition of it, out of nothing, made by this
> > machine of yours. A mathematician did it, once.
>
>
> It might be possible to do that, but then someone will find some other task
> that only some humans can do and AI has not yet done. The final thing, when
> they can beat humans at everything, will be that they are not conscious,
> because they will never be able to prove that.

Sure. However, if I am to take thing-B as a replacement for thing-A,
then I am free to want whatever function from thing-A to be replicated
in thing-B. Or else this is not going to be replacement. Someone else
may claim that my requirements are not very important, because for
them certain aspects of thing-A was never important. But for me, those
functions are the clue of being thing-A.

Allowing for anything less is like voluntarily allowing to be
scammed. They take from you a sports car and they give you a
sketeboard. Hey, it is rolling like a sports car. We have made great
progress. Our shares are roaring even higher than a day before.

[John Clark]

On Wed, Jun 3, 2026 at 4:36 PM Quentin Anciaux <allc...@gmail.com> wrote:

> Don't play dumb. They are asking about formulating new problems... and solve them.

Erdos didn't solve any of those nine problems nor did any other human being, an AI did using only a few hundred dollars worth of computer time. Are you seriously proposing that although AI is capable of correctly answering questions it will never be able to ask questions?! 

  John K Clark    See what's on my list at  Extropolis

evv

[Quentin Anciaux]

All those moments will be lost in time, like tears in rain. (Roy Batty/Rutger Hauer)

Le jeu. 4 juin 2026, 11:50, John Clark <johnk...@gmail.com> a écrit :

On Wed, Jun 3, 2026 at 4:36 PM Quentin Anciaux <allc...@gmail.com> wrote:

> Don't play dumb. They are asking about formulating new problems... and solve them.

Erdos didn't solve any of those nine problems nor did any other human being, an AI did using only a few hundred dollars worth of computer time. Are you seriously proposing that although AI is capable of correctly answering questions it will never be able to ask questions?! 

I do not, I'm pointing you're dodging their argument. 

Quentin 

  John K Clark    See what's on my list at  Extropolis

evv

 

All those moments will be lost in time, like tears in rain. (Roy Batty/Rutger Hauer)

Le mer. 3 juin 2026, 22:22, John Clark <johnk...@gmail.com> a écrit :

On Wed, Jun 3, 2026 at 3:53 PM Brent Meeker <meeke...@gmail.com> wrote:

> Formulated is what Erdos did for 353 problems.

In other words Erdos asked 353 questions and an AI answered 9 of them, answers that no Human was able to come up with even though they were decades old.  

John K Clark

> *An AI from Google solved nine out of 353 open Erdős problems it attempted,
> including two questions that had gone unanswered for 56 years. The system
> also proved 44 out of 492 open conjectures from the Online Encyclopedia of
> Integer Sequences (OEIS), settled a 15-year-old question about Hilbert
> functions in algebraic geometry, and improved a known bound in convex
> optimization. Inference costs ran just a few hundred dollars per problem:*

Cool.

Indeed!  

> So how many problems had this AI formulated, so far?

I don't know what you mean by "formulated", you should've used the word "prove".  The answer to that question is in the very quote from my post that you made in the above; 9  Erdős problems that have gone unsold for decades, and 44 open problems from the Online Encyclopedia of Integer Sequences, and improved a known bound in convex optimization. And today, on June 3, 2026, AI is the stupidest it will ever be. AI keeps getting smarter. Unfortunately human beings do not. 

John K Clark    See what's on my list at  Extropolis

ljk

 

--
You received this message because you are subscribed to the Google Groups "Everything List" group.
To unsubscribe from this group and stop receiving emails from it, send an email to everything-li...@googlegroups.com.

To view this discussion visit https://groups.google.com/d/msgid/everything-list/CAJPayv1ZouS%2BoJF8SW3Reot%2BMn%3Dn5kHCDW7KgsEriMnEPh2Nsg%40mail.gmail.com.

[John Clark]

On Thu, Jun 4, 2026 at 6:01 AM Quentin Anciaux <allc...@gmail.com> wrote:

>>> Don't play dumb. They are asking about formulating new problems... and solve them.

>> Erdos didn't solve any of those nine problems nor did any other human being, an AI did using only a few hundred dollars worth of computer time. Are you seriously proposing that although AI is capable of correctly answering questions it will never be able to ask questions?! 

> I do not, I'm pointing you're dodging their argument. 

It's very easy to dodge because I don't know what their argument is, or yours. 

  John K Clark    See what's on my list at  Extropolis

wcw

evv

To view this discussion visit https://groups.google.com/d/msgid/everything-list/CAMW2kApEhY7c5p-f2BQceLOX1P8PAh1%2Br43ZXDcvsEzcy4oepw%40mail.gmail.com.

[Quentin Anciaux]

All those moments will be lost in time, like tears in rain. (Roy Batty/Rutger Hauer)

Le jeu. 4 juin 2026, 12:43, John Clark <johnk...@gmail.com> a écrit :

On Thu, Jun 4, 2026 at 6:01 AM Quentin Anciaux <allc...@gmail.com> wrote:

>>> Don't play dumb. They are asking about formulating new problems... and solve them.

>> Erdos didn't solve any of those nine problems nor did any other human being, an AI did using only a few hundred dollars worth of computer time. Are you seriously proposing that although AI is capable of correctly answering questions it will never be able to ask questions?! 

> I do not, I'm pointing you're dodging their argument. 

It's very easy to dodge because I don't know what their argument is, or yours. 

The argument is that albeit it's true it proved, solved unsolved problems, it currently didn't formulate new unknown problems. I'm sure it will, but currently it didn't. 

Quentin 

To view this discussion visit https://groups.google.com/d/msgid/everything-list/CAJPayv1rDvMPdyzumtRpC%2BRwM%2Bkx_HfaMS7rj2zHC%2BG5AQJCAw%40mail.gmail.com.

[John Clark]

On Thu, Jun 4, 2026 at 6:52 AM Quentin Anciaux <allc...@gmail.com> wrote:

 > it currently didn't formulate new unknown problems

I still don't understand your point. As I understand the word, Andrew Wiles didn't "formulate" any new unknown problems, but he was able for the first time to answer a question that Fermat asked nearly 400 years ago. And I'm willing to bet that very few mathematicians have even asked an AI to find new unsolved problems because we already have more than enough old unsolved problems.  

John K Clark

mvt

>> Erdos didn't solve any of those nine problems nor did any other human being, an AI did using only a few hundred dollars worth of computer time. Are you seriously proposing that although AI is capable of correctly answering questions it will never be able to ask questions?! 

> I do not, I'm pointing you're dodging their argument. 

It's very easy to dodge because I don't know what their argument is, or yours. 

The argument is that albeit it's true it proved, solved unsolved problems, it currently didn't formulate new unknown problems. I'm sure it will, but currently it didn't. 

[Quentin Anciaux]

All those moments will be lost in time, like tears in rain. (Roy Batty/Rutger Hauer)

Le jeu. 4 juin 2026, 13:24, John Clark <johnk...@gmail.com> a écrit :

On Thu, Jun 4, 2026 at 6:52 AM Quentin Anciaux <allc...@gmail.com> wrote:

 > it currently didn't formulate new unknown problems

I still don't understand your point. As I understand the word, Andrew Wiles didn't "formulate" any new unknown problems, but he was able for the first time to answer a question that Fermat asked nearly 400 years ago.

Fermat did ask, no AI currently asked... also it's not my point, I'm sure AI will find new unknown problems, but currently the result is solving known problems  which is great. 

--
You received this message because you are subscribed to the Google Groups "Everything List" group.
To unsubscribe from this group and stop receiving emails from it, send an email to everything-li...@googlegroups.com.

To view this discussion visit https://groups.google.com/d/msgid/everything-list/CAJPayv14%3DymJWt7J-Tq9bY-X92Vh3HU1KbBqUvE09GcFhD8RWg%40mail.gmail.com.

[Brent Meeker]

On 6/4/2026 2:49 AM, John Clark wrote:

On Wed, Jun 3, 2026 at 4:36 PM Quentin Anciaux <allc...@gmail.com> wrote:

> Don't play dumb. They are asking about formulating new problems... and solve them.

Erdos didn't solve any of those nine problems nor did any other human being, an AI did using only a few hundred dollars worth of computer time. Are you seriously proposing that although AI is capable of correctly answering questions it will never be able to ask questions?! 

I'm pointing out that it hasn't been proved capable of that yet.  Even among mathematicians, Erdos stood out for his ability to ask interesting questions.

"I don't know what you mean by "formulated", you should've used the word "prove".   At least you figured out what "formulated" means.

Brent

  John K Clark    See what's on my list at  Extropolis

evv

 

All those moments will be lost in time, like tears in rain. (Roy Batty/Rutger Hauer)

Le mer. 3 juin 2026, 22:22, John Clark <johnk...@gmail.com> a écrit :

On Wed, Jun 3, 2026 at 3:53 PM Brent Meeker <meeke...@gmail.com> wrote:

> Formulated is what Erdos did for 353 problems.

In other words Erdos asked 353 questions and an AI answered 9 of them, answers that no Human was able to come up with even though they were decades old.  

John K Clark

> *An AI from Google solved nine out of 353 open Erdős problems it attempted,
> including two questions that had gone unanswered for 56 years. The system
> also proved 44 out of 492 open conjectures from the Online Encyclopedia of
> Integer Sequences (OEIS), settled a 15-year-old question about Hilbert
> functions in algebraic geometry, and improved a known bound in convex
> optimization. Inference costs ran just a few hundred dollars per problem:*

Cool.

Indeed!  

> So how many problems had this AI formulated, so far?

I don't know what you mean by "formulated", you should've used the word "prove".  The answer to that question is in the very quote from my post that you made in the above; 9  Erdős problems that have gone unsold for decades, and 44 open problems from the Online Encyclopedia of Integer Sequences, and improved a known bound in convex optimization. And today, on June 3, 2026, AI is the stupidest it will ever be. AI keeps getting smarter. Unfortunately human beings do not. 

John K Clark    See what's on my list at  Extropolis

ljk

 

--
You received this message because you are subscribed to the Google Groups "Everything List" group.
To unsubscribe from this group and stop receiving emails from it, send an email to everything-li...@googlegroups.com.

To view this discussion visit https://groups.google.com/d/msgid/everything-list/CAJPayv1ZouS%2BoJF8SW3Reot%2BMn%3Dn5kHCDW7KgsEriMnEPh2Nsg%40mail.gmail.com.

[John Clark]

On Thu, Jun 4, 2026 at 9:59 PM Brent Meeker <meeke...@gmail.com> wrote:

>> Erdos didn't solve any of those nine problems nor did any other human being, an AI did using only a few hundred dollars worth of computer time. Are you seriously proposing that although AI is capable of correctly answering questions it will never be able to ask questions?! 

>I'm pointing out that it hasn't been proved capable of that yet. 

Does something that obvious even need a demonstration? And as I said before "I'm willing to bet that very few mathematicians have even asked an AI to find new unsolved problems because we already have more than enough old unsolved problems".  

   >At least you figured out what "formulated" means.

Apparently as used around here it's just a pompous way of saying "think of a question". And it's usually easier to ask a question than it is to answer one just as it's easier to read a book than it is to write one; however I can't actually prove that because although I strongly suspect that P≠NP I can't actually prove it. 

  John K Clark    See what's on my list at  Extropolis

m.5

[Tomasz Rola]

On Fri, Jun 05, 2026 at 07:48:30AM -0400, John Clark wrote:
> On Thu, Jun 4, 2026 at 9:59 PM Brent Meeker <meeke...@gmail.com> wrote:
>

> *>> Erdos didn't solve any of those nine problems nor did any other human

> >> being, an AI did using only a few hundred dollars worth of computer time.
> >> Are you seriously proposing that although AI is capable of correctly

> >> answering questions it will never be able to ask questions?! *
> >
> >
> > *>I'm pointing out that it hasn't been proved capable of that yet. *
> >
>
> *Does something that obvious even need a demonstration?

Yes. Your assertion was, that AI was to replace a mathematician, still
present in the subject of this email. Mathematicians are doing
things. AI will be doing those things or it will not replace
mathemathicians.

> And as I said before "I'm willing to bet that very few
> mathematicians have even asked an AI to find new unsolved problems

> because we already have more than enough old unsolved problems". *

My question was not about people asking AI for guidance. My question
was about AI making new ideas by asking questions, something that
nobody before had thought about. And not some trivial questions ("is
the Sun green?"), and not some questions which can be made by doing
steps proposed in some books on "creative" problem solving, which are
not creative so much, because they are just combining existing
solutions and trying to squeeze something out of this ("inventing"
binoculars with right color of glass, so that Sun looks green,
indeed).

Like, in Turing case, "can machine think", or even "can machine think
like human". But there is more to it. If I am correct, Turing was
working on a problem (so called Entscheidungsproblem [1]) and invented
concept of certain automaton (nowadays called by his name) to answer
question about this problem. Similarly, Alonzo Church was also working
on this problem and invented lambda calculus [2] to help himself find
an answer. In other words, theories that form a basis of modern
computing are by-products of some other work done by mathematicians,
which is in a way funny. And Hilbert, when formulating his problem,
would have never dreamt of the consequences, I guess.

Nobody before them had idea like this, to my knowledge (ok, Leibniz,
if memory serves, did some musings). There was no hint for it in
pre-existing literature, so your AI would not be able to invent
anything similar by combinatoricaly combining relevant fragments of
books and articles from its vast memory.

The question about asking questions is important, despite your efforts
to make it look dumb (because if AI does not do it, then it must be
something dumb, right). Some questions actually moved the whole
civilisation forward. And maybe there are mathematicians who do not
ask questions, but there is mathematics which had been built by people
asking them (and finding creative, really creative ways of answering
them).

[1] https://en.wikipedia.org/wiki/Entscheidungsproblem
[2] https://en.wikipedia.org/wiki/Lambda_calculus

[Brent Meeker]

On 6/5/2026 4:48 AM, John Clark wrote:

On Thu, Jun 4, 2026 at 9:59 PM Brent Meeker <meeke...@gmail.com> wrote:

>> Erdos didn't solve any of those nine problems nor did any other human being, an AI did using only a few hundred dollars worth of computer time. Are you seriously proposing that although AI is capable of correctly answering questions it will never be able to ask questions?! 

>I'm pointing out that it hasn't been proved capable of that yet. 

Does something that obvious even need a demonstration? 

Erdos got a lot of love for thinking of his questions.  If it's so easy, let's see it done.  Have you thought of one? You can ask your own AI.

And as I said before "I'm willing to bet that very few mathematicians have even asked an AI to find new unsolved problems because we already have more than enough old unsolved problems".  

   >At least you figured out what "formulated" means.

Apparently as used around here it's just a pompous way of saying "think of a question". 

How is it used where you live?

And it's usually easier to ask a question than it is to answer one just as it's easier to read a book than it is to write one; however I can't actually prove that because although I strongly suspect that P≠NP I can't actually prove it. 

Nobody asked for a proof of which is easier.  I just asked for some examples.

Brent

[John Clark]

On Fri, Jun 5, 2026 at 3:59 PM Brent Meeker <meeke...@gmail.com> wrote:

>> although I strongly suspect that P≠NP I can't actually prove it.

> Nobody asked for a proof of which is easier.  I just asked for some examples.

If I could give you an example of an algorithm that could solve just one NP Complete problem in polynomial time then I would have proven that P=NP, but unfortunately I don't know of such an example.  

John K Clark