Lean

aid: lean
name: Lean
description: >-
  Lean is an open-source theorem prover and programming language based on
  dependent type theory, designed for formal verification of mathematics and
  software. It supports interactive proof development and is used by
  mathematicians and computer scientists.
type: Index
image: https://kinlane-productions.s3.amazonaws.com/apis-json/apis-json-logo.jpg
tags:
  - Dependent Types
  - Formal Verification
  - Programming Language
  - Theorem Prover
url: https://raw.githubusercontent.com/api-evangelist/lean/refs/heads/main/apis.yml
created: '2025-01-01'
modified: '2026-04-28'
specificationVersion: '0.19'
apis:
  - aid: lean:lean
    name: Lean
    description: >-
      Lean theorem prover and programming language for formal verification
      of mathematics and software.
    humanURL: https://lean-lang.org/
    tags:
      - Formal Verification
      - Theorem Prover
    properties:
      - type: Documentation
        url: https://lean-lang.org/documentation/
common:
  - type: Website
    url: https://lean-lang.org/
  - type: Documentation
    url: https://lean-lang.org/documentation/
  - type: GitHub Organization
    url: https://github.com/leanprover/lean4
maintainers:
  - FN: Kin Lane
    email: [email protected]