FROM INTUITION TO RESEARCH
Drie niveaus van uitleg
01 · Begrijp het probleem
Voor n groter dan twee bestaan geen positieve gehele a, b en c met aⁿ + bⁿ = cⁿ. Mensen bewezen dit al; Claude formaliseerde het.
02 · Begrijp de bijdrage
Anthropic meldt dat Claude in elf dagen een volledig Lean-bewijs met circa 29.500 tussenstellingen maakte; Kevin Buzzard gaf commentaar.
03 · Academische verdieping
Dit is formalisering, geen oplossing van een nog open probleem. De Lean-kernel toetst bewijstermen tegen expliciete definities en axioma's; correcte specificaties blijven essentieel.
Mogelijke betekenis
Maakt grootschalige controle van ingewikkelde bewijzen voorstelbaar.
Wat NIET is aangetoond
De stelling was eerder door Andrew Wiles bewezen; formele controle verklaart niet hoe het model intern dacht.