Lean (Beweisassistent)

Lean ist ein mathematischer Beweisassistent und eine Programmiersprache. Lean beruht auf Calculus of constructions (nach Thierry Coquand) mit induktiven Typen. Lean ist ein Open-Source-Projekt.

  1. ↑ Lean and its Mathematical Library. In: Lean. 2024, abgerufen am 1. März 2024 (englisch).
Dieser Artikel wurde von Wikipedia herausgegeben. Der Text ist unter Creative Commons Attribution-Share Alike 4.0 verfügbar, sofern nicht anders angegeben. Für die Mediendateien können zusätzliche Bedingungen gelten.