Project "First Proof" in Mathematics with AI proofs

Dear friends,

being retired, I have started to make more mathematics
than in the years before. On August 07, 2025, the publication
of ChatGPT 5 was a game changer, concerning LLMs in
math research.

In the last 7 days very crazy stuff took place.
I explain the background: In chess chess-programs had become
serious helpers for analysis in the early 1990's. (My friend
GM Dr. Karsten Müller was second of GM Alexei Shirov, and used
Fritz 2 and Fritz 3 in analysis of adjourned games from 1992 on).
In the meantime, chess programs (in particular Stockfish) are
understanding (and playing) chess in another league than any human.

Starting in August 2025, ChatGPT, Gemini 3 and a few other LLMs
have become real helpers when proving theorems in mathematics.
(Karsten Müller however has remained old school - still proving
theorems in the old way, but asking me from time to time to
check his papers critically with the help of ChatGPT and Gemini.)

When in Dewcember 25 and January 26 first larger successes in
autonomous solving of Erdos problems by AIs happened, in certain
circles in Mathematics it became frequent opinion that LLMs could
prove only things that were near to what was already in the
literature. Thus: "nothing new and nothing really creative"
many mathematicians claimed.

Now a group of 11 math profs (most of them from the US) joined
forces and started a project named "First Proof": On Feb 06
they published ten math problems where they had solutions, but
which were not known to the public (and not availabe online).
One of the eleven is Martin Hairer, a fields medaillist.

On Feb 14, 9:00 a.m. UK time zone (midnight California time)
the groups wants to publish hints for their solutions.
Here are links to their project and to the ten problems:

https://1stproof.org/
https://arxiv.org/abs/2602.05192

Starting on Feb 07, my friend Dr. Dietmar Wolz (born in 1963, retired
like me) and I have been engaged in this "contest". The special thing:
People should not use own (human) math skills, but only steer the LLMs
in use so that the "bots" found (total or partial) solutions. Dietmar
and I did this mainly by using ChatGPT and Gemini in "intelligent"
pingpong mode.

A coarse documentation of our engagement (+ some cartoons) is
online, including a detailed description by Dietmar of our
agentic setting.

https://althofer.de/first-proof-competition/first-proof-report.html

I expect that our agentic team has solved X of the ten problems
correctly, with unknown variable X from {2, 3, 4}.

I am so fanatic in this experiment because it reminds me of the 1980's
and 1990'S when I had developed the 3-Hirn approach in chess:
using 2 different chess computers, coordinated by a human.

In case of questions I will happily explain more.

Kind regards, Ingo.

The proofs of the authors of FirstProof can be downloaded from here: the pdf file

https://codeberg.org/tgkolda/1stproof/src/branch/main/2026-02-batch/

It has 68 pages and is 10 MB large.
First impression: Hard bread to understand the solutions,
for Dietmar and me, but also for the AI bots.

Cheers, Ingo.

Great project !

I use ChatGpt5.2 a lot to work to understand Collatz Conjecture better, rational cycles and why powers of 3 can't approximate powers of 2. Maybe we will manage to solve one of your easier problems...

Aren't you afraid that if the proofs are somewhere online, the AI could browse the net and use them to derive their own simpler proofs ?

@carroll.

Yes, "First Proof" is a great project, and it just came at the right moment.

It seems Dietmar and I got 2 (q9 and q10) + 0.5 (q5) + 0.5 (q6) of the problems solved.
We are now writing a report "Lessons learned".

---

On the 3n+1 problem.
I think the variants for x >= 5 (in Xn+1) and 9n+1 should be doable.

The new Prize 0 with
n -> 3n+1 and 3n-1, both with prob 1/2, and trapped at 1 earler or later,
is difficult, but should be easier than original Collatz. Perhaps, this
will be a qeustion where AIs may help a lot in the next few years.

By the way: AIs help me to evaluate "solution attempts" by amateurs within
minutes.

Regards, Ingo.