What A Time To Be Alive

Woordenlijst

Lean

Lean is een programmeertaal en hulpprogramma voor wiskundige bewijzen. Elke definitie en elke stap staat zo precies opgeschreven dat de computer kan nagaan of het bewijs klopt.

Lean is een programmeertaal waarin je wiskunde opschrijft, zo precies dat een computer elke stap kan nakijken. Zo'n programma heet een proof assistant, een bewijsassistent. Je schrijft een stelling en een bewijs op, en Lean controleert of het bewijs de stelling echt aantoont, zonder te gokken en zonder iets over te slaan.

Het is te vergelijken met een leraar die een uitwerking regel voor regel nakijkt en het hele bewijs afkeurt zodra één stap niet klopt.

Hoe werkt het?

In Lean staan definities, stellingen en bewijzen als code. De kern van Lean is klein en wordt algemeen vertrouwd. Alles wat erbovenop komt, hoeft niet apart vertrouwd te worden: Lean controleert het. Een bewijs dat door Lean wordt goedgekeurd, is dus correct voor wat er is opgeschreven. Het blijft wel belangrijk dat de definities in Lean precies hetzelfde zeggen als de wiskunde die men bedoelt.

Het opschrijven kost veel tijd, want je moet elke stap uitspelen. Daar kan AI bij helpen. De AI bedenkt en schrijft uit, en Lean kijkt het na. Dat controleren met wiskundige zekerheid heet formele verificatie.

Waarom het ertoe doet

Lean is in het nieuws omdat AI wiskunde levert op een schaal die geen mens kan nalopen. Het bedrijf Axiom Math liet tientallen AI-agents in 24 dagen het ongeveer 15.000 pagina's lange bewijs van de classificatie van eindige enkelvoudige groepen omzetten in Lean-code (link). Onderweg vonden ze afwijkingen in het gepubliceerde werk, die zijn gerepareerd.

Ook bij nieuwe resultaten is zo'n computercontrole waardevol. OpenAI zegt dat zijn interne AI-modellen drie lang openstaande vraagstukken in wiskunde, informatica en natuurkunde hebben opgelost, en een deel van de bewijzen is al door een controleprogramma nagelopen (link). Kort daarna meldde Anthropic dat een intern Claude-model zelf een snellere manier vond om een beroemde rekenpuzzel op te lossen, met een bewijs dat een computer al controleerde (link). Zo hoeven wiskundigen niet alles zelf na te rekenen om te weten dat het klopt.

Artikelen over Lean