The Lean 4 theorem prover and programming language
type: Item
instance of: scholarly article
title: The Lean 4 theorem prover and programming language
DOI: 10.1007/978-3-030-79876-5_37
author: Leonardo de Moura
author: Sebastian Ullrich
publication date: 2021-12-01T00:00:00Z
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7437105
describes a project that uses: Lean
MaRDI profile type: Publication
full work available at URL: 978-3-030-79876-5 37
OpenAlex ID: W3178506813
cites work: The calculus of constructions
cites work: Maintaining a library of formal mathematics
cites work: Programming with higher-order logic.
cites work: The Lean Theorem Prover (System Description)
cites work: Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
Recommended article: The Lean Theorem Prover (System Description)
Recommended article: Automated Technology for Verification and Analysis
Recommended article: Voting theory in the Lean theorem prover
Recommended article: Logic programming as a basis for lean automated deduction
Recommended article: Q4286882
Recommended article: leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
Recommended article: LEAN: An intermediate language based on graph rewriting
Recommended article: Q3400636
Recommended article: The higher-order prover Leo-III
description: scientific article; zbMATH DE number 7437105