Lean (proof assistant)

Website: leanprover.github.io

Lean este un limbaj de teoremă și limbaj de programare.

Se bazează pe calculul construcțiilor cu tipuri inductive.

Proiectul Lean este un proiect open-source găzduit pe Github.

Acesta a fost lansat de Leonardo de Moura la Microsoft Research în 2013.Lean are o interfață, implementată ca extensie de cod Visual Studio și Server Language Server Protocol, care o diferențiază de alți provenitori de teoremă interactivă.

Are suport nativ pentru simbolurile Unicode, care pot fi tastate folosind secvențe asemănătoare latexului, cum ar fi „\ ori” pentru „×”.

Lean poate fi, de asemenea, compilat la JavaScript și accesat într-un browser web și are un suport extins pentru meta-programare.

Început în 2017, biblioteca întreținută de utilizator Mathlib conține cea mai mare colecție de matematică care a fost oficializată în Lean.

În februarie 2023, Mathlib conține peste 100.000 de teoreme și 1.000.000 de linii de cod.

În lansările anterioare de Lean, mai multe părți de bază ale logicii sistemului nu au fost modificate.

Un utilizator care dorește să schimbe aceste părți ale sistemului ar trebui să modifice implementarea C ++ a Lean.

Mai mult, aerul asociat cu interpretarea mașinii virtuale a însemnat că eficiența Lean nu a fost competitivă cu alți asistenți de probă, cum ar fi Coq.

În 2021, Leonardo de Moura și Sebastian Ullrich au lansat Lean 4: o reimplementare a proverului teoremei slabe în sine, cu scopul de a aborda cele două critici menționate mai sus.

Lean 4 produce cod C care este apoi compilat, permițând dezvoltarea automatizării eficiente specifice domeniului.

Lean 4 nu este compatibil înapoi cu Lean 3.Lean a atras atenția de la matematicienii Thomas Hales și Kevin Buzzard.

Hales îl folosește pentru proiectul său, rezumate formale.

Buzzard îl folosește pentru proiectul Xena.

Unul dintre obiectivele proiectului Xena este de a rescrie fiecare teoremă și dovadă în programa de matematică de licență a Imperial College London din Lean.