Home · Browse · Lean4

Lean4

1 program Added 2026-02-26T12:00:00Z Agent: claude-codeModel: claude-sonnet-4-6WebSearch: disabled Evidence Report issue View issues

Aliases: Lean 4, Lean

Provenance: commit 97a33ce529 · authored 2026-02-26T12:14:36+01:00 · agent claude-code · model claude-sonnet-4-6

Sources mentioning this language

5 sources · pl_id: pl/lean-4

LLM (this repo) · 1 Linguist Pygments Wikipedia Wikidata · Q6509476

Wikipedia infobox ↗

Pulled from the wikimedia/structured-wikipedia snapshot — see data/raw/wikipedia_pl_facts.*.jsonl and pl_fact.csv for the long-table provenance.

Paradigms	strict purely functional · dependently typed
Typing	static, strong, inferred
Designed by	Lean FRO · Leonardo de Moura
First appeared	2013
Influenced by	ML · Rocq (formerly named Coq) · Haskell
License	Apache 2.0
Implemented in	Lean · C++
Homepage	http://lean-lang.org

Extensions claimed by this language

2 claims. Each row is one upstream assertion with its strength. SWH column shows file occurrences with that extension across the entire archive.

Extension	Source	Strength	SWH
`.lean`	linguist	primary	1.0M files
`.lean`	pygments	primary	1.0M files

Related languages

Lean 4 (1.00)Lean (0.33)Clean (0.29)Bean (0.21)JEAN (0.21)

LLM-contributed programs

Fibonacci

Origin · Download · manifest.json · Report

Provenance: commit 97a33ce529 · authored 2026-02-26T12:14:36+01:00 · agent claude-code · model claude-sonnet-4-6 · WebSearch disabled

code.lean · license: Public Domain · added: 2026-02-26T12:00:00Z

def fib : Nat → Nat
  | 0 => 0
  | 1 => 1
  | (n + 2) => fib n + fib (n + 1)

#eval fib 10

Real programs from Software Heritage

1 sample mined from derived_datasets/<date>/contents/*.parquet, byte-verified against the SWH archive. Citation-grade qualified SWHIDs preserved.

CvxLeanTest.lean · 52 B · ext .lean · seen 386× in SWH

via heuristicrule h/linguist/.lean/1

swh:1:cnt:4304f49277615a8e932ae620b36a6df9250111d6;origin=https://github.com/verified-optimization/CvxLean;anchor=swh:1:rev:4d8c9ab20d101f9b4e7fb1ca9eaa95080fbfd448;path=/CvxLeanTest.lean

Open in SWH · Raw bytes (SWH) · GitHub raw

Show source

import CvxLean.Test.All
import CvxLean.Examples.All

Disambiguation rules

Linguist heuristic rules that predict this language when one of its claimed extensions is shared with another.

Rule	Ext	Kind	Predicates (truncated)
`h/linguist/.lean/1`	`.lean`	predicates	`[{"kind": "any", "regexes": ["^import [A-Z]"]}]`

Contribute — propose a file extension

Tell us where to find evidence about Lean4 (mapped to pl/lean-4). A reference URL is required; at least one of extension or program code must be provided too. A maintainer reviews each submission via a draft PR before anything lands.

File extension (optional) — e.g. .oak. Some PLs (e.g. esolangs) have no convention; leave empty if so. Friendly name (optional)

Reference URL * — public URL where the extension is used (GitHub file, GitLab, spec page, …) Notes (optional) — 1–3 sentences if context helps the maintainer

Optional: attach a program from that URL

If the reference URL points at a single source file you'd like to add as an example program, paste it below. The workflow will write it under languages/Lean4/programs/<sha>/. Keep under ~200 lines.

Title (optional) — e.g. "Factorial", "Quicksort" License guess (optional) — MIT, GPL-2.0, …

Code (optional) — paste verbatim bytes from the reference URL

(or open the pre-filled issue directly)