Diary of #autoformalization
The methodology and approaches are not too far from how my brain works or what would be the output if I would record every of my thoughts on such a problem.
But it also becomes clear that claude code is a beginner who does lots of trial-and-error and copy-paste coding.
All this is about maths that we would not write about in a research paper. It is stuff that humans just know and don't talk about.
Example:
In the paper we wrote: "Let < be the lex term order derived from the variable ordering x_1 > ... > x_n."
Takes hours and hours of labor (for claude, maybe not human experts!) and pages of code to show that this order exists and satisfies basic properties.
The human brain is amazing at focussing on the relevant and ignoring everything else.
Ja, das hatte ich auch so verstanden. Allerdings ist bei claude code und ähnlichen tools ja immer ein großer Teil der Konversation gleich wieder der Input für die nächste Runde. Das LLM läuft quasi in einer gigantischen while(true) Schleife auf seinem eigenen Output. Insofern steuert sich das damit schon selbst in eine gewisse Richtung.
Thomas Kahle
geeeero