diff --git a/README.md b/README.md
index 08f2838ce..f583fb290 100644
--- a/README.md
+++ b/README.md
@@ -138,7 +138,7 @@ The gains scale with codebase size: on large repos the agent answers from the in
 | **Full-Text Search** | Find code by name instantly across your entire codebase, powered by FTS5 |
 | **Impact Analysis** | Trace callers, callees, and the full impact radius of any symbol before making changes |
 | **Always Fresh** | File watcher uses native OS events (FSEvents/inotify/ReadDirectoryChangesW) with debounced auto-sync — the graph stays current as you code, zero config |
-| **20+ Languages** | TypeScript, JavaScript, Python, Go, Rust, Java, C#, PHP, Ruby, C, C++, Objective-C, Swift, Kotlin, Dart, Lua, Luau, Svelte, Liquid, Pascal/Delphi |
+| **20+ Languages** | TypeScript, JavaScript, Python, Go, Rust, Java, C#, PHP, Ruby, C, C++, Objective-C, Swift, Kotlin, Dart, Lean, Lua, Luau, Svelte, Liquid, Pascal/Delphi |
 | **Framework-aware Routes** | Recognizes web-framework routing files and links URL patterns to their handlers across 14 frameworks |
 | **Mixed iOS / React Native / Expo** | Closes cross-language flows that static parsing misses: Swift ↔ ObjC bridging, React Native legacy bridge + TurboModules + Fabric view components, native → JS event emitters, Expo Modules |
 | **100% Local** | No data leaves your machine. No API keys. No external services. SQLite database only |
@@ -465,7 +465,7 @@ nothing to wire up per language.
 What it skips out of the box:
 
 - **Dependency, build, and cache directories** — `node_modules`, `vendor`,
-  `dist`, `build`, `target`, `.venv`, `Pods`, `.next`, and the like across every
+  `dist`, `build`, `target`, `.lake`, `.venv`, `Pods`, `.next`, and the like across every
   [supported stack](#supported-languages) — so the graph is your code, not
   third-party noise. This holds even with no `.gitignore`.
 - **Anything in your `.gitignore`** — honored in git repos via git, and in
@@ -526,6 +526,7 @@ is written):
 | Kotlin | `.kt`, `.kts` | Full support |
 | Scala | `.scala`, `.sc` | Full support (classes, traits, methods, type aliases, Scala 3 enums) |
 | Dart | `.dart` | Full support |
+| Lean | `.lean` | Static extraction with optional Lean/Lake LSP definition resolution |
 | Svelte | `.svelte` | Full support (script extraction, Svelte 5 runes, SvelteKit routes) |
 | Vue | `.vue` | Full support (script + script-setup extraction, Nuxt page/API/middleware routes) |
 | Liquid | `.liquid` | Full support |
@@ -533,6 +534,13 @@ is written):
 | Lua | `.lua` | Full support (functions, methods with receivers, local variables, `require` imports, call edges) |
 | Luau | `.luau` | Full support (everything in Lua, plus `type`/`export type` aliases, typed signatures, and Roblox instance-path `require`) |
 
+Lean files index without requiring a local Lean toolchain. When available,
+CodeGraph tries `lake env lean --server` (or `lean --server`) for better
+definition edges. Set `CODEGRAPH_LEAN_SEMANTICS=off` to force static-only
+indexing, or override the command with `CODEGRAPH_LEAN_LSP_COMMAND`;
+`CODEGRAPH_LEAN_LSP_TIMEOUT_MS` and `CODEGRAPH_LEAN_LSP_REF_LIMIT` bound the
+best-effort LSP pass.
+
 ## Troubleshooting
 
 **"CodeGraph not initialized"** — Run `codegraph init` in your project directory first.
@@ -546,7 +554,7 @@ is written):
 
 **MCP server not connecting** — Ensure the project is initialized/indexed, verify the path in your MCP config, and check that `codegraph serve --mcp` works from the command line.
 
-**Missing symbols** — The MCP server auto-syncs on save (wait a couple seconds). Run `codegraph sync` manually if needed. Check that the file's language is supported and isn't inside a `.gitignore`d or default-excluded directory (e.g. `node_modules`, `dist`).
+**Missing symbols** — The MCP server auto-syncs on save (wait a couple seconds). Run `codegraph sync` manually if needed. Check that the file's language is supported and isn't inside a `.gitignore`d or default-excluded directory (e.g. `node_modules`, `dist`, `.lake`).
 
 ## Star History
 
