Ik heb persoonlijk een grens overschreden, en ik ben een beetje onder de indruk. Dit is mijn eerste volledig geautomatiseerde, LLM-gegeneerde en auto-geformaliseerde bewijs van een nieuwe wiskundige stelling. Laat me het probleem opzetten: we hebben drie roterende cirkels met elk zes posities, die allemaal in totaal zes punten elkaar snijden. Bewijs dat de groep van bewegingen die ze genereren de volledige symmetrische groep S_{12} is. Dit is een probleem dat ik oorspronkelijk opmerkte in een prachtige puzzel in het spel Machinarium van Amanita Design. De taak is niet extreem moeilijk, maar het heeft blijkbaar twee bewijzen: 1. Een brute-force zoekopdracht over conjugatieklassen om alle transposities te vertegenwoordigen (dit deed ik vele jaren geleden maar heb het nooit gepubliceerd). 2. Een LLM-gegeneerd bewijs (in dit geval ongeveer drie maanden geleden geproduceerd door GPT-5-Pro), of eigenlijk twee bewijzen, beide op een briljante manier gebruikmakend van een stelling van Jordan over primitieve groepen (of een nauw verwante variant die nog directer is). ( Wat ik tot vanavond miste, was een hulpmiddel om dit bewijs automatisch te formaliseren. Dankzij @HarmonicMath kreeg ik toegang tot hun opmerkelijke software, Aristotle. Samengevat, hier is wat ik deed: A. Auto-gegeneerd het bewijs met een LLM (en het meerdere keren uitgevoerd om een veel verbeterde versie te verkrijgen). B. Het bewijs teruggebracht tot de essentiële wiskundige tekst—definities, proposities, lemma's, stellingen—met bewijzen geleverd door de LLM. C. Het Aristotle-systeem 's nachts laten draaien (via API). Vanmorgen ontving ik een volledig geformaliseerde versie in Lean (ongeveer 700 regels code). De code compileert, dus ik heb nu een certificaat dat bevestigt dat het LLM-gegeneerde bewijs inderdaad leidde tot een correcte oplossing. Bovendien kreeg ik een conceptueel bewijs, beter dan mijn eigen brute-force. Ik ben van plan om het verder uit te breiden naar een bredere klasse van dergelijke algebraïsche problemen. Het is een klein project, maar voor mij persoonlijk markeert het een mijlpaal. Ik heb nu hulpmiddelen die, met mijn orkestratie, me echt kunnen helpen om bewijzen van wiskundige stellingen te ontdekken, te formaliseren en te bestuderen. Dit is niet triviaal. Vragen: 1. Hoe zal dit in de toekomst opschalen? 2. Hoeveel training zal nodig zijn om succesvol te zijn in dergelijke taken?...