iiRecord
Agentic AI Atlas · Lean
language:leana5c.ai
II.
Language JSON

language:lean

Structured · live

Lean json

Inspect the normalized record payload exactly as the atlas UI reads it.

File · domain/languages/lean.yamlCluster · domain
Record JSON
{
  "id": "language:lean",
  "_kind": "Language",
  "_file": "domain/languages/lean.yaml",
  "_cluster": "domain",
  "attributes": {
    "displayName": "Lean",
    "paradigms": [
      "functional",
      "dependently-typed",
      "proof-assistant"
    ],
    "description": "Lean — a dependently-typed functional programming language and\ntheorem prover (Lean 4) developed by Microsoft Research / the Lean\nFRO, paired with the mathlib mathematics library.\n"
  },
  "outgoingEdges": [
    {
      "from": "language:lean",
      "to": "domain:mathematics",
      "kind": "applies_to",
      "attributes": {}
    },
    {
      "from": "language:lean",
      "to": "domain:computer-science",
      "kind": "applies_to",
      "attributes": {}
    }
  ],
  "incomingEdges": []
}