diff --git a/__tests__/lean-extraction.test.ts b/__tests__/lean-extraction.test.ts
new file mode 100644
index 000000000..1e922c712
--- /dev/null
+++ b/__tests__/lean-extraction.test.ts
@@ -0,0 +1,408 @@
+import { describe, expect, it, beforeAll } from 'vitest';
+import * as fs from 'fs';
+import * as os from 'os';
+import * as path from 'path';
+import { CodeGraph } from '../src';
+import { DatabaseConnection } from '../src/db';
+import { extractFromSource, scanDirectory } from '../src/extraction';
+import {
+  detectLanguage,
+  getLanguageDisplayName,
+  getSupportedLanguages,
+  initGrammars,
+  isGrammarLoaded,
+  isLanguageSupported,
+  loadGrammarsForLanguages,
+} from '../src/extraction/grammars';
+
+beforeAll(async () => {
+  await initGrammars();
+  await loadGrammarsForLanguages(['lean']);
+});
+
+const LEAN_ENV_KEYS = [
+  'CODEGRAPH_LEAN_SEMANTICS',
+  'CODEGRAPH_LEAN_LSP_COMMAND',
+  'CODEGRAPH_LEAN_LSP_TIMEOUT_MS',
+  'CODEGRAPH_LEAN_LSP_REF_LIMIT',
+  'FAKE_LEAN_TARGET_URI',
+  'FAKE_LEAN_TARGET_LINE',
+  'FAKE_LEAN_TARGET_COLUMN',
+  'FAKE_LEAN_SKIP_DEFINITION',
+] as const;
+
+function snapshotLeanEnv(): Partial<Record<typeof LEAN_ENV_KEYS[number], string>> {
+  const snapshot: Partial<Record<typeof LEAN_ENV_KEYS[number], string>> = {};
+  for (const key of LEAN_ENV_KEYS) {
+    if (process.env[key] !== undefined) snapshot[key] = process.env[key];
+  }
+  return snapshot;
+}
+
+function restoreLeanEnv(snapshot: Partial<Record<typeof LEAN_ENV_KEYS[number], string>>): void {
+  for (const key of LEAN_ENV_KEYS) {
+    if (snapshot[key] === undefined) {
+      delete process.env[key];
+    } else {
+      process.env[key] = snapshot[key];
+    }
+  }
+}
+
+function writeFakeLeanLsp(): string {
+  const serverPath = path.join(os.tmpdir(), `codegraph-fake-lean-lsp-${process.pid}-${Date.now()}.cjs`);
+  fs.writeFileSync(serverPath, String.raw`
+const { pathToFileURL } = require('url');
+
+let buffer = Buffer.alloc(0);
+
+function send(message) {
+  const body = Buffer.from(JSON.stringify(message), 'utf8');
+  process.stdout.write(Buffer.from('Content-Length: ' + body.length + '\r\n\r\n', 'ascii'));
+  process.stdout.write(body);
+}
+
+function handle(message) {
+  if (!message || !message.id) return;
+  if (message.method === 'initialize') {
+    send({ jsonrpc: '2.0', id: message.id, result: { capabilities: { definitionProvider: true } } });
+    return;
+  }
+  if (message.method === 'textDocument/definition') {
+    if (process.env.FAKE_LEAN_SKIP_DEFINITION === '1') return;
+    const uri = process.env.FAKE_LEAN_TARGET_URI || pathToFileURL('/tmp/outside.lean').href;
+    const line = Number.parseInt(process.env.FAKE_LEAN_TARGET_LINE || '0', 10);
+    const character = Number.parseInt(process.env.FAKE_LEAN_TARGET_COLUMN || '0', 10);
+    send({
+      jsonrpc: '2.0',
+      id: message.id,
+      result: {
+        uri,
+        range: {
+          start: { line, character },
+          end: { line, character: character + 6 },
+        },
+      },
+    });
+  }
+}
+
+process.stdin.on('data', (chunk) => {
+  buffer = Buffer.concat([buffer, chunk]);
+  while (true) {
+    const headerEnd = buffer.indexOf('\r\n\r\n');
+    if (headerEnd < 0) return;
+    const header = buffer.slice(0, headerEnd).toString('ascii');
+    const match = header.match(/Content-Length:\s*(\d+)/i);
+    if (!match) {
+      buffer = buffer.slice(headerEnd + 4);
+      continue;
+    }
+    const length = Number.parseInt(match[1], 10);
+    const start = headerEnd + 4;
+    const end = start + length;
+    if (buffer.length < end) return;
+    const body = buffer.slice(start, end).toString('utf8');
+    buffer = buffer.slice(end);
+    try {
+      handle(JSON.parse(body));
+    } catch {
+      // Ignore malformed input.
+    }
+  }
+});
+`, 'utf-8');
+  return serverPath;
+}
+
+describe('Lean support', () => {
+  it('detects and reports Lean as a grammar-backed supported language', () => {
+    expect(detectLanguage('Example.lean')).toBe('lean');
+    expect(isLanguageSupported('lean')).toBe(true);
+    expect(isGrammarLoaded('lean')).toBe(true);
+    expect(getSupportedLanguages()).toContain('lean');
+    expect(getLanguageDisplayName('lean')).toBe('Lean');
+  });
+
+  it('extracts namespaces, imports, declarations, fields, constructors, docs, visibility, and references', () => {
+    const code = `
+import Foo.Bar
+
+namespace Demo
+
+/-- doubles a number -/
+def twice (n : Nat) : Nat := Nat.succ n
+
+private lemma hidden : twice 0 = 1 := by
+  rfl
+
+structure Point where
+  /-- x coordinate -/
+  x : Nat
+  y : Nat := Nat.zero
+
+class Size (α : Type) where
+  size : α → Nat
+
+inductive Color where
+  | red
+  | blue : Color
+
+opaque mystery : Nat
+axiom trusted : Nat
+constant answer : Nat
+abbrev Alias := Nat
+
+end Demo
+`;
+
+    const result = extractFromSource('Demo.lean', code);
+    expect(result.errors).toHaveLength(0);
+
+    expect(result.nodes.find((n) => n.kind === 'file' && n.language === 'lean')).toBeDefined();
+    expect(result.nodes.find((n) => n.kind === 'import' && n.name === 'Foo.Bar')).toBeDefined();
+    expect(result.nodes.find((n) => n.kind === 'namespace' && n.qualifiedName === 'Demo')).toBeDefined();
+
+    const twice = result.nodes.find((n) => n.kind === 'function' && n.qualifiedName === 'Demo.twice');
+    expect(twice?.docstring).toBe('doubles a number');
+    expect(twice?.isExported).toBe(true);
+
+    const hidden = result.nodes.find((n) => n.name === 'hidden');
+    expect(hidden).toMatchObject({ kind: 'function', visibility: 'private', isExported: false });
+
+    expect(result.nodes.find((n) => n.kind === 'struct' && n.qualifiedName === 'Demo.Point')).toBeDefined();
+    expect(result.nodes.find((n) => n.kind === 'class' && n.qualifiedName === 'Demo.Size')).toBeDefined();
+    expect(result.nodes.find((n) => n.kind === 'enum' && n.qualifiedName === 'Demo.Color')).toBeDefined();
+    expect(result.nodes.find((n) => n.kind === 'field' && n.qualifiedName === 'Demo.Point.x')).toMatchObject({
+      docstring: 'x coordinate',
+    });
+    expect(result.nodes.find((n) => n.kind === 'field' && n.qualifiedName === 'Demo.Size.size')).toBeDefined();
+    expect(result.nodes.find((n) => n.kind === 'enum_member' && n.qualifiedName === 'Demo.Color.red')).toBeDefined();
+    expect(result.nodes.find((n) => n.kind === 'enum_member' && n.qualifiedName === 'Demo.Color.blue')).toBeDefined();
+    expect(result.nodes.find((n) => n.kind === 'type_alias' && n.qualifiedName === 'Demo.Alias')).toBeDefined();
+    expect(result.nodes.find((n) => n.kind === 'constant' && n.qualifiedName === 'Demo.trusted')).toBeDefined();
+
+    expect(result.unresolvedReferences).toEqual(expect.arrayContaining([
+      expect.objectContaining({ referenceKind: 'imports', referenceName: 'Foo.Bar' }),
+      expect.objectContaining({ referenceKind: 'calls', referenceName: 'Nat.succ' }),
+      expect.objectContaining({ referenceKind: 'calls', referenceName: 'twice' }),
+      expect.objectContaining({ referenceKind: 'references', referenceName: 'Nat' }),
+    ]));
+    expect(result.unresolvedReferences.some((r) => r.fromNodeId === twice?.id && r.referenceName === 'twice')).toBe(false);
+  });
+
+  it('extracts Lean open/export/section/attributes/extends/anonymous instances and candidates', () => {
+    const code = `
+import Foo.Bar
+open Helpers
+export Helpers (helper)
+
+namespace Demo
+section Tools
+
+@[simp, inline] def use (n : Nat) : Nat := helper n
+
+structure Point extends ToString where
+  x : Nat
+
+class Sized (α : Type) extends Inhabited α where
+  size : α → Nat
+
+instance : Inhabited Point where
+  default := { x := 0 }
+
+theorem t : use 0 = 0 := by
+  simp [use]
+
+end Tools
+end Demo
+`;
+
+    const result = extractFromSource('Demo.lean', code);
+    expect(result.errors).toHaveLength(0);
+
+    expect(result.nodes.find((n) => n.kind === 'import' && n.name === 'open Helpers')).toBeDefined();
+    expect(result.nodes.find((n) => n.kind === 'export' && n.name === 'Helpers (helper)')).toBeDefined();
+    expect(result.nodes.find((n) => n.kind === 'module' && n.name === 'Tools')).toBeDefined();
+
+    const use = result.nodes.find((n) => n.kind === 'function' && n.qualifiedName === 'Demo.use');
+    expect(use?.decorators).toEqual(['simp', 'inline']);
+
+    expect(result.nodes.find((n) => n.kind === 'constant' && n.name.startsWith('instInhabitedPoint@'))).toBeDefined();
+    expect(result.unresolvedReferences).toEqual(expect.arrayContaining([
+      expect.objectContaining({
+        referenceKind: 'extends',
+        referenceName: 'ToString',
+        candidates: expect.arrayContaining(['Demo.ToString', 'Helpers.ToString']),
+      }),
+      expect.objectContaining({
+        referenceKind: 'extends',
+        referenceName: 'Inhabited',
+        candidates: expect.arrayContaining(['Demo.Inhabited', 'Helpers.Inhabited']),
+      }),
+      expect.objectContaining({
+        referenceKind: 'calls',
+        referenceName: 'helper',
+        candidates: expect.arrayContaining(['Demo.helper', 'Helpers.helper', 'Foo.Bar.helper']),
+      }),
+      expect.objectContaining({
+        referenceKind: 'references',
+        referenceName: 'use',
+        candidates: expect.arrayContaining(['Demo.use']),
+      }),
+    ]));
+  });
+
+  it('resolves local Lean module imports and qualified calls end-to-end', async () => {
+    const env = snapshotLeanEnv();
+    process.env.CODEGRAPH_LEAN_SEMANTICS = 'off';
+    const tempProject = fs.mkdtempSync(path.join(os.tmpdir(), 'codegraph-lean-e2e-'));
+    let cg: CodeGraph | null = null;
+    try {
+      fs.mkdirSync(path.join(tempProject, 'Foo'), { recursive: true });
+      fs.writeFileSync(
+        path.join(tempProject, 'Foo', 'Bar.lean'),
+        `namespace Foo\n\ndef bar (n : Nat) : Nat := n\n\nend Foo\n`
+      );
+      fs.writeFileSync(
+        path.join(tempProject, 'Main.lean'),
+        `import Foo.Bar\n\nnamespace Main\n\ndef main : Nat := Foo.bar 1\n\nend Main\n`
+      );
+
+      cg = await CodeGraph.init(tempProject, { index: true });
+      const db = DatabaseConnection.open(path.join(tempProject, '.codegraph', 'codegraph.db'));
+      const rows = db.getDb().prepare(`
+        select src.kind as srcKind, src.file_path as srcPath, dst.kind as dstKind,
+               dst.file_path as dstPath, dst.qualified_name as dstQName, e.kind as edgeKind
+        from edges e
+        join nodes src on e.source = src.id
+        join nodes dst on e.target = dst.id
+        where src.file_path = 'Main.lean'
+      `).all() as Array<{
+        srcKind: string;
+        srcPath: string;
+        dstKind: string;
+        dstPath: string;
+        dstQName: string;
+        edgeKind: string;
+      }>;
+      db.close();
+
+      expect(rows.some((r) =>
+        r.srcKind === 'file' &&
+        r.edgeKind === 'imports' &&
+        r.dstKind === 'file' &&
+        r.dstPath === 'Foo/Bar.lean'
+      )).toBe(true);
+      expect(rows.some((r) =>
+        r.edgeKind === 'calls' &&
+        r.dstKind === 'function' &&
+        r.dstQName === 'Foo.bar'
+      )).toBe(true);
+    } finally {
+      if (cg) cg.destroy();
+      fs.rmSync(tempProject, { recursive: true, force: true });
+      restoreLeanEnv(env);
+    }
+  });
+
+  it('uses fake Lean LSP definition results when semantic resolution is available', async () => {
+    const env = snapshotLeanEnv();
+    const tempProject = fs.mkdtempSync(path.join(os.tmpdir(), 'codegraph-lean-lsp-'));
+    const fakeServer = writeFakeLeanLsp();
+    let cg: CodeGraph | null = null;
+    try {
+      fs.writeFileSync(path.join(tempProject, 'Lib.lean'), `namespace Lib\n\ndef target : Nat := 1\n\nend Lib\n`);
+      fs.writeFileSync(path.join(tempProject, 'Main.lean'), `import Lib\n\nnamespace Main\n\ndef caller : Nat := alias 0\n\nend Main\n`);
+
+      process.env.CODEGRAPH_LEAN_SEMANTICS = 'auto';
+      process.env.CODEGRAPH_LEAN_LSP_COMMAND = `${process.execPath} ${fakeServer}`;
+      process.env.CODEGRAPH_LEAN_LSP_TIMEOUT_MS = '1000';
+      process.env.CODEGRAPH_LEAN_LSP_REF_LIMIT = '10';
+      process.env.FAKE_LEAN_TARGET_URI = new URL(`file://${path.join(tempProject, 'Lib.lean')}`).href;
+      process.env.FAKE_LEAN_TARGET_LINE = '2';
+      process.env.FAKE_LEAN_TARGET_COLUMN = '4';
+
+      cg = await CodeGraph.init(tempProject, { index: true });
+      const caller = cg.getNodesByKind('function').find((n) => n.name === 'caller');
+      expect(caller).toBeDefined();
+      const edge = cg.getOutgoingEdges(caller!.id).find((e) => e.kind === 'calls');
+      expect(edge?.metadata?.resolvedBy).toBe('lean-lsp');
+      expect(cg.getNode(edge!.target)?.qualifiedName).toBe('Lib.target');
+    } finally {
+      if (cg) cg.destroy();
+      fs.rmSync(tempProject, { recursive: true, force: true });
+      fs.rmSync(fakeServer, { force: true });
+      restoreLeanEnv(env);
+    }
+  });
+
+  it('falls back when Lean LSP returns a project-external location, times out, or is disabled', async () => {
+    const run = async (configure: (project: string, fakeServer: string) => void) => {
+      const env = snapshotLeanEnv();
+      const tempProject = fs.mkdtempSync(path.join(os.tmpdir(), 'codegraph-lean-lsp-fallback-'));
+      const fakeServer = writeFakeLeanLsp();
+      let cg: CodeGraph | null = null;
+      try {
+        fs.writeFileSync(path.join(tempProject, 'Lib.lean'), `namespace Lib\n\ndef target : Nat := 1\n\nend Lib\n`);
+        fs.writeFileSync(path.join(tempProject, 'Main.lean'), `import Lib\n\nnamespace Main\n\ndef caller : Nat := alias 0\n\nend Main\n`);
+        configure(tempProject, fakeServer);
+
+        cg = await CodeGraph.init(tempProject, { index: true });
+        const caller = cg.getNodesByKind('function').find((n) => n.name === 'caller');
+        expect(caller).toBeDefined();
+        expect(cg.getOutgoingEdges(caller!.id).filter((e) => e.kind === 'calls')).toHaveLength(0);
+      } finally {
+        if (cg) cg.destroy();
+        fs.rmSync(tempProject, { recursive: true, force: true });
+        fs.rmSync(fakeServer, { force: true });
+        restoreLeanEnv(env);
+      }
+    };
+
+    await run((_project, fakeServer) => {
+      process.env.CODEGRAPH_LEAN_SEMANTICS = 'auto';
+      process.env.CODEGRAPH_LEAN_LSP_COMMAND = `${process.execPath} ${fakeServer}`;
+      process.env.CODEGRAPH_LEAN_LSP_TIMEOUT_MS = '1000';
+      process.env.FAKE_LEAN_TARGET_URI = new URL('file:///tmp/outside.lean').href;
+    });
+
+    await run((project, fakeServer) => {
+      process.env.CODEGRAPH_LEAN_SEMANTICS = 'auto';
+      process.env.CODEGRAPH_LEAN_LSP_COMMAND = `${process.execPath} ${fakeServer}`;
+      process.env.CODEGRAPH_LEAN_LSP_TIMEOUT_MS = '50';
+      process.env.FAKE_LEAN_SKIP_DEFINITION = '1';
+      process.env.FAKE_LEAN_TARGET_URI = new URL(`file://${path.join(project, 'Lib.lean')}`).href;
+    });
+
+    await run((project, fakeServer) => {
+      process.env.CODEGRAPH_LEAN_SEMANTICS = 'off';
+      process.env.CODEGRAPH_LEAN_LSP_COMMAND = `${process.execPath} ${fakeServer}`;
+      process.env.FAKE_LEAN_TARGET_URI = new URL(`file://${path.join(project, 'Lib.lean')}`).href;
+      process.env.FAKE_LEAN_TARGET_LINE = '2';
+      process.env.FAKE_LEAN_TARGET_COLUMN = '4';
+    });
+  });
+
+  it('skips Lake dependency packages by default unless explicitly unignored', () => {
+    const tempProject = fs.mkdtempSync(path.join(os.tmpdir(), 'codegraph-lean-ignore-'));
+    try {
+      fs.mkdirSync(path.join(tempProject, '.lake', 'packages', 'Dep'), { recursive: true });
+      fs.writeFileSync(path.join(tempProject, 'Main.lean'), 'def main := 1\n');
+      fs.writeFileSync(path.join(tempProject, '.lake', 'packages', 'Dep', 'Lib.lean'), 'def dep := 1\n');
+
+      let files = scanDirectory(tempProject);
+      expect(files).toContain('Main.lean');
+      expect(files).not.toContain('.lake/packages/Dep/Lib.lean');
+
+      fs.writeFileSync(
+        path.join(tempProject, '.gitignore'),
+        '!.lake/\n!.lake/packages/\n!.lake/packages/**\n'
+      );
+      files = scanDirectory(tempProject);
+      expect(files).toContain('.lake/packages/Dep/Lib.lean');
+    } finally {
+      fs.rmSync(tempProject, { recursive: true, force: true });
+    }
+  });
+});
diff --git a/__tests__/resolution.test.ts b/__tests__/resolution.test.ts
index 03b8ea6ab..6109c7662 100644
--- a/__tests__/resolution.test.ts
+++ b/__tests__/resolution.test.ts
@@ -268,6 +268,55 @@ describe('Resolution Module', () => {
       expect(result).not.toBeNull();
       expect(result?.targetNodeId).toBe('method:user.ts:User.save:15');
     });
