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.
09 March, 2026
On formalizing proofs: There is a nice 30-minutes report on
Youtube by Terence Tao, how he used Claude Code to formalize
a proof in Lean interactively. He is a virtuose.
When formalizing a proof in Lean with help of Aristotle, I learned
one lesson: if Aristotle's output is only "partial formalization"
you can ask ChatGPT to look through that output and to identify
missing pieces. The answer is typically much more userfriendly
than Aristotle's protocoll.
Quanyu Tang has a good second service. He came back to
#650 and completely closed the gap between lower and upper bound.
The final answer has constant 2*root(n). Before, the lower
bound had been only 1*root(n).
To repeat a wish from yesterday: I hope for more user-friendly
tools to formalize proofs in Lean! (In the late 1990's I was actively
involved in a similar process to make chess programs better tools
for analysis of positions.)
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 FirstProof 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