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-images.s3.amazonaws.com/shared/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: GitHubOrganization
  url: https://github.com/leanprover/lean4
maintainers:
- FN: Kin Lane
  email: kin@apievangelist.com