+
+    it('should prefer extractor-provided qualified candidates', () => {
+      const preferred: Node = {
+        id: 'func:src/Demo/Helpers.lean:helper:3',
+        kind: 'function',
+        name: 'helper',
+        qualifiedName: 'Demo.Helpers.helper',
+        filePath: 'src/Demo/Helpers.lean',
+        language: 'lean',
+        startLine: 3,
+        endLine: 3,
+        startColumn: 0,
+        endColumn: 30,
+        updatedAt: Date.now(),
+      };
+      const unrelated: Node = {
+        ...preferred,
+        id: 'func:src/Other.lean:helper:3',
+        qualifiedName: 'Other.helper',
+        filePath: 'src/Other.lean',
+      };
+
+      const context: ResolutionContext = {
+        getNodesInFile: () => [],
+        getNodesByName: (name) => name === 'helper' ? [unrelated, preferred] : [],
+        getNodesByQualifiedName: (qualifiedName) => qualifiedName === 'Demo.Helpers.helper' ? [preferred] : [],
+        getNodesByKind: () => [],
+        fileExists: () => true,
+        readFile: () => null,
+        getProjectRoot: () => '/test',
+        getAllFiles: () => ['src/Demo/Helpers.lean', 'src/Other.lean'],
+        getNodesByLowerName: () => [],
+        getImportMappings: () => [],
+      };
+
+      const result = matchReference({
+        fromNodeId: 'func:src/Main.lean:caller:10',
+        referenceName: 'helper',
+        referenceKind: 'calls',
+        line: 10,
+        column: 8,
+        filePath: 'src/Main.lean',
+        language: 'lean',
+        candidates: ['Demo.Helpers.helper', 'Other.helper'],
+      }, context);
+
+      expect(result?.targetNodeId).toBe(preferred.id);
+      expect(result?.resolvedBy).toBe('qualified-name');
+    });
   });
 
   describe('Import Resolver', () => {
@@ -352,6 +401,40 @@ from ..services import auth_service
       expect(mappings.some((m) => m.localName === 'helper')).toBe(true);
       expect(mappings.some((m) => m.localName === 'User')).toBe(true);
     });
