# Lean (Q6509476)

| Property ID | Property | Value | Value entity | Amount | Unit | Date / from | Until | Rank | Sources |
| --- | --- | --- | --- | ---: | --- | --- | --- | --- | --- |
| P366 | Has use | automated theorem proving | Q431667 |  |  |  |  | normal |  |
| P31 | Instance of | open-source software | Q1130645 |  |  |  |  | normal |  |
| P31 | Instance of | proof assistant | Q11387554 |  |  |  |  | normal |  |
| P31 | Instance of | programming language | Q9143 |  |  |  |  | normal | https://lean-lang.org/documentation/ |
| P275 | License | Apache Software License 2.0 | Q13785927 |  |  |  |  | normal |  |
| P856 | Website | https://lean-lang.org/ |  |  |  |  |  | normal | https://github.com/leanprover/lean4 |
| P737 | Influenced by | Rocq prover | Q1131652 |  |  |  |  | normal |  |
| P737 | Influenced by | Isabelle | Q460340 |  |  |  |  | normal |  |
| P178 | Developer | Microsoft Research | Q1144725 |  |  |  |  | normal |  |
| P178 | Developer | Leonardo de Moura | Q84844322 |  |  |  |  | normal |  |
| P277 | Written in | C | Q15777 |  |  |  |  | normal |  |
| P277 | Written in | C++ | Q2407 |  |  |  |  | normal |  |
| P277 | Written in | Lean | Q6509476 |  |  |  |  | normal |  |
| P571 | Founded | 2013 |  |  |  |  |  | normal |  |
| P400 | Platforms | cross-platform | Q174666 |  |  |  |  | normal |  |
| P6216 | Copyright status | copyrighted | Q50423863 |  |  |  |  | normal |  |
| P306 | Operating system | cross-platform | Q174666 |  |  |  |  | normal |  |
| P577 | Released | 2013 |  |  |  |  |  | normal |  |
| P407 | Language | English | Q1860 |  |  |  |  | normal |  |
| P348 | Latest version | 4.34.1 |  |  |  |  |  | preferred | https://github.com/leanprover/lean4/releases/tag/v4.34.1 |
| P348 | Latest version | 3.0.0 |  |  |  |  |  | normal | https://github.com/leanprover/lean/releases/tag/v3.0.0 |
| P348 | Latest version | 3.1.0 |  |  |  |  |  | normal | https://github.com/leanprover/lean/releases/tag/v3.1.0 |
| P348 | Latest version | 3.2.0 |  |  |  |  |  | normal | https://github.com/leanprover/lean/releases/tag/v3.2.0 |
| P348 | Latest version | 3.3.0 |  |  |  |  |  | normal | https://github.com/leanprover/lean/releases/tag/v3.3.0 |
| P348 | Latest version | 3.4.0 |  |  |  |  |  | normal | https://github.com/leanprover/lean/releases/tag/v3.4.0 |
| P348 | Latest version | 3.4.1 |  |  |  |  |  | normal | https://github.com/leanprover/lean/releases/tag/v3.4.1 |
| P348 | Latest version | 3.4.2 |  |  |  |  |  | normal | https://github.com/leanprover/lean/releases/tag/v3.4.2 |
| P348 | Latest version | 4.0.0 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.0.0 |
| P348 | Latest version | 4.1.0 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.1.0 |
| P348 | Latest version | 4.2.0 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.2.0 |
| P348 | Latest version | 4.3.0 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.3.0 |
| P348 | Latest version | 4.4.0 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.4.0 |
| P348 | Latest version | 4.5.0 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.5.0 |
| P348 | Latest version | 4.6.0 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.6.0 |
| P348 | Latest version | 4.6.1 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.6.1 |
| P348 | Latest version | 4.7.0 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.7.0 |
| P348 | Latest version | 4.8.0 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.8.0 |
| P348 | Latest version | 4.9.0 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.9.0 |
| P348 | Latest version | 4.9.1 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.9.1 |
| P348 | Latest version | 4.10.0 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.10.0 |
| P348 | Latest version | 4.11.0 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.11.0 |
| P348 | Latest version | 4.12.0 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.12.0 |
| P348 | Latest version | 4.13.0 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.13.0 |
| P348 | Latest version | 4.14.0 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.14.0 |
| P348 | Latest version | 4.15.0 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.15.0 |
| P348 | Latest version | 4.16.0 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.16.0 |
| P348 | Latest version | 4.17.0 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.17.0 |
| P348 | Latest version | 4.18.0 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.18.0 |
| P348 | Latest version | 4.19.0 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.19.0 |
| P348 | Latest version | 4.20.1 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.20.1 |
| P348 | Latest version | 4.20.0 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.20.0 |
| P348 | Latest version | 4.21.0 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.21.0 |
| P348 | Latest version | 4.22.0 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.22.0 |
| P348 | Latest version | 4.23.0 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.23.0 |
| P348 | Latest version | 4.24.0 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.24.0 |
| P348 | Latest version | 4.25.0 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.25.0 |
| P348 | Latest version | 4.25.1 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.25.1 |
| P348 | Latest version | 4.24.1 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.24.1 |
| P348 | Latest version | 4.25.2 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.25.2 |
| P348 | Latest version | 4.26.0 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.26.0 |
| P348 | Latest version | 4.27.0 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.27.0 |
| P348 | Latest version | 4.28.0 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.28.0 |
| P348 | Latest version | 4.29.0 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.29.0 |
| P348 | Latest version | 4.28.1 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.28.1 |
| P348 | Latest version | 4.29.1 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.29.1 |
| P348 | Latest version | 4.30.0 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.30.0 |
| P348 | Latest version | 4.31.0 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.31.0 |
| P348 | Latest version | 4.32.0 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.32.0 |
| P348 | Latest version | 4.32.1 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.32.1 |
| P348 | Latest version | 4.32.2 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.32.2 |
| P348 | Latest version | 4.33.0 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.33.0 |
| P348 | Latest version | 4.33.1 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.33.1 |
| P348 | Latest version | 4.34.0 |  |  |  |  |  | normal | https://github.com/leanprover/lean4/releases/tag/v4.34.0 |
| P3966 | Programming paradigm | functional programming | Q193076 |  |  |  |  | normal |  |
| P1072 | Readable file format | Lean 3 file format | Q130223835 |  |  |  |  | normal |  |
| P1072 | Readable file format | Lean 4 file format | Q130224300 |  |  |  |  | normal |  |
| P1073 | Writable file format | Lean 3 file format | Q130223835 |  |  |  |  | normal |  |
| P1073 | Writable file format | Lean 4 file format | Q130224300 |  |  |  |  | normal |  |
| P2283 | Uses | dependent type | Q997433 |  |  |  |  | normal |  |
| P287 | Designed by | Leonardo de Moura | Q84844322 |  |  |  |  | normal | https://lean-lang.org/about/ |
| P166 | Awards | Programming Languages Software Award | Q61890391 |  |  | 2025-01-01 |  | normal | https://www.sigplan.org/Awards/Software/#2025_Lean_Theorem_Prover |
| P4162 | AUR package | lean-bin |  |  |  |  |  | normal | https://aur.archlinux.org/packages/lean-bin/ |
| P7427 | FreeBSD port | math/lean |  |  |  |  |  | normal | https://www.freshports.org/math/lean |
| P2037 | GitHub account | leanprover |  |  |  |  |  | normal | https://github.com/leanprover |
| P9100 | GitHub topic | lean |  |  |  |  |  | normal | https://github.com/topics/lean |
| P227 | GND ID | 1292701188 |  |  |  |  |  | normal | https://d-nb.info/gnd/1292701188 |
| P2671 | Google Knowledge Graph ID | /g/11j7dt82fy |  |  |  |  |  | normal | https://www.google.com/search?kgmid=/g/11j7dt82fy |
| P8443 | Homebrew formula name | lean |  |  |  |  |  | normal | https://formulae.brew.sh/formula/lean |
| P4215 | NLab ID | Lean |  |  |  |  |  | normal | https://ncatlab.org/nlab/show/Lean |
| P1972 | Open Hub ID | lean |  |  |  |  |  | normal | https://openhub.net/p/lean |
| P6931 | Repology project name | lean |  |  |  |  |  | normal | https://repology.org/project/lean/information |

Source: https://aidb.si/e/lean-Q6509476 — Wikidata (CC0) via AIDB