Picture inspired by Donald Knuth's euphoric report
on an AI-aided proof of certain triples of Hamiltonian cycles
Diary: Math with AI
Ingo Althofer
Time is running like a wild horse, in particular
concerning Math with AI.
08 March, 2026 - Formalizing Proofs
Dietmar Wolz and I had not been so successful in the
FirstProof experiment. But we learned a lot in
"milking proofs" with help of AI:
Our FirtProof Diary
Now the new Archon team from Beijing formalized not only
the 1/256-proof of OpenAI, but also our milking results
for the better constants 1/20 and 3/40. In particular,
their formalizer exploited the fact that our proofs
were "merely" results from milking the OpenAI solution.
Archon team readme
I am looking forward to see user-friendly variants of Lean and co
in the near future!
07 March, 2026 - ChatGPT 5.4 on the road
Math student Quanyu Tang from Xi'an is one of the early adopters.
He directly solved an Erdos problem with the help of 5.4:
#650 on Thomas Blooms website.
No problem, that it turned out later in the night that
Uncle Paul himself had had a solution already.
06 March, 2026 - ChatGPT 5.4
Yesterday in the evening I learned that ChatGPT 5.4 was released.
I took a chance immediately and tested it on the old alpha-proof question from August 2025.
Seeing that it was going to get stuck immediately I gave a one-line hint:
>>Treat sqrt(alpha) not as a decimal but as an algebraic number<<
Direct hit! 5.4 produced a nice proof, much better than the proofs given by other LLMs before. After some pingpong with Gemini 3.1 Pro the result was a nice preprint. I will keep it confidential - to use this test also in the future.
05 March, 2026 - learned about Donald Knuth's enthusiastic AI-report
***********************************************************
Contact: substitute PingPongPadam
ingo.althoeferPingPongPadamuni-jena.de
Back to the main site
Initiated on 06 March 2026