Lean (bewijsassistent)
Lean is een bewijsassistent en programmeertaal. Het typesysteem is gebaseerd op de calculus of constructions met inductieve typen. Het is een open sourceproject dat wordt gehost op GitHub. Het werd voornamelijk ontwikkeld door Leonardo de Moura terwijl hij in dienst was bij Microsoft Research en nu Amazon Web Services, en heeft in de loop van zijn geschiedenis aanzienlijke bijdragen gehad van andere coauteurs en medewerkers. De ontwikkeling wordt momenteel ondersteund door de non-profit Lean Focused Research Organization (FRO).
Geschiedenis[bewerken | brontekst bewerken]
Lean werd voor het eerst gelanceerd door Leonardo de Moura bij Microsoft Research in 2013. De eerste versies van de taal, later bekend als Lean 1 en 2, waren experimenteel. Deze bevatten functies zoals ondersteuning voor op homotopietypetheorie gebaseerde grondslagen van de wiskunde. Deze werden later geschrapt.
Lean 3 werd voor het eerst uitgebracht op 20 januari 2017. Dit was de eerste redelijk stabiele versie van Lean. Het werd voornamelijk geïmplementeerd in C++, waarbij enkele functies in Lean zelf waren geschreven. Na versie 3.4.2 werd Lean 3 officieel beëindigd terwijl de ontwikkeling van Lean 4 begon. In deze tussenperiode hebben leden van de Lean-gemeenschap onofficiële versies tot en met 3.51.1 ontwikkeld en uitgebracht.
In 2021 werd Lean 4 uitgebracht, een herimplementatie van de Lean-stellingbewijzer die in staat is C-code te produceren, die vervolgens wordt gecompileerd, waardoor de ontwikkeling van efficiënte domeinspecifieke automatisering mogelijk wordt gemaakt. Lean 4 bevat ook een macrosysteem en verbeterde typeclass-synthese en geheugenbeheerprocedures ten opzichte van de vorige versie. Een ander voordeel ten opzichte van Lean 3 is de mogelijkheid om te voorkomen dat men C++-code hoeft aan te raken om de frontend en andere belangrijke onderdelen van het kernsysteem aan te passen, aangezien deze nu allemaal in Lean zijn geïmplementeerd en beschikbaar zijn voor de eindgebruiker om indien nodig te worden overschreven.
Lean 4 is niet achterwaarts compatibel met Lean 3.
In 2023 werd de Lean FRO opgericht, met als doel de schaalbaarheid en bruikbaarheid van de taal te verbeteren en bewijsautomatisering te implementeren.
Overzicht[bewerken | brontekst bewerken]
Bibliotheken[bewerken | brontekst bewerken]
Het officiële lean-pakket bevat een standaardbibliotheek std4, die gemeenschappelijke datastructuren implementeert die kunnen worden gebruikt voor zowel wiskundig onderzoek als meer conventionele softwareontwikkeling.
In 2017 begon een door de gemeenschap onderhouden project om een Lean-bibliotheek mathlib te ontwikkelen, met als doel zoveel mogelijk zuivere wiskunde te digitaliseren in één grote, samenhangende bibliotheek, met onder andere wiskunde op onderzoeksniveau.
Integratie van editors[bewerken | brontekst bewerken]
Lean integreert met:
Het heeft native ondersteuning voor Unicode-symbolen, die kunnen worden getypt met behulp van LaTeX-achtige reeksen, zoals "\times" voor "×". Lean kan ook worden gecompileerd naar JavaScript en is toegankelijk via een webbrowser, en biedt uitgebreide ondersteuning voor metaprogrammeren.
Voorbeelden (Lean 4)[bewerken | brontekst bewerken]
De natuurlijke getallen kunnen worden gedefinieerd als een inductief type. Deze definitie is gebaseerd op de axioma's van Peano en stelt dat elk natuurlijk getal nul is of de opvolger van een ander natuurlijk getal.
def Nat.add : Nat → Nat → Nat
| n, Nat.zero => n -- n + 0 = n
| n, Nat.succ m => Nat.succ (Nat.add n m) -- n + succ(m) = succ(n + m)
Gebruik[bewerken | brontekst bewerken]
Wiskunde[bewerken | brontekst bewerken]
Lean heeft de aandacht getrokken van wiskundigen Thomas Hales en Kevin Buzzard. Hales gebruikt het voor zijn project Formal Abstracts. Buzzard gebruikt het voor het Xena-project. Een van de doelstellingen van het Xena-project is om elke stelling en elk bewijs in het wiskundecurriculum van het Imperial College London in Lean te herschrijven.
In 2021 gebruikte een team van onderzoekers Lean om de juistheid van een bewijs van Peter Scholze op het gebied van de gecondenseerde wiskunde te verifiëren. Het project kreeg veel aandacht vanwege het formaliseren van een gloednieuw resultaat op wiskundig onderzoeksniveau. In 2023 gebruikte Terence Tao Lean om een bewijs van het polynomiale Freiman-Ruzsa-vermoeden te formaliseren, een resultaat dat in hetzelfde jaar door Tao en medewerkers werd gepubliceerd.
Kunstmatige intelligentie[bewerken | brontekst bewerken]
In 2022 creëerde OpenAI een op een neuraal netwerk gebaseerde stellingbewijzer voor lean, die een taalmodel gebruikte om bewijzen te genereren voor verschillende olympiadeproblemen op middelbare schoolniveau.
Later dat jaar creëerde Meta AI een AI-model dat 10 problemen van de Internationale Wiskunde Olympiade heeft opgelost.