+
+    it('should resolve Lean module imports by exact path or one unique suffix match', () => {
+      const makeContext = (files: string[], exists: (p: string) => boolean): ResolutionContext => ({
+        getNodesInFile: () => [],
+        getNodesByName: () => [],
+        getNodesByQualifiedName: () => [],
+        getNodesByKind: () => [],
+        fileExists: exists,
+        readFile: () => null,
+        getProjectRoot: () => '',
+        getAllFiles: () => files,
+      });
+
+      expect(resolveImportPath(
+        'Foo.Bar',
+        'Main.lean',
+        'lean',
+        makeContext(['Foo/Bar.lean'], (p) => p === 'Foo/Bar.lean')
+      )).toBe('Foo/Bar.lean');
+
+      expect(resolveImportPath(
+        'Foo.Bar',
+        'src/Main.lean',
+        'lean',
+        makeContext(['src/Foo/Bar.lean'], () => false)
+      )).toBe('src/Foo/Bar.lean');
+
+      expect(resolveImportPath(
+        'Foo.Bar',
+        'src/Main.lean',
+        'lean',
+        makeContext(['src/Foo/Bar.lean', 'vendor/Foo/Bar.lean'], () => false)
+      )).toBeNull();
+    });
   });
 
   describe('JVM FQN Import Resolution', () => {
diff --git a/site/src/content/docs/getting-started/configuration.md b/site/src/content/docs/getting-started/configuration.md
index bba4ddb92..01bea5630 100644
--- a/site/src/content/docs/getting-started/configuration.md
+++ b/site/src/content/docs/getting-started/configuration.md
@@ -7,7 +7,7 @@ There isn't any — CodeGraph is **zero-config**, with **no config file** to wri
 
 ## What it skips out of the box
 
-- **Dependency, build, and cache directories** — `node_modules`, `vendor`, `dist`, `build`, `target`, `.venv`, `Pods`, `.next`, and the like across every [supported stack](/codegraph/reference/languages/) — so the graph is your code, not third-party noise. This holds even with no `.gitignore`.
+- **Dependency, build, and cache directories** — `node_modules`, `vendor`, `dist`, `build`, `target`, `.lake`, `.venv`, `Pods`, `.next`, and the like across every [supported stack](/codegraph/reference/languages/) — so the graph is your code, not third-party noise. This holds even with no `.gitignore`.
 - **Anything in your `.gitignore`** — honored in git repos via git, and in non-git projects by reading `.gitignore` directly (root and nested).
 - **Files larger than 1 MB** — generated bundles, minified JS, vendored blobs.
 
diff --git a/site/src/content/docs/guides/indexing.md b/site/src/content/docs/guides/indexing.md
index 7c0fd1ddc..d9437f309 100644
--- a/site/src/content/docs/guides/indexing.md
+++ b/site/src/content/docs/guides/indexing.md
@@ -98,4 +98,4 @@ Reports node/edge/file counts, the active SQLite backend, and the journal mode.
 
 ## What gets indexed
 
-Every file whose extension maps to a [supported language](/codegraph/reference/languages/), minus dependency/build directories excluded by default (`node_modules`, `vendor`, `dist`, …), anything your `.gitignore` excludes, and files over 1 MB. See [Configuration](/codegraph/getting-started/configuration/).
+Every file whose extension maps to a [supported language](/codegraph/reference/languages/), minus dependency/build directories excluded by default (`node_modules`, `vendor`, `dist`, `.lake`, …), anything your `.gitignore` excludes, and files over 1 MB. See [Configuration](/codegraph/getting-started/configuration/).
diff --git a/site/src/content/docs/reference/languages.md b/site/src/content/docs/reference/languages.md
index 184b579ac..602e8946b 100644
--- a/site/src/content/docs/reference/languages.md
+++ b/site/src/content/docs/reference/languages.md
@@ -22,9 +22,12 @@ Language support is automatic from the file extension — there's nothing to con
 | Kotlin | `.kt`, `.kts` | Full support |
 | Scala | `.scala`, `.sc` | Full support (classes, traits, methods, type aliases, Scala 3 enums) |
 | Dart | `.dart` | Full support |
+| Lean | `.lean` | Static extraction with optional Lean/Lake LSP definition resolution |
 | Svelte | `.svelte` | Full support (script extraction, Svelte 5 runes, SvelteKit routes) |
 | Vue | `.vue` | Full support (script + script-setup, Nuxt page/API/middleware routes) |
 | Liquid | `.liquid` | Full support |
 | Pascal / Delphi | `.pas`, `.dpr`, `.dpk`, `.lpr` | Full support (classes, records, interfaces, enums, DFM/FMX forms) |
 | Lua | `.lua` | Full support (functions, methods, locals, `require` imports, call edges) |
 | Luau | `.luau` | Full support (Lua, plus typed signatures, `type` aliases, Roblox `require`) |
+
+Lean files are indexed without requiring Lean locally. If `lake` or `lean` is available, CodeGraph runs a best-effort LSP definition pass for unresolved Lean references. Set `CODEGRAPH_LEAN_SEMANTICS=off` to force static-only indexing, or override the command with `CODEGRAPH_LEAN_LSP_COMMAND`. `CODEGRAPH_LEAN_LSP_TIMEOUT_MS` and `CODEGRAPH_LEAN_LSP_REF_LIMIT` cap the optional pass.
diff --git a/site/src/content/docs/troubleshooting.md b/site/src/content/docs/troubleshooting.md
index 2a4de29ef..33f9c27cd 100644
--- a/site/src/content/docs/troubleshooting.md
+++ b/site/src/content/docs/troubleshooting.md
@@ -24,4 +24,4 @@ Ensure the project is initialized/indexed, verify the path in your MCP config, a
 
 ## Missing symbols
 
-The MCP server auto-syncs on save (wait a couple of seconds). Run `codegraph sync` manually if needed. Check that the file's language is [supported](/codegraph/reference/languages/) and isn't excluded by `.gitignore`.
+The MCP server auto-syncs on save (wait a couple of seconds). Run `codegraph sync` manually if needed. Check that the file's language is [supported](/codegraph/reference/languages/) and isn't excluded by `.gitignore` or a default-excluded directory such as `node_modules`, `dist`, or `.lake`.
diff --git a/src/extraction/grammars.ts b/src/extraction/grammars.ts
index c9a2bcb37..6c11f95ee 100644
--- a/src/extraction/grammars.ts
+++ b/src/extraction/grammars.ts
@@ -14,7 +14,7 @@ export type GrammarLanguage = Exclude<Language, 'svelte' | 'vue' | 'liquid' | 'y
 
 /**
  * WASM filename map — maps each language to its .wasm grammar file
- * in the tree-sitter-wasms package.
+ * in tree-sitter-wasms or src/extraction/wasm for vendored grammars.
  */
 const WASM_GRAMMAR_FILES: Record<GrammarLanguage, string> = {
   typescript: 'tree-sitter-typescript.wasm',
@@ -38,6 +38,7 @@ const WASM_GRAMMAR_FILES: Record<GrammarLanguage, string> = {
   lua: 'tree-sitter-lua.wasm',
   luau: 'tree-sitter-luau.wasm',
   objc: 'tree-sitter-objc.wasm',
+  lean: 'tree-sitter-lean.wasm',
 };
 
 /**
@@ -95,6 +96,7 @@ export const EXTENSION_MAP: Record<string, Language> = {
   '.luau': 'luau',
   '.m': 'objc',
   '.mm': 'objc',
+  '.lean': 'lean',
   // XML: file-level tracking; the MyBatis extractor matches `<mapper namespace="...">`
   // shape and emits SQL-statement nodes (other XML returns empty).
   '.xml': 'xml',
@@ -179,7 +181,7 @@ export async function loadGrammarsForLanguages(languages: Language[]): Promise<v
       // ABI-13 build that corrupts the shared WASM heap under web-tree-sitter
       // 0.25 (drops nested calls/imports on every file after the first); we
       // vendor the upstream ABI-15 wasm instead.
-      const wasmPath = (lang === 'pascal' || lang === 'scala' || lang === 'lua' || lang === 'luau')
+      const wasmPath = (lang === 'pascal' || lang === 'scala' || lang === 'lua' || lang === 'luau' || lang === 'lean')
         ? path.join(__dirname, 'wasm', wasmFile)
         : require.resolve(`tree-sitter-wasms/out/${wasmFile}`);
       const language = await WasmLanguage.load(wasmPath);
@@ -378,6 +380,7 @@ export function getLanguageDisplayName(language: Language): string {
     lua: 'Lua',
     luau: 'Luau',
     objc: 'Objective-C',
+    lean: 'Lean',
     yaml: 'YAML',
     twig: 'Twig',
     xml: 'XML',
diff --git a/src/extraction/index.ts b/src/extraction/index.ts
index 42037d7f6..cecadeed9 100644
--- a/src/extraction/index.ts
+++ b/src/extraction/index.ts
@@ -131,6 +131,8 @@ const DEFAULT_IGNORE_DIRS: ReadonlySet<string> = new Set([
   '.ipynb_checkpoints', '.eggs',
   // Rust / JVM (Maven, Gradle, Scala)
   'target', '.gradle',
+  // Lean / Lake
+  '.lake',
   // .NET
   'obj',
   // Vendored deps (Go, PHP/Composer, Ruby/Bundler)
diff --git a/src/extraction/lean-extractor.ts b/src/extraction/lean-extractor.ts
new file mode 100644
index 000000000..e697ba4c5
--- /dev/null
+++ b/src/extraction/lean-extractor.ts
@@ -0,0 +1,848 @@
+import * as path from 'path';
+import { Node as SyntaxNode, Tree } from 'web-tree-sitter';
+import {
+  Edge,
+  ExtractionError,
+  ExtractionResult,
+  Node,
+  NodeKind,
+  UnresolvedReference,
+} from '../types';
+import { getParser } from './grammars';
+import { generateNodeId, getChildByField, getNodeText } from './tree-sitter-helpers';
+
+type ScopeFrame =
+  | { type: 'namespace'; nodeId: string; qualifiedName: string; opens: string[] }
+  | { type: 'section'; nodeId: string | null; name: string; opens: string[] };
+
+const DECLARATION_TYPES = new Set([
+  'def',
+  'theorem',
+  'abbrev',
+  'instance',
+  'axiom',
+  'opaque',
+  'constant',
+  'structure',
+  'inductive',
+]);
+
+const DECL_NAME_NODE_TYPES = new Set([
+  'def',
+  'theorem',
+  'abbrev',
+  'instance',
+  'axiom',
+  'opaque',
+  'constant',
+  'structure',
+  'inductive',
+  'field',
+  'ctor',
+  'ctor_alt',
+  'struct_field',
+  'namespace',
+  'import',
+  'open',
+  'export',
+]);
+
+const BINDER_NODE_TYPES = new Set([
+  'binders',
+  'explicit_binder',
+  'implicit_binder',
+  'strict_implicit_binder',
+  'inst_implicit_binder',
+  'tuple_binder',
+  'anon_ctor_binder',
+  'binder_predicate',
+]);
+
+/**
+ * Lean 4 extractor backed by tree-sitter-lean.
+ *
+ * The Lean grammar deliberately represents `namespace` / `section` / `end`
+ * as flat top-level commands. This extractor reconstructs namespace scope
+ * while using the AST for declarations, fields, constructors, and references.
+ */
+export class LeanExtractor {
+  private filePath: string;
+  private source: string;
+  private tree: Tree | null = null;
+  private nodes: Node[] = [];
+  private edges: Edge[] = [];
+  private unresolvedReferences: UnresolvedReference[] = [];
+  private errors: ExtractionError[] = [];
+  private scopeStack: ScopeFrame[] = [];
+  private moduleOpenNamespaces: string[] = [];
+  private importedModules: string[] = [];
+
+  constructor(filePath: string, source: string) {
+    this.filePath = filePath;
+    this.source = source;
+  }
+
+  extract(): ExtractionResult {
+    const startTime = Date.now();
+
+    const parser = getParser('lean');
+    if (!parser) {
+      return {
+        nodes: [],
+        edges: [],
+        unresolvedReferences: [],
+        errors: [
+          {
+            message: 'Failed to get parser for language: lean',
+            filePath: this.filePath,
+            severity: 'error',
+            code: 'parser_error',
+          },
+        ],
+        durationMs: Date.now() - startTime,
+      };
+    }
+
+    try {
+      this.tree = parser.parse(this.source) ?? null;
+      if (!this.tree) throw new Error('Parser returned null tree');
+
+      const fileNode = this.createFileNode();
+      this.visitModule(fileNode.id, this.tree.rootNode);
+      this.closeOpenNamespaces(fileNode.endLine);
+    } catch (error) {
+      const msg = error instanceof Error ? error.message : String(error);
+      if (msg.includes('memory access out of bounds') || msg.includes('out of memory')) {
+        throw error;
+      }
+      this.errors.push({
+        message: `Lean extraction error: ${msg}`,
+        filePath: this.filePath,
+        severity: 'error',
+        code: 'parse_error',
+      });
+    } finally {
+      if (this.tree) {
+        this.tree.delete();
+        this.tree = null;
+      }
+    }
+
+    return {
+      nodes: this.nodes,
+      edges: this.edges,
+      unresolvedReferences: this.unresolvedReferences,
+      errors: this.errors,
+      durationMs: Date.now() - startTime,
+    };
+  }
+
+  private createFileNode(): Node {
+    const lines = this.source.split('\n');
+    const fileNode: Node = {
+      id: `file:${this.filePath}`,
+      kind: 'file',
+      name: path.basename(this.filePath),
+      qualifiedName: this.filePath,
+      filePath: this.filePath,
+      language: 'lean',
+      startLine: 1,
+      endLine: lines.length,
+      startColumn: 0,
+      endColumn: lines[lines.length - 1]?.length ?? 0,
+      isExported: false,
+      updatedAt: Date.now(),
+    };
+    this.nodes.push(fileNode);
+    return fileNode;
+  }
+
+  private visitModule(fileNodeId: string, root: SyntaxNode): void {
+    for (let i = 0; i < root.namedChildCount; i++) {
+      const child = root.namedChild(i);
+      if (!child) continue;
+
+      if (child.type === 'import') {
+        this.extractImport(fileNodeId, child);
+      } else if (child.type === 'open') {
+        this.extractOpen(fileNodeId, child);
+      } else if (child.type === 'export') {
+        this.extractExport(fileNodeId, child);
+      } else if (child.type === 'namespace') {
+        this.enterNamespace(fileNodeId, child);
+      } else if (child.type === 'section') {
+        this.enterSection(fileNodeId, child);
+      } else if (child.type === 'end') {
+        this.exitScope(child);
+      } else if (child.type === 'declaration') {
+        this.extractDeclaration(fileNodeId, child);
+      }
+    }
+  }
+
+  private extractImport(fileNodeId: string, node: SyntaxNode): void {
+    const nameNode = getChildByField(node, 'name');
+    if (!nameNode) return;
+    const moduleName = getNodeText(nameNode, this.source);
+    this.importedModules.push(moduleName);
+    const importNode = this.createNode(fileNodeId, 'import', moduleName, node, {
+      qualifiedName: `${this.filePath}::import:${moduleName}`,
+      signature: getNodeText(node, this.source).trim(),
+      isExported: false,
+    });
+    if (!importNode) return;
+
+    this.unresolvedReferences.push({
+      fromNodeId: fileNodeId,
+      referenceName: moduleName,
+      referenceKind: 'imports',
+      line: node.startPosition.row + 1,
+      column: node.startPosition.column,
+      filePath: this.filePath,
+      language: 'lean',
+    });
+  }
+
+  private extractOpen(fileNodeId: string, node: SyntaxNode): void {
+    const openedNamespaces: string[] = [];
+    const openedScopes: string[] = [];
+    for (let i = 0; i < node.namedChildCount; i++) {
+      const child = node.namedChild(i);
+      if (!child || child.type !== 'identifier') continue;
+      const field = node.fieldNameForNamedChild(i);
+      const text = getNodeText(child, this.source);
+      if (field === 'namespace') {
+        openedNamespaces.push(text);
+      } else if (field === 'scoped') {
+        openedScopes.push(text);
+      }
+    }
+
+    if (openedNamespaces.length === 0 && openedScopes.length === 0) return;
+
+    const name = [...openedNamespaces, ...openedScopes.map((scope) => `scoped ${scope}`)].join(', ');
+    const parentId = this.currentContainerNodeId() ?? fileNodeId;
+    const openNode = this.createNode(parentId, 'import', `open ${name}`, node, {
+      qualifiedName: `${this.filePath}::open:${node.startPosition.row + 1}:${name}`,
+      signature: getNodeText(node, this.source).trim(),
+      isExported: false,
+    });
+
+    if (!openNode) return;
+    for (const namespaceName of openedNamespaces) {
+      this.unresolvedReferences.push({
+        fromNodeId: openNode.id,
+        referenceName: namespaceName,
+        referenceKind: 'references',
+        line: node.startPosition.row + 1,
+        column: node.startPosition.column,
+        filePath: this.filePath,
+        language: 'lean',
+        candidates: this.candidatesFor(namespaceName),
+      });
+    }
+    this.addOpenNamespaces(openedNamespaces);
+  }
+
+  private extractExport(fileNodeId: string, node: SyntaxNode): void {
+    const namespaceNode = this.namedChildrenWithField(node, 'namespace')[0];
+    if (!namespaceNode) return;
+
+    const namespaceName = getNodeText(namespaceNode, this.source);
+    const exportedNames = this.namedChildrenWithField(node, 'only')
+      .map((child) => getNodeText(child, this.source));
+    const name = exportedNames.length > 0
+      ? `${namespaceName} (${exportedNames.join(', ')})`
+      : namespaceName;
+    const parentId = this.currentContainerNodeId() ?? fileNodeId;
+    const exportNode = this.createNode(parentId, 'export', name, node, {
+      qualifiedName: `${this.filePath}::export:${node.startPosition.row + 1}:${name}`,
+      signature: getNodeText(node, this.source).trim(),
+      isExported: true,
+    });
+    if (!exportNode) return;
+
+    const targets = exportedNames.length > 0
+      ? exportedNames.map((exportedName) => `${namespaceName}.${exportedName}`)
+      : [namespaceName];
+    for (const target of targets) {
+      this.unresolvedReferences.push({
+        fromNodeId: exportNode.id,
+        referenceName: target,
+        referenceKind: 'exports',
+        line: node.startPosition.row + 1,
+        column: node.startPosition.column,
+        filePath: this.filePath,
+        language: 'lean',
+        candidates: this.candidatesFor(target),
+      });
+    }
+  }
+
+  private enterNamespace(fileNodeId: string, node: SyntaxNode): void {
+    const nameNode = getChildByField(node, 'name');
+    if (!nameNode) return;
+
+    const rawName = getNodeText(nameNode, this.source);
+    const parentNamespace = this.currentNamespaceQualifiedName();
+    const qualifiedName = parentNamespace ? `${parentNamespace}.${rawName}` : rawName;
+    const parentId = this.currentContainerNodeId() ?? fileNodeId;
+    const namespaceNode = this.createNode(parentId, 'namespace', rawName, node, {
+      qualifiedName,
+      signature: getNodeText(node, this.source).trim(),
+      isExported: true,
+    });
+    if (!namespaceNode) return;
+
+    this.scopeStack.push({
+      type: 'namespace',
+      nodeId: namespaceNode.id,
+      qualifiedName,
+      opens: [],
+    });
+  }
+
+  private enterSection(fileNodeId: string, node: SyntaxNode): void {
+    const nameNode = getChildByField(node, 'name');
+    const sectionName = nameNode
+      ? getNodeText(nameNode, this.source)
+      : `section@${node.startPosition.row + 1}`;
+    const parentId = this.currentContainerNodeId() ?? fileNodeId;
+    const sectionNode = this.createNode(parentId, 'module', sectionName, node, {
+      qualifiedName: `${this.filePath}::section:${sectionName}:${node.startPosition.row + 1}`,
+      signature: getNodeText(node, this.source).trim(),
+      isExported: false,
+    });
+    this.scopeStack.push({
+      type: 'section',
+      nodeId: sectionNode?.id ?? null,
+      name: sectionName,
+      opens: [],
+    });
+  }
+
+  private exitScope(node: SyntaxNode): void {
+    const frame = this.scopeStack.pop();
+    if (!frame) return;
+
+    if (frame.nodeId) {
+      const scopeNode = this.nodes.find((n) => n.id === frame.nodeId);
+      if (scopeNode) {
+        scopeNode.endLine = node.endPosition.row + 1;
+        scopeNode.endColumn = node.endPosition.column;
+      }
+    }
+  }
+
+  private closeOpenNamespaces(endLine: number): void {
+    for (const frame of this.scopeStack) {
+      if (!frame.nodeId) continue;
+      const node = this.nodes.find((n) => n.id === frame.nodeId);
+      if (node) node.endLine = Math.max(node.endLine, endLine);
+    }
+    this.scopeStack = [];
+  }
+
+  private extractDeclaration(fileNodeId: string, declaration: SyntaxNode): void {
+    const decl = this.findDeclarationPayload(declaration);
+    if (!decl) return;
+
+    const kind = this.declarationKind(decl);
+    if (!kind) return;
+
+    const nameNode = getChildByField(decl, 'name');
+    const rawName = nameNode
+      ? getNodeText(nameNode, this.source)
+      : decl.type === 'instance'
+        ? this.anonymousInstanceName(decl)
+        : null;
+    if (!rawName) return;
+
+    const simpleName = this.simpleName(rawName);
+    const parentNamespace = this.currentNamespaceQualifiedName();
+    const qualifiedName = parentNamespace ? `${parentNamespace}.${rawName}` : rawName;
+    const parentId = this.currentContainerNodeId() ?? fileNodeId;
+    const visibility = this.visibilityForDeclaration(declaration);
+
+    const declNode = this.createNode(parentId, kind, simpleName, decl, {
+      qualifiedName,
+      signature: getNodeText(decl, this.source).trim().slice(0, 300),
+      docstring: this.getLeanDocstring(declaration),
+      visibility,
+      isExported: visibility !== 'private',
+      decorators: this.extractAttributes(declaration),
+    });
+    if (!declNode) return;
+
+    this.extractInheritanceReferences(decl, declNode.id);
+
+    if (decl.type === 'structure') {
+      this.extractStructureMembers(declNode, decl);
+    } else if (decl.type === 'inductive') {
+      this.extractInductiveConstructors(declNode, decl);
+    }
+
+    this.extractReferencesFromDeclaration(decl, declNode.id, rawName);
+  }
+
+  private findDeclarationPayload(declaration: SyntaxNode): SyntaxNode | null {
+    for (let i = 0; i < declaration.namedChildCount; i++) {
+      const child = declaration.namedChild(i);
+      if (child && DECLARATION_TYPES.has(child.type)) return child;
+    }
+    return null;
+  }
+
+  private declarationKind(node: SyntaxNode): NodeKind | null {
+    switch (node.type) {
+      case 'def':
+      case 'theorem':
+      case 'opaque':
+        return 'function';
+      case 'abbrev':
+        return 'type_alias';
+      case 'axiom':
+      case 'constant':
+      case 'instance':
+        return 'constant';
+      case 'structure':
+        return this.leadingKeyword(node) === 'class' ? 'class' : 'struct';
+      case 'inductive':
+        return 'enum';
+      default:
+        return null;
+    }
+  }
+
+  private extractStructureMembers(parent: Node, node: SyntaxNode): void {
+    this.walkDescendants(node, (child) => {
+      if (child.type === 'ctor') {
+        this.createMember(parent, 'enum_member', child);
+        return false;
+      }
+      if (child.type === 'field') {
+        this.createMember(parent, 'field', child);
+        return false;
+      }
+      return true;
+    });
+  }
+
+  private extractInductiveConstructors(parent: Node, node: SyntaxNode): void {
+    this.walkDescendants(node, (child) => {
+      if (child.type !== 'ctor_alt') return true;
+      this.createMember(parent, 'enum_member', child);
+      return false;
+    });
+  }
+
+  private createMember(parent: Node, kind: NodeKind, node: SyntaxNode): Node | null {
+    const nameNode = getChildByField(node, 'name');
+    if (!nameNode) return null;
+    const rawName = getNodeText(nameNode, this.source);
+    const simpleName = this.simpleName(rawName);
+    return this.createNode(parent.id, kind, simpleName, node, {
+      qualifiedName: `${parent.qualifiedName}.${rawName}`,
+      signature: getNodeText(node, this.source).trim().slice(0, 300),
+      docstring: this.getLeanDocstring(node),
+      visibility: this.visibilityForDeclaration(node),
+      isExported: this.visibilityForDeclaration(node) !== 'private',
+    });
+  }
+
+  private extractReferencesFromDeclaration(declaration: SyntaxNode, fromNodeId: string, declarationName: string): void {
+    const locals = new Set<string>([declarationName, this.simpleName(declarationName)]);
+    this.collectLocalNames(declaration, locals);
+    this.collectDeclaredNames(declaration, locals);
+
+    const emitted = new Set<string>();
+
+    this.walkDescendants(declaration, (node) => {
+      if (node.type !== 'app') return true;
+      if (this.isInsideNodeType(node, 'attributes') || this.isInInheritancePosition(node)) return true;
+      const fn = getChildByField(node, 'fn');
+      if (!fn) return true;
+      const referenceName = this.identifierLikeText(fn);
+      if (!referenceName || locals.has(referenceName) || locals.has(this.simpleName(referenceName))) {
+        return true;
+      }
+      this.addReference(fromNodeId, referenceName, 'calls', fn, emitted);
+      return true;
+    });
+
+    this.walkDescendants(declaration, (node) => {
+      if (node.type !== 'identifier') return true;
+      const name = getNodeText(node, this.source);
+      if (!name || name === '_' || locals.has(name) || locals.has(this.simpleName(name))) {
+        return true;
+      }
+      if (
+        this.isIdentifierNamePosition(node) ||
+        this.isBinderName(node) ||
+        this.isAppFunction(node) ||
+        this.isInsideNodeType(node, 'attributes') ||
+        this.isInInheritancePosition(node)
+      ) {
+        return true;
+      }
+      this.addReference(fromNodeId, name, 'references', node, emitted);
+      return true;
+    });
+  }
+
+  private addReference(
+    fromNodeId: string,
+    referenceName: string,
+    referenceKind: 'calls' | 'references',
+    node: SyntaxNode,
+    emitted: Set<string>
+  ): void {
+    const key = `${referenceKind}:${referenceName}`;
+    if (emitted.has(key)) return;
+    emitted.add(key);
+    this.unresolvedReferences.push({
+      fromNodeId,
+      referenceName,
+      referenceKind,
+      line: node.startPosition.row + 1,
+      column: node.startPosition.column,
+      filePath: this.filePath,
+      language: 'lean',
+      candidates: this.candidatesFor(referenceName),
+    });
+  }
+
+  private extractInheritanceReferences(decl: SyntaxNode, fromNodeId: string): void {
+    if (decl.type !== 'structure') return;
+
+    const emitted = new Set<string>();
+    for (let i = 0; i < decl.namedChildCount; i++) {
+      const child = decl.namedChild(i);
+      if (!child) continue;
+      if (!this.isInheritanceChild(child, decl)) continue;
+
+      const referenceName = this.identifierLikeText(child);
+      if (!referenceName || emitted.has(referenceName)) continue;
+      emitted.add(referenceName);
+      this.unresolvedReferences.push({
+        fromNodeId,
+        referenceName,
+        referenceKind: 'extends',
+        line: child.startPosition.row + 1,
+        column: child.startPosition.column,
+        filePath: this.filePath,
+        language: 'lean',
+        candidates: this.candidatesFor(referenceName),
+      });
+    }
+  }
+
+  private collectLocalNames(node: SyntaxNode, out: Set<string>): void {
+    this.walkDescendants(node, (child) => {
+      if (!BINDER_NODE_TYPES.has(child.type)) return true;
+
+      for (let i = 0; i < child.namedChildCount; i++) {
+        const named = child.namedChild(i);
+        if (!named) continue;
+        const field = child.fieldNameForNamedChild(i);
+        if (field === 'name' || (child.type === 'binders' && named.type === 'identifier')) {
+          const text = getNodeText(named, this.source);
+          out.add(text);
+          out.add(this.simpleName(text));
+        }
+      }
+
+      return true;
+    });
+  }
+
+  private collectDeclaredNames(node: SyntaxNode, out: Set<string>): void {
+    this.walkDescendants(node, (child) => {
+      if (!DECL_NAME_NODE_TYPES.has(child.type)) return true;
+      const nameNode = getChildByField(child, 'name');
+      if (nameNode) {
+        const text = getNodeText(nameNode, this.source);
+        out.add(text);
+        out.add(this.simpleName(text));
+      }
+      return true;
+    });
+  }
+
+  private createNode(
+    parentId: string,
+    kind: NodeKind,
+    name: string,
+    syntaxNode: SyntaxNode,
+    extra: Partial<Node> = {}
+  ): Node | null {
+    if (!name) return null;
+    const qualifiedName = extra.qualifiedName ?? name;
+    const node: Node = {
+      id: generateNodeId(this.filePath, kind, qualifiedName, syntaxNode.startPosition.row + 1),
+      kind,
+      name,
+      qualifiedName,
+      filePath: this.filePath,
+      language: 'lean',
+      startLine: syntaxNode.startPosition.row + 1,
+      endLine: syntaxNode.endPosition.row + 1,
+      startColumn: syntaxNode.startPosition.column,
+      endColumn: syntaxNode.endPosition.column,
+      updatedAt: Date.now(),
+      ...extra,
+    };
+
+    this.nodes.push(node);
+    this.edges.push({
+      source: parentId,
+      target: node.id,
+      kind: 'contains',
+    });
+    return node;
+  }
+
+  private currentNamespaceQualifiedName(): string | null {
+    for (let i = this.scopeStack.length - 1; i >= 0; i--) {
+      const frame = this.scopeStack[i]!;
+      if (frame.type === 'namespace') return frame.qualifiedName;
+    }
+    return null;
+  }
+
+  private currentContainerNodeId(): string | null {
+    for (let i = this.scopeStack.length - 1; i >= 0; i--) {
+      const frame = this.scopeStack[i]!;
+      if (frame.nodeId) return frame.nodeId;
+    }
+    return null;
+  }
+
+  private visibilityForDeclaration(node: SyntaxNode): 'public' | 'private' | 'protected' | undefined {
+    const text = getNodeText(node, this.source);
+    if (/\b(?:private|local)\b/.test(text)) return 'private';
+    if (/\bprotected\b/.test(text)) return 'protected';
+    return 'public';
+  }
+
+  private leadingKeyword(node: SyntaxNode): string {
+    return getNodeText(node, this.source).trimStart().split(/\s+/, 1)[0] ?? node.type;
+  }
+
+  private simpleName(name: string): string {
+    const parts = name.split('.').filter(Boolean);
+    return parts[parts.length - 1] ?? name;
+  }
+
+  private anonymousInstanceName(node: SyntaxNode): string {
+    const typeNode = this.namedChildrenWithField(node, 'type')[0] ?? getChildByField(node, 'type');
+    const typeParts = typeNode
+      ? getNodeText(typeNode, this.source)
+          .split(/[^A-Za-z0-9_]+/)
+          .filter(Boolean)
+      : [];
+    return `inst${typeParts.join('') || 'anonymous'}@${node.startPosition.row + 1}`;
+  }
+
+  private identifierLikeText(node: SyntaxNode): string | null {
+    if (node.type === 'identifier') return getNodeText(node, this.source);
+    if (node.type === 'app') {
+      const fn = getChildByField(node, 'fn');
+      return fn ? this.identifierLikeText(fn) : null;
+    }
+    const name = getChildByField(node, 'name') ?? getChildByField(node, 'field');
+    return name && name.type === 'identifier' ? getNodeText(name, this.source) : null;
+  }
+
+  private extractAttributes(node: SyntaxNode): string[] | undefined {
+    const attributes = node.namedChildren.find((child) => child.type === 'attributes');
+    if (!attributes) return undefined;
+
+    const names: string[] = [];
+    for (let i = 0; i < attributes.namedChildCount; i++) {
+      const child = attributes.namedChild(i);
+      if (!child || child.type !== 'identifier') continue;
+      if (attributes.fieldNameForNamedChild(i) !== 'name') continue;
+      names.push(getNodeText(child, this.source));
+    }
+    return names.length > 0 ? names : undefined;
+  }
+
+  private isIdentifierNamePosition(node: SyntaxNode): boolean {
+    const parent = node.parent;
+    if (!parent || !DECL_NAME_NODE_TYPES.has(parent.type)) return false;
+    return this.fieldNameInParent(node) === 'name';
+  }
+
+  private isBinderName(node: SyntaxNode): boolean {
+    const parent = node.parent;
+    if (!parent) return false;
+    return BINDER_NODE_TYPES.has(parent.type) && (
+      this.fieldNameInParent(node) === 'name' ||
+      (parent.type === 'binders' && this.fieldNameInParent(node) === null)
+    );
+  }
+
+  private isAppFunction(node: SyntaxNode): boolean {
+    return node.parent?.type === 'app' && this.fieldNameInParent(node) === 'fn';
+  }
+
+  private isInsideNodeType(node: SyntaxNode, type: string): boolean {
+    let current: SyntaxNode | null = node.parent;
+    while (current) {
+      if (current.type === type) return true;
+      current = current.parent;
+    }
+    return false;
+  }
+
+  private isInInheritancePosition(node: SyntaxNode): boolean {
+    let current: SyntaxNode | null = node;
+    while (current?.parent) {
+      const parent: SyntaxNode = current.parent;
+      if (parent.type === 'structure') {
+        return this.isInheritanceChild(current, parent);
+      }
+      current = parent;
+    }
+    return false;
+  }
+
+  private isInheritanceChild(child: SyntaxNode, parent: SyntaxNode): boolean {
+    if (parent.type !== 'structure') return false;
+    if (child.type !== 'identifier' && child.type !== 'app') return false;
+    if (this.fieldNameInParent(child) === 'name') return false;
+
+    for (let i = 0; i < parent.namedChildCount; i++) {
+      const candidate = parent.namedChild(i);
+      if (!candidate) continue;
+      if (candidate.id === child.id) return true;
+      if (
+        candidate.type === 'field' ||
+        candidate.type === 'struct_field' ||
+        candidate.type === 'where_struct'
+      ) {
+        return false;
+      }
+    }
+    return false;
+  }
+
+  private fieldNameInParent(node: SyntaxNode): string | null {
+    const parent = node.parent;
+    if (!parent) return null;
+    for (let i = 0; i < parent.namedChildCount; i++) {
+      if (parent.namedChild(i)?.id === node.id) {
+        return parent.fieldNameForNamedChild(i);
+      }
+    }
+    return null;
+  }
+
+  private namedChildrenWithField(node: SyntaxNode, fieldName: string): SyntaxNode[] {
+    const children: SyntaxNode[] = [];
+    for (let i = 0; i < node.namedChildCount; i++) {
+      const child = node.namedChild(i);
+      if (child && node.fieldNameForNamedChild(i) === fieldName) {
+        children.push(child);
+      }
+    }
+    return children;
+  }
+
+  private addOpenNamespaces(namespaces: string[]): void {
+    if (namespaces.length === 0) return;
+    const frame = this.scopeStack[this.scopeStack.length - 1];
+    const target = frame ? frame.opens : this.moduleOpenNamespaces;
+    for (const namespaceName of namespaces) {
+      if (!target.includes(namespaceName)) target.push(namespaceName);
+    }
+  }
+
+  private currentOpenNamespaces(): string[] {
+    const namespaces: string[] = [...this.moduleOpenNamespaces];
+    for (const frame of this.scopeStack) {
+      namespaces.push(...frame.opens);
+    }
+    return namespaces;
+  }
+
+  private currentNamespacePrefixes(): string[] {
+    const qualifiedName = this.currentNamespaceQualifiedName();
+    if (!qualifiedName) return [];
+    const parts = qualifiedName.split('.').filter(Boolean);
+    const prefixes: string[] = [];
+    for (let i = parts.length; i >= 1; i--) {
+      prefixes.push(parts.slice(0, i).join('.'));
+    }
+    return prefixes;
+  }
+
+  private candidatesFor(referenceName: string): string[] | undefined {
+    const cleanName = referenceName.replace(/^_root_\./, '');
+    if (!cleanName || cleanName === '_') return undefined;
+
+    const candidates: string[] = [];
+    const add = (candidate: string) => {
+      if (candidate && !candidates.includes(candidate)) candidates.push(candidate);
+    };
+
+    if (cleanName.includes('.')) {
+      add(cleanName);
+      for (const namespaceName of this.currentNamespacePrefixes()) {
+        add(`${namespaceName}.${cleanName}`);
+      }
+      for (const namespaceName of this.currentOpenNamespaces()) {
+        add(`${namespaceName}.${cleanName}`);
+      }
+      return candidates.length > 0 ? candidates : undefined;
+    }
+
+    for (const namespaceName of this.currentNamespacePrefixes()) {
+      add(`${namespaceName}.${cleanName}`);
+    }
+    for (const namespaceName of this.currentOpenNamespaces()) {
+      add(`${namespaceName}.${cleanName}`);
+    }
+    for (const moduleName of this.importedModules) {
+      const parts = moduleName.split('.').filter(Boolean);
+      for (let i = parts.length; i >= 1; i--) {
+        add(`${parts.slice(0, i).join('.')}.${cleanName}`);
+      }
+    }
+    add(cleanName);
+
+    return candidates.length > 0 ? candidates : undefined;
+  }
+
+  private getLeanDocstring(node: SyntaxNode): string | undefined {
+    const comments: string[] = [];
+    let sibling = node.previousNamedSibling;
+    while (sibling && (sibling.type === 'doc_comment' || sibling.type === 'module_doc_comment')) {
+      comments.unshift(getNodeText(sibling, this.source));
+      sibling = sibling.previousNamedSibling;
+    }
+    if (comments.length === 0) return undefined;
+    const cleaned = comments
+      .map((comment) => comment
+        .replace(/^\/-!/, '')
+        .replace(/^\/--?/, '')
+        .replace(/-\/$/, '')
+        .replace(/^--!? ?/gm, '')
+        .replace(/^\s*\* ?/gm, '')
+        .trim())
+      .filter(Boolean)
+      .join('\n')
+      .trim();
+    return cleaned || undefined;
+  }
+
+  private walkDescendants(node: SyntaxNode, visit: (node: SyntaxNode) => boolean): void {
+    for (let i = 0; i < node.namedChildCount; i++) {
+      const child = node.namedChild(i);
+      if (!child) continue;
+      const shouldDescend = visit(child);
+      if (shouldDescend) this.walkDescendants(child, visit);
+    }
+  }
+}
diff --git a/src/extraction/tree-sitter.ts b/src/extraction/tree-sitter.ts
index f576839fa..466d888a9 100644
--- a/src/extraction/tree-sitter.ts
+++ b/src/extraction/tree-sitter.ts
@@ -24,6 +24,7 @@ import { SvelteExtractor } from './svelte-extractor';
 import { DfmExtractor } from './dfm-extractor';
 import { VueExtractor } from './vue-extractor';
 import { MyBatisExtractor } from './mybatis-extractor';
+import { LeanExtractor } from './lean-extractor';
 import {
   getAllFrameworkResolvers,
   getApplicableFrameworks,
@@ -3067,6 +3068,11 @@ export function extractFromSource(
     // Use custom extractor for Liquid
     const extractor = new LiquidExtractor(filePath, source);
     result = extractor.extract();
+  } else if (detectedLanguage === 'lean') {
+    // Lean namespaces are flat sibling commands in the grammar, so a custom
+    // extractor reconstructs namespace scope while still using tree-sitter.
+    const extractor = new LeanExtractor(filePath, source);
+    result = extractor.extract();
   } else if (detectedLanguage === 'xml') {
     // Custom extractor for MyBatis mapper XML. Non-mapper XML returns just a
     // file node so the watcher tracks it without emitting symbols.
diff --git a/src/extraction/wasm/tree-sitter-lean.wasm b/src/extraction/wasm/tree-sitter-lean.wasm
new file mode 100755
index 000000000..3647d04c6
Binary files /dev/null and b/src/extraction/wasm/tree-sitter-lean.wasm differ
diff --git a/src/resolution/import-resolver.ts b/src/resolution/import-resolver.ts
index bc493704d..dffd92bcf 100644
--- a/src/resolution/import-resolver.ts
+++ b/src/resolution/import-resolver.ts
@@ -28,6 +28,7 @@ const EXTENSION_RESOLUTION: Record<string, string[]> = {
   php: ['.php'],
   ruby: ['.rb'],
   objc: ['.h', '.m', '.mm'],
+  lean: ['.lean'],
 };
 
 /**
@@ -59,6 +60,10 @@ export function resolveImportPath(
   const aliased = resolveAliasedImport(importPath, projectRoot, language, context);
   if (aliased) return aliased;
 
+  if (language === 'lean') {
+    return resolveLeanModulePath(importPath, context);
+  }
+
   // C/C++ include directory search: when neither relative nor aliased
   // resolution found a match, search -I directories from
   // compile_commands.json or heuristic probing.
@@ -69,6 +74,22 @@ export function resolveImportPath(
   return null;
 }
 
+function resolveLeanModulePath(
+  moduleName: string,
+  context: ResolutionContext
+): string | null {
+  const modulePath = moduleName.replace(/\./g, '/') + '.lean';
+  if (context.fileExists(modulePath)) return modulePath;
+
+  const suffix = '/' + modulePath;
+  const matches = context
+    .getAllFiles()
+    .map((file) => file.replace(/\\/g, '/'))
+    .filter((file) => file.endsWith(suffix));
+
+  return matches.length === 1 ? matches[0]! : null;
+}
+
 /**
  * C and C++ standard library header names (without delimiters).
  * Used by isExternalImport to filter system includes from resolution.
@@ -987,6 +1008,22 @@ export function resolveViaImport(
   ref: UnresolvedRef,
   context: ResolutionContext
 ): ResolvedRef | null {
+  if (ref.language === 'lean' && ref.referenceKind === 'imports') {
+    const resolvedPath = resolveImportPath(ref.referenceName, ref.filePath, ref.language, context);
+    if (!resolvedPath) return null;
+    const basename = resolvedPath.split('/').pop()!;
+    const fileNode = context
+      .getNodesByName(basename)
+      .find((n) => n.kind === 'file' && n.filePath.replace(/\\/g, '/') === resolvedPath);
+    if (!fileNode) return null;
+    return {
+      original: ref,
+      targetNodeId: fileNode.id,
+      confidence: 0.9,
+      resolvedBy: 'import',
+    };
+  }
+
   // C/C++ #include references — resolve directly to the included file
   // (file→file edge), bypassing symbol lookup. The extractor emits these
   // with `referenceKind: 'imports'` and `referenceName: <include path>`
diff --git a/src/resolution/index.ts b/src/resolution/index.ts
index 5158e8301..e297bf303 100644
--- a/src/resolution/index.ts
+++ b/src/resolution/index.ts
@@ -22,6 +22,7 @@ import { detectFrameworks } from './frameworks';
 import { synthesizeCallbackEdges } from './callback-synthesizer';
 import { loadProjectAliases, type AliasMap } from './path-aliases';
 import { loadGoModule, type GoModule } from './go-module';
+import { resolveLeanLspBatch } from './lean-lsp-resolver';
 import { logDebug } from '../errors';
 import type { ReExport } from './types';
 import { LRUCache } from './lru-cache';
@@ -465,14 +466,16 @@ export class ReferenceResolver {
       column: ref.column,
       filePath: ref.filePath || this.getFilePathFromNodeId(ref.fromNodeId),
       language: ref.language || this.getLanguageFromNodeId(ref.fromNodeId),
+      candidates: ref.candidates,
     }));
 
+    const leanLspResolved = resolveLeanLspBatch(refs, this.context);
     const total = refs.length;
     let lastReportedPercent = -1;
 
     for (let i = 0; i < refs.length; i++) {
       const ref = refs[i]!; // Array index is guaranteed to be in bounds
-      const result = this.resolveOne(ref);
+      const result = leanLspResolved.get(i) ?? this.resolveOne(ref);
 
       if (result) {
         resolved.push(result);
@@ -589,6 +592,7 @@ export class ReferenceResolver {
     // from './auth'`) intentionally call a name that has no
     // declaration anywhere — only the renamed upstream symbol does.
     if (
+      ref.referenceKind !== 'imports' &&
       !this.hasAnyPossibleMatch(ref.referenceName) &&
       !this.matchesAnyImport(ref) &&
       !this.frameworks.some((f) => f.claimsReference?.(ref.referenceName))
diff --git a/src/resolution/lean-lsp-resolver.ts b/src/resolution/lean-lsp-resolver.ts
new file mode 100644
index 000000000..4affcdf6a
--- /dev/null
+++ b/src/resolution/lean-lsp-resolver.ts
@@ -0,0 +1,356 @@
+import * as fs from 'fs';
+import * as path from 'path';
+import { spawnSync } from 'child_process';
+import { fileURLToPath } from 'url';
+import { Node } from '../types';
+import { ResolutionContext, ResolvedRef, UnresolvedRef } from './types';
+
+interface LeanLspWorkerLocation {
+  index: number;
+  uri: string;
+  line: number;
+  column: number;
+}
+
+interface LeanLspWorkerOutput {
+  locations?: LeanLspWorkerLocation[];
+}
+
+const DEFAULT_LEAN_LSP_TIMEOUT_MS = 2_000;
+const DEFAULT_LEAN_LSP_REF_LIMIT = 100;
+
+function parsePositiveInt(value: string | undefined, fallback: number): number {
+  if (!value) return fallback;
+  const parsed = Number.parseInt(value, 10);
+  return Number.isFinite(parsed) && parsed > 0 ? parsed : fallback;
+}
+
+function commandExists(command: string): boolean {
+  const pathEnv = process.env.PATH ?? '';
+  const extensions = process.platform === 'win32'
+    ? (process.env.PATHEXT ?? '.EXE;.CMD;.BAT').split(';')
+    : [''];
+  for (const dir of pathEnv.split(path.delimiter)) {
+    if (!dir) continue;
+    for (const ext of extensions) {
+      try {
+        fs.accessSync(path.join(dir, command + ext), fs.constants.X_OK);
+        return true;
+      } catch {
+        // keep searching
+      }
+    }
+  }
+  return false;
+}
+
+function leanLspCommand(): string | null {
+  const override = process.env.CODEGRAPH_LEAN_LSP_COMMAND?.trim();
+  if (override) return override;
+  if (commandExists('lake')) return 'lake env lean --server';
+  if (commandExists('lean')) return 'lean --server';
+  return null;
+}
+
+function isLeanSemanticsEnabled(): boolean {
+  const mode = (process.env.CODEGRAPH_LEAN_SEMANTICS ?? 'auto').trim().toLowerCase();
+  return mode !== 'off' && mode !== 'false' && mode !== '0';
+}
+
+function uriToProjectPath(uri: string, projectRoot: string): string | null {
+  try {
+    const absolutePath = fileURLToPath(uri);
+    const relativePath = path.relative(projectRoot, absolutePath).replace(/\\/g, '/');
+    if (!relativePath || relativePath.startsWith('..') || path.isAbsolute(relativePath)) {
+      return null;
+    }
+    return relativePath;
+  } catch {
+    return null;
+  }
+}
+
+function containsPosition(node: Node, line: number, column: number): boolean {
+  if (line < node.startLine || line > node.endLine) return false;
+  if (line === node.startLine && column < node.startColumn) return false;
+  if (line === node.endLine && column > node.endColumn) return false;
+  return true;
+}
+
+function findSmallestCoveringNode(
+  filePath: string,
+  line: number,
+  column: number,
+  context: ResolutionContext
+): Node | null {
+  const candidates = context
+    .getNodesInFile(filePath)
+    .filter((node) => node.kind !== 'file' && containsPosition(node, line, column));
+  if (candidates.length === 0) return null;
+
+  candidates.sort((a, b) => {
+    const aSpan = (a.endLine - a.startLine) * 10_000 + (a.endColumn - a.startColumn);
+    const bSpan = (b.endLine - b.startLine) * 10_000 + (b.endColumn - b.startColumn);
+    if (aSpan !== bSpan) return aSpan - bSpan;
+    return b.startLine - a.startLine;
+  });
+  return candidates[0] ?? null;
+}
+
+/**
+ * Resolve Lean references through `textDocument/definition` when a Lean LSP is
+ * available. This is deliberately best-effort: any missing command, timeout,
+ * malformed response, or project-external location returns an empty map and the
+ * static resolver continues unchanged.
+ */
+export function resolveLeanLspBatch(
+  refs: UnresolvedRef[],
+  context: ResolutionContext
+): Map<number, ResolvedRef> {
+  const resolved = new Map<number, ResolvedRef>();
+  if (!isLeanSemanticsEnabled()) return resolved;
+
+  const command = leanLspCommand();
+  if (!command) return resolved;
+
+  const refLimit = parsePositiveInt(process.env.CODEGRAPH_LEAN_LSP_REF_LIMIT, DEFAULT_LEAN_LSP_REF_LIMIT);
+  const timeoutMs = parsePositiveInt(process.env.CODEGRAPH_LEAN_LSP_TIMEOUT_MS, DEFAULT_LEAN_LSP_TIMEOUT_MS);
+  const leanRefs = refs
+    .map((ref, index) => ({ ref, index }))
+    .filter(({ ref }) => ref.language === 'lean' && ref.referenceKind !== 'imports')
+    .slice(0, refLimit);
+  if (leanRefs.length === 0) return resolved;
+
+  const workerInput = {
+    command,
+    projectRoot: context.getProjectRoot(),
+    timeoutMs,
+    refs: leanRefs.map(({ ref, index }) => ({
+      index,
+      filePath: ref.filePath,
+      line: ref.line,
+      column: ref.column,
+    })),
+  };
+
+  const totalTimeoutMs = Math.max(timeoutMs, Math.min(10_000, timeoutMs * 2 + leanRefs.length * 50));
+  const result = spawnSync(process.execPath, ['-e', LEAN_LSP_WORKER_SOURCE], {
+    input: JSON.stringify(workerInput),
+    encoding: 'utf-8',
+    timeout: totalTimeoutMs,
+    maxBuffer: 1024 * 1024,
+    env: process.env,
+  });
+
+  if (result.error || result.status !== 0 || !result.stdout.trim()) return resolved;
+
+  let parsed: LeanLspWorkerOutput;
+  try {
+    parsed = JSON.parse(result.stdout) as LeanLspWorkerOutput;
+  } catch {
+    return resolved;
+  }
+
+  for (const location of parsed.locations ?? []) {
+    const ref = refs[location.index];
+    if (!ref) continue;
+
+    const targetPath = uriToProjectPath(location.uri, context.getProjectRoot());
+    if (!targetPath) continue;
+
+    const targetNode = findSmallestCoveringNode(
+      targetPath,
+      location.line,
+      location.column,
+      context
+    );
+    if (!targetNode) continue;
+
+    resolved.set(location.index, {
+      original: ref,
+      targetNodeId: targetNode.id,
+      confidence: 0.99,
+      resolvedBy: 'lean-lsp',
+    });
+  }
+
+  return resolved;
+}
+
+const LEAN_LSP_WORKER_SOURCE = String.raw`
+const fs = require('fs');
+const path = require('path');
+const { spawn } = require('child_process');
+const { pathToFileURL } = require('url');
+
+function readStdin() {
+  return new Promise((resolve) => {
+    let data = '';
+    process.stdin.setEncoding('utf8');
+    process.stdin.on('data', (chunk) => { data += chunk; });
+    process.stdin.on('end', () => resolve(data));
+  });
+}
+
+function writeOutput(locations) {
+  process.stdout.write(JSON.stringify({ locations }));
+}
+
+function makeRpc(child) {
+  let nextId = 1;
+  let buffer = Buffer.alloc(0);
+  const pending = new Map();
+
+  function sendMessage(message) {
+    const body = Buffer.from(JSON.stringify(message), 'utf8');
+    child.stdin.write(Buffer.from('Content-Length: ' + body.length + '\r\n\r\n', 'ascii'));
+    child.stdin.write(body);
+  }
+
+  function handleMessage(message) {
+    if (message && Object.prototype.hasOwnProperty.call(message, 'id')) {
+      const entry = pending.get(message.id);
+      if (entry) {
+        clearTimeout(entry.timer);
+        pending.delete(message.id);
+        entry.resolve(message);
+      }
+    }
+  }
+
+  child.stdout.on('data', (chunk) => {
+    buffer = Buffer.concat([buffer, chunk]);
+    while (true) {
+      const headerEnd = buffer.indexOf('\r\n\r\n');
+      if (headerEnd < 0) return;
+      const header = buffer.slice(0, headerEnd).toString('ascii');
+      const match = header.match(/Content-Length:\s*(\d+)/i);
+      if (!match) {
+        buffer = buffer.slice(headerEnd + 4);
+        continue;
+      }
+      const length = Number.parseInt(match[1], 10);
+      const messageStart = headerEnd + 4;
+      const messageEnd = messageStart + length;
+      if (buffer.length < messageEnd) return;
+      const body = buffer.slice(messageStart, messageEnd).toString('utf8');
+      buffer = buffer.slice(messageEnd);
+      try {
+        handleMessage(JSON.parse(body));
+      } catch {
+        // Ignore malformed server output.
+      }
+    }
+  });
+
+  function request(method, params, timeoutMs) {
+    const id = nextId++;
+    return new Promise((resolve) => {
+      const timer = setTimeout(() => {
+        pending.delete(id);
+        resolve(null);
+      }, timeoutMs);
+      pending.set(id, { resolve, timer });
+      sendMessage({ jsonrpc: '2.0', id, method, params });
+    });
+  }
+
+  function notify(method, params) {
+    sendMessage({ jsonrpc: '2.0', method, params });
+  }
+
+  return { request, notify };
+}
+
+function lspUri(projectRoot, filePath) {
+  return pathToFileURL(path.join(projectRoot, filePath)).href;
+}
+
+function locationFromResult(index, result) {
+  const value = Array.isArray(result) ? result[0] : result;
+  if (!value) return null;
+  const uri = value.uri || value.targetUri;
+  const range = value.range || value.targetSelectionRange || value.targetRange;
+  if (!uri || !range || !range.start) return null;
+  return {
+    index,
+    uri,
+    line: (range.start.line ?? 0) + 1,
+    column: range.start.character ?? 0,
+  };
+}
+
+(async () => {
+  let input;
+  try {
+    input = JSON.parse(await readStdin());
+  } catch {
+    writeOutput([]);
+    return;
+  }
+
+  const timeoutMs = input.timeoutMs || 2000;
+  const child = spawn(input.command, {
+    cwd: input.projectRoot,
+    shell: true,
+    stdio: ['pipe', 'pipe', 'ignore'],
+  });
+
+  let spawnFailed = false;
+  child.on('error', () => { spawnFailed = true; });
+
+  const rpc = makeRpc(child);
+  const rootUri = pathToFileURL(input.projectRoot.endsWith(path.sep) ? input.projectRoot : input.projectRoot + path.sep).href;
+  const initialized = await rpc.request('initialize', {
+    processId: process.pid,
+    rootUri,
+    capabilities: {},
+    workspaceFolders: null,
+  }, timeoutMs);
+
+  if (spawnFailed || !initialized) {
+    child.kill();
+    writeOutput([]);
+    return;
+  }
+
+  rpc.notify('initialized', {});
+
+  const opened = new Set();
+  const locations = [];
+  for (const ref of input.refs || []) {
+    if (!opened.has(ref.filePath)) {
+      opened.add(ref.filePath);
+      let text = '';
+      try {
+        text = fs.readFileSync(path.join(input.projectRoot, ref.filePath), 'utf8');
+      } catch {
+        continue;
+      }
+      rpc.notify('textDocument/didOpen', {
+        textDocument: {
+          uri: lspUri(input.projectRoot, ref.filePath),
+          languageId: 'lean4',
+          version: 1,
+          text,
+        },
+      });
+    }
+
+    const response = await rpc.request('textDocument/definition', {
+      textDocument: { uri: lspUri(input.projectRoot, ref.filePath) },
+      position: {
+        line: Math.max(0, (ref.line || 1) - 1),
+        character: Math.max(0, ref.column || 0),
+      },
+    }, timeoutMs);
+    const location = response ? locationFromResult(ref.index, response.result) : null;
+    if (location) locations.push(location);
+  }
+
+  child.kill();
+  writeOutput(locations);
+})().catch(() => {
+  writeOutput([]);
+});
+`;
diff --git a/src/resolution/name-matcher.ts b/src/resolution/name-matcher.ts
index 03fa79242..f9ec461b1 100644
--- a/src/resolution/name-matcher.ts
+++ b/src/resolution/name-matcher.ts
@@ -146,6 +146,50 @@ export function matchByQualifiedName(
   return null;
 }
 
+/**
+ * Try extractor-provided qualified-name candidates before broad name matching.
+ * Languages such as Lean can cheaply enumerate lexical candidates from the
+ * current namespace plus active `open` / `import` declarations. Those are more
+ * precise than path-proximity when several files define the same simple name.
+ */
+export function matchByCandidates(
+  ref: UnresolvedRef,
+  context: ResolutionContext
+): ResolvedRef | null {
+  if (!ref.candidates || ref.candidates.length === 0) return null;
+
+  const seen = new Set<string>();
+  for (const candidateName of ref.candidates) {
+    if (seen.has(candidateName)) continue;
+    seen.add(candidateName);
+
+    const candidates = context
+      .getNodesByQualifiedName(candidateName)
+      .filter((node) => node.language === ref.language || ref.language === 'unknown');
+    if (candidates.length === 1) {
+      return {
+        original: ref,
+        targetNodeId: candidates[0]!.id,
+        confidence: 0.97,
+        resolvedBy: 'qualified-name',
+      };
+    }
+    if (candidates.length > 1) {
+      const bestMatch = findBestMatch(ref, candidates, context);
+      if (bestMatch) {
+        return {
+          original: ref,
+          targetNodeId: bestMatch.id,
+          confidence: 0.9,
+          resolvedBy: 'qualified-name',
+        };
+      }
+    }
+  }
+
+  return null;
+}
+
 function resolveMethodOnType(
   typeName: string,
   methodName: string,
@@ -692,19 +736,23 @@ export function matchReference(
   result = matchByFilePath(ref, context);
   if (result) return result;
 
-  // 1. Qualified name match (highest confidence)
+  // 1. Extractor-provided qualified-name candidates
+  result = matchByCandidates(ref, context);
+  if (result) return result;
+
+  // 2. Qualified name match (highest confidence)
   result = matchByQualifiedName(ref, context);
   if (result) return result;
 
-  // 2. Method call pattern
+  // 3. Method call pattern
   result = matchMethodCall(ref, context);
   if (result) return result;
 
-  // 3. Exact name match
+  // 4. Exact name match
   result = matchByExactName(ref, context);
   if (result) return result;
 
-  // 4. Fuzzy match (lowest confidence)
+  // 5. Fuzzy match (lowest confidence)
   result = matchFuzzy(ref, context);
   if (result) return result;
 
diff --git a/src/resolution/types.ts b/src/resolution/types.ts
index e0ef5efa3..05c2ede39 100644
--- a/src/resolution/types.ts
+++ b/src/resolution/types.ts
@@ -39,7 +39,7 @@ export interface ResolvedRef {
   /** Confidence score (0-1) */
   confidence: number;
   /** How it was resolved */
-  resolvedBy: 'exact-match' | 'import' | 'qualified-name' | 'framework' | 'fuzzy' | 'instance-method' | 'file-path';
+  resolvedBy: 'exact-match' | 'import' | 'qualified-name' | 'framework' | 'fuzzy' | 'instance-method' | 'file-path' | 'lean-lsp';
 }
 
 /**
diff --git a/src/types.ts b/src/types.ts
index 0cfaf0bba..15f5a1cf4 100644
--- a/src/types.ts
+++ b/src/types.ts
@@ -88,6 +88,7 @@ export const LANGUAGES = [
   'lua',
   'luau',
   'objc',
+  'lean',
   'yaml',
   'twig',
   'xml',