Two retirees: Dietmar Wolz at the machines and Ingo at the coffee cup!

Diary on the "First Proof" Competition

10 February, 2026
11 February, 2026
12 February, 2026
13 February, 2026

14 February, 2026
18 February, 2026
19 February, 2026

Ingo Althofer and Dr. Dietmar Wolz

We tried on the ten questions of the "First Proof" experiment.

"First Proof" announcement

Here are results of our quick attempts, using several AIs in pingpong interplay.
As expected, most of the answers were not fully satisfying.
But we learned a lot through these days.

February 12, 16:50 (CET zone): Short description of "Agentic Strategy": Agentic Strategy
February 12, 23:55 (CET zone): Agentic Strategy Design for Math Proofs: Long Paper by Dietmar Wolz

Aftermath (or Afterproof)

February 14, 20:00 (CET zone): Lessons learned from the event
February 14, 20:00 (CET zone): ChatGPT compares
February 14, 20:00 (CET zone): Gemini compares + some comments from us

On Question 6: Proof-Milking Forever

First milk: FP-Constant 1/42 improved to 1/(41+eps) by ChatGPT 5.2 4 pages, Feb 18

Second milk: OpenAI-Constant 1/256 milked to 1/20 by ChatGPT 5.2 Thinking 2 pages, Feb 19, 04:30 (CET) - confirmed bei ChatGPT 5.3 on Feb 19, 12:00 (CET)
Third milk: OpenAI-Constant 1/256 milked to 3/40 by ChatGPT 5.2 Thinking 4 pages, Feb 19, 06:20 (CET)
Feb 19, 07:00 (CET): ChatGPT analysed all graphs with 3 to 5 vertices, case by case. The finding: Here constant c = 1/2 is valid.
Check of all graphs with 6 and 7 vertices is underway.
Fourth milk: OpenAI-Constant 1/256 milked to 151/2000 by ChatGPT 5.2 Thinking 3 pages, Feb 19, 09:00 (CET)

Fifth milk: "Cursor Team" constant 0.14644 milked to 0.14706 with the help of ChatGPT 5.2, seconded by Gemini 3.
More explicitly: Their constant c= (2 - sqrt(2))/4 improved to c= (18 - 12*sqrt(2))/7; Feb 19, 21:15 (CET).

c = 1/2 was (and is) our conjecture for the general case, first formulated on February 07.
However, our AIs never came near to a proof.
So far, we did NOT find any graph which fails for c = 1/2,
although testing many examples with 16 vertices.

***********************************************************

Output after several rounds (Feb 09 - 12):
On Question 1 3 pages, Feb 09

On Question 2 7 pages, Feb 10
checked by Aristotle on Feb 12

On Question 3 5 pages, Feb 10
On Question 4 4 pages, Feb 10
On Question 5 3 pages, Feb 10

On Question 6 3 pages, Feb 10;
On Question 6 6 pages, Feb 11; - only partial proof

On Question 7 2 pages, Feb 09
On Question 7 2 pages, Feb 12
checked by Aristotle

On Question 8 3 pages, Feb 10
On Question 9 3 pages, Feb 10
On Question 10 3 pages, Feb 10

tex files on request
experimental Python code related to questions 4, 6 and 8 on request.
chat protocols on request