Een driehoek vol priemgetallen:
Categorie archieven: Weetjes
Wiskunde en Chatgpt 5.2
De voorbije dagen wees Terence Tao erop dat er op de Erdős Problems-website een mijlpaal is bereikt: een open probleem van Erdős (nummer #728) kreeg een oplossing waarbij AI-tools een opvallend grote rol speelden — en de kernstelling werd bovendien formeel geverifieerd in Lean.
Lean is een bewijsassistent : software waarmee je wiskundige definities, stellingen en bewijzen zó precies opschrijft dat de computer stap voor stap kan controleren of alles logisch klopt.
Wat doet Lean concreet?
-
Het definieert objecten: groepen, ringen, verzamelingen, limieten, enz.
-
Het formuleert een stelling in formele taal.
-
Het schrijft een bewijs als een reeks kleine logische stappen (tactieken of termen).
-
Lean accepteert het bewijs alleen als elke stap geldig is volgens de logica én volgens de eerder gedefinieerde begrippen.
Als Lean “QED” bereikt, betekent dat: het bewijs is formeel correct binnen het systeem.
De status op de probleem-pagina is ondertussen:
PROVED (LEAN) – opgelost en het bewijs is in Lean geverifieerd.
Concreet vermeldt de pagina dat Kevin Barreto en ChatGPT-5.2 bewezen hebben dat er (zelfs vrij “symmetrische”) oplossingen bestaan.
En wat is nu juist de rol geweest van Chatgpt?
-
Een informeel argument werd gegenereerd met een taalmodel (GPT-5.2/ChatGPT-5.2).
-
Dat argument werd vervolgens geformaliseerd in Lean met hulp van een automatische formaliserings-/theorem-proving tool (“Aristotle” wordt expliciet genoemd), waarna anderen konden nakijken of de formele statement klopt.
-
Daarna volgden er menselijke controles: klopt de formulering, hoe zit het met trivialiteiten, en is er eerdere literatuur (bv. Pomerance) die verwant is?
Dat laatste is cruciaal: een Lean-check geeft heel veel zekerheid dat de formele proof correct is voor de exacte formele stelling — maar je wil nog steeds menselijke zorg voor (i) interpretatie van het “bedoelde” probleem en (ii) correcte situering in bestaande literatuur.
In de thread maakt Tao een heel didactisch punt: wiskunde gaat niet enkel om een proof-object, maar om begrip. Een AI kan een technisch correcte redenering produceren, maar het “rondmaken” — motivering, context, why-this-works, verbanden met eerdere resultaten — blijft essentieel. AI speelde een hoofdrol in het produceren van een bruikbaar argument en in (semi-)automatische formaliseringsstappen, maar het geheel gebeurde in een community-proces met menselijke controle, discussie over interpretatie, en aandacht voor literatuur.
De driehoek van Kepler
De Kepler-driehoek is een bijzondere rechthoekige driehoek die werd bestudeerd door de astronoom en wiskundige Johannes Kepler (1571–1630). Wat deze driehoek uniek maakt, is dat de lengtes van zijn zijden een meetkundige rij vormen en dat het iets te maken heeft met de gulden snede. Kepler schreef ooit:
“Geometria duas magnas res habet: theoremata Pythagorae et sectionem auream.”
(De meetkunde bezit twee grote schatten: de stelling van Pythagoras en de gulden snede.)
Voor Kepler waren deze twee diep verbonden, en de Kepler-driehoek was voor hem een symbolische en wiskundige schakel tussen beide. We weten dat de gulden snede gegeven wordt door 
en dat 
. Zodoende krijgen we volgende situatie:
Hadamard matrix
Een Hadamard matrix is een vierkante matrix met alleen maar 1 of -1 als elementen en zodat elk tweetal kolommen ( of rijen) loodrecht op elkaar staan ( de som van de producten op de zelfde rij is nul). Een Hadamard matrix is dus een vierkante orthogonale matrix met elementen 1 en -1. Hij is vernoemd naar de Franse wiskundige J. Hadamard(1865-1963).
Er kan niet voor elke willekeurige orde een Hadamard matrix bestaan. Een noodzakelijke voorwaarde is dat de orde gelijk moet zijn aan 1, 2 of een veelvoud van 4. De grote open vraag in de wiskunde, bekend als het Hadamard-vermoeden, is: Bestaat er een Hadamard-matrix voor elke orde die een veelvoud van 4 is? Tot nu toe is er nog geen tegenvoorbeeld gevonden, maar een algemeen bewijs ontbreekt nog steeds. De kleinste orde waarvoor het bestaan van een Hadamard-matrix nog niet is bewezen of weerlegd, is .
In de telecommunicatie en informatietheorie worden Hadamard-matrices gebruikt om foutcorrectiecodes te construeren, zoals de Reed-Muller-codes. De orthogonaliteit van de rijen maakt het mogelijk om verzonden signalen ondanks ruis betrouwbaar te decoderen, omdat de verschillende ‘woorden’ (rijen van de matrix) zo ver mogelijk van elkaar verwijderd zijn. Dit is cruciaal voor bijvoorbeeld de CDMA-techniek (Code Division Multiple Access) in mobiele netwerken.
Jurassic fractaal of drakenkromme
De Drakenfractaal werd onafhankelijk ontdekt door de natuurkundigen John Heighway en Bruce Banks, en later grondiger geanalyseerd door de wiskundigen Chandler Davis en Donald Knuth in 1967.
De roman Jurassic Park (1990) bevat illustratiesvan de iteraties van de Drakenfractaal tussen de hoofdstukken. Deze afbeeldingen dienen als visuele representatie van de theorieën die in het verhaal worden besproken.
De Jurassic fractaal wordt vaak gedefinieerd met een iteratieve regelsysteem (L-systeem, of Lindenmayer-systeem). Zo’n systeem bestaat uit:
-
een axioma (de startregel): F = teken een lijn
-
en productieregels die bepalen hoe elke stap verandert: F+F-F-F+F, met + draai rechts en – draai links.
Door dit proces herhaald toe te passen (itereren), groeit een steeds complexere, grillige vorm — dat is de fractaal.
