RT
@nasqret: I have personally crossed a line, and I am a bit in awe.
This is my first fully automated, LLM-generated and auto-formalized proof of a new mathematical theorem.
Let me set up the problem: we have three rotating circles with six positions each, all three intersecting in a total of six points.
Prove that the group of motions they generate is the full symmetric group S_{12}.
This is a problem I originally noticed in a lovely puzzle in the game Machinarium by Amanita Design.
The task is not extremely hard, but it apparently has two proofs:
1. A brute-force search over conjugacy classes to represent all transpositions (I did this many years ago but never published it).
2. An LLM-generated proof (in this case produced about three months ago by GPT-5-Pro), or actually two proofs, both using in a brilliant way a theorem of Jordan about primitive groups (or a closely related variant that is even more direct). (
What I was missing until tonight was a tool to auto-formalize this proof.
Thanks to
@HarmonicMath , I gained access to their remarkable software, Aristotle. In summary, here is what I did:
A. Auto-generated the proof with an LLM (and ran it multiple times to obtain a much improved version).
B. Trimmed the proof to the bare mathematical text—definitions, propositions, lemmas, theorems—with proofs supplied by the LLM.
C. Ran the Aristotle system overnight (via API). This morning I received a fully formalized version in Lean (about 700 lines of code).
The code compiles, so I now have a certificate confirming that the LLM-generated proof indeed led to a correct solution. Moreover, I got a conceptual proof, better than my own brute-force. I am planning to push it further to more broad class of such algebra problems.
It is a small project, but for me personally it marks a milestone. I now have tools which, with my orchestration, can genuinely help me discover, formalize, and study proofs of mathematical theorems. This is non-trivial.
Questions:
1. How will this scale in the future?
2. How much training will be necessary to be successful on such tasks?
3. How should we treat authorship of such proofs?
4. What is the deeper role of mathematicians?
