diff --git a/src/renderer/src/lib/monaco-languages/register-lean.ts b/src/renderer/src/lib/monaco-languages/register-lean.ts
new file mode 100644
index 00000000000..b00ddab2faf
--- /dev/null
+++ b/src/renderer/src/lib/monaco-languages/register-lean.ts
@@ -0,0 +1,23 @@
+import type * as Monaco from 'monaco-editor'
+import type { LanguageRegistration } from 'shiki/core'
+import { registerTextMateLanguage } from './textmate-language-registration'
+
+export async function loadLeanTextMateGrammar(): Promise<LanguageRegistration> {
+  const { default: grammars } = await import('shiki/langs/lean.mjs')
+  const grammar = grammars[0]
+  const repository = Object.assign({}, grammar.repository)
+  // TextMate drops this rule when its only pattern includes the unbundled Lean Markdown grammar.
+  repository.dashComment = { ...repository.dashComment, patterns: [] }
+  return { ...grammar, repository }
+}
+
+export function registerLeanLanguage(monaco: typeof Monaco): void {
+  registerTextMateLanguage(monaco, {
+    language: {
+      id: 'lean',
+      extensions: ['.lean'],
+      aliases: ['Lean 4', 'Lean', 'lean', 'lean4']
+    },
+    loadGrammar: loadLeanTextMateGrammar
+  })
+}
diff --git a/src/renderer/src/lib/monaco-languages/textmate-token-provider.test.ts b/src/renderer/src/lib/monaco-languages/textmate-token-provider.test.ts
index bd2f3e01198..37e09729238 100644
--- a/src/renderer/src/lib/monaco-languages/textmate-token-provider.test.ts
+++ b/src/renderer/src/lib/monaco-languages/textmate-token-provider.test.ts
@@ -1,5 +1,6 @@
 import { describe, expect, it, vi } from 'vitest'
 import { loadNodeOniguruma } from '../syntax-highlighting/oniguruma-test-harness'
+import { loadLeanTextMateGrammar } from './register-lean'
 import { loadNimTextMateGrammar } from './register-nim'
 import { loadTypstTextMateGrammar } from './register-typst'
 import { createTextMateTokensProvider } from './textmate-token-provider'
@@ -7,6 +8,33 @@ import { createTextMateTokensProvider } from './textmate-token-provider'
 vi.mock('../syntax-highlighting/oniguruma', () => ({ loadOniguruma: loadNodeOniguruma }))
 
 describe('createTextMateTokensProvider', () => {
+  it('tokenizes Lean definitions, proof keywords, Unicode binders, strings, and comments', async () => {
+    const provider = await createTextMateTokensProvider({ loadGrammar: loadLeanTextMateGrammar })
+    const scopesOf = (line: string) =>
+      provider.tokenize(line, provider.getInitialState()).tokens.map((token) => token.scopes)
+
+    expect(scopesOf('theorem identity (p : Prop) : p → p := by')).toEqual(
+      expect.arrayContaining(['keyword.other.definitioncommand.lean4', 'storage.type.lean4'])
+    )
+    expect(scopesOf('  show p from h')).toContain('keyword.other.lean4')
+    expect(scopesOf('#check ∀ (α : Type), α → α')).toContain('storage.type.lean4')
+    expect(scopesOf('#eval "hello"')).toContain('string.quoted.double.lean4')
+    expect(scopesOf('-- proof note')).toContain('comment.line.double-dash.lean4')
+  })
+
+  it('carries nested Lean block comments across lines and resumes code after both closers', async () => {
+    const provider = await createTextMateTokensProvider({ loadGrammar: loadLeanTextMateGrammar })
+    let state = provider.tokenize('/- outer /- inner', provider.getInitialState()).endState
+    state = provider.tokenize('-/ still outer', state).endState
+    const hidden = provider.tokenize('theorem hidden : True := by trivial', state)
+    expect(hidden.tokens.map((token) => token.scopes)).toEqual(['comment.block.lean4'])
+    const closed = provider.tokenize('-/', hidden.endState)
+    const line = 'def answer : Nat := 42'
+    const after = provider.tokenize(line, closed.endState)
+    expect(after.tokens).toEqual(provider.tokenize(line, provider.getInitialState()).tokens)
+    expect(after.tokens.length).toBeGreaterThan(1)
+  })
+
   it('tokenizes Nim with the vendored TextMate grammar', async () => {
     const provider = await createTextMateTokensProvider({ loadGrammar: loadNimTextMateGrammar })
 
@@ -114,6 +142,7 @@ describe('createTextMateTokensProvider', () => {
   })
 
   it.each([
+    ['Lean', loadLeanTextMateGrammar, '/-'.repeat(40000), 'def value : Nat := 42'],
     ['Nim', loadNimTextMateGrammar, 'abcdefghij'.repeat(8000), 'proc greet() = discard'],
     ['Typst', loadTypstTextMateGrammar, '#let x = 12pt; *b* $x^2$ '.repeat(2000), '#let y = 2']
   ])(
diff --git a/src/renderer/src/lib/monaco-setup.ts b/src/renderer/src/lib/monaco-setup.ts
index be9b001adf4..49cad5673e0 100644
--- a/src/renderer/src/lib/monaco-setup.ts
+++ b/src/renderer/src/lib/monaco-setup.ts
@@ -10,6 +10,7 @@ import htmlWorker from 'monaco-editor/esm/vs/language/html/html.worker?worker'
 import tsWorker from 'monaco-editor/esm/vs/language/typescript/ts.worker?worker'
 import { registerAstroLanguage } from './monaco-languages/register-astro'
 import { registerJsonlLanguage } from './monaco-languages/register-jsonl'
+import { registerLeanLanguage } from './monaco-languages/register-lean'
 import { registerNimLanguage } from './monaco-languages/register-nim'
 import { registerQuartoLanguage } from './monaco-languages/register-quarto'
 import { registerShellMarkdownAliases } from './monaco-languages/register-shell-markdown-aliases'
@@ -84,6 +85,7 @@ runMonacoSetupSteps([
   ['Svelte language registration', () => registerSvelteLanguage(monaco)],
   ['Astro language registration', () => registerAstroLanguage(monaco)],
   ['Nim language registration', () => registerNimLanguage(monaco)],
+  ['Lean language registration', () => registerLeanLanguage(monaco)],
   ['Typst language registration', () => registerTypstLanguage(monaco)],
   ['JSONL language registration', () => registerJsonlLanguage(monaco)],
   ['Quarto language registration', () => registerQuartoLanguage(monaco)],
diff --git a/src/shared/editor-language/editor-language-detect.test.ts b/src/shared/editor-language/editor-language-detect.test.ts
index 7100a17b23c..d3c47efb29e 100644
--- a/src/shared/editor-language/editor-language-detect.test.ts
+++ b/src/shared/editor-language/editor-language-detect.test.ts
@@ -20,6 +20,23 @@ describe('detectLanguage', () => {
     expect(detectLanguage('packages/app.nimble')).toBe('nim')
   })
 
+  it.each([
+    'Main.lean',
+    'lakefile.lean',
+    'C:\\proofs\\MAIN.LEAN',
+    '\\\\server\\share\\Main.lean',
+    '/home/user/folder workspace/Proof.LeAn'
+  ])('maps Lean source %s to the lean language id', (filePath) => {
+    expect(detectLanguage(filePath)).toBe('lean')
+  })
+
+  it.each(['Main.lean.bak', 'Main.leanx', 'proofs.lean/README', 'proofs.lean\\README'])(
+    'keeps non-Lean file %s on plaintext',
+    (filePath) => {
+      expect(detectLanguage(filePath)).toBe('plaintext')
+    }
+  )
+
   it.each([
     'documents/report.typ',
     'C:\\documents\\REPORT.TYP',
diff --git a/src/shared/editor-language/editor-language-detect.ts b/src/shared/editor-language/editor-language-detect.ts
index a58c0e8e5c7..d7365669e35 100644
--- a/src/shared/editor-language/editor-language-detect.ts
+++ b/src/shared/editor-language/editor-language-detect.ts
@@ -112,6 +112,7 @@ const EXT_TO_LANGUAGE: Record<string, string> = {
   '.nim': 'nim',
   '.nims': 'nim',
   '.nimble': 'nim',
+  '.lean': 'lean',
   '.typ': 'typst',
   '.tf': 'hcl',
   '.hcl': 'hcl',
diff --git a/tests/e2e/editor-lean-highlighting.spec.ts b/tests/e2e/editor-lean-highlighting.spec.ts
new file mode 100644
index 00000000000..7464cc69dd1
--- /dev/null
+++ b/tests/e2e/editor-lean-highlighting.spec.ts
@@ -0,0 +1,153 @@
+import { writeFileSync } from 'node:fs'
+import path from 'node:path'
+import type { Locator } from '@stablyai/playwright-test'
+import { test, expect } from './helpers/orca-app'
+import {
+  cleanupGoldenWorktree,
+  createGoldenWorktree,
+  openGoldenSourceControl
+} from './helpers/golden-source-control'
+import { waitForSessionReady } from './helpers/store'
+
+const source = [
+  '-- proof note',
+  'theorem identity (p : Prop) : p → p := by',
+  '  intro h',
+  '  exact h',
+  '#check ∀ (α : Type), α → α',
+  '#eval "hello"',
+  '/- outer /- inner',
+  '-/ still outer',
+  'theorem hidden : True := by trivial',
+  '-/',
+  'def answer : Nat := 42',
+  ''
+].join('\n')
+
+async function paintedTokens(editor: Locator) {
+  return editor.locator('.view-lines:not(.line-delete)').evaluate((lines) =>
+    [...lines.querySelectorAll('.view-line')].map((line) => ({
+      text: (line.textContent ?? '').replaceAll('\u00a0', ' '),
+      tokens: [...line.querySelectorAll('span[class*="mtk"]')].map((token) => ({
+        text: (token.textContent ?? '').replaceAll('\u00a0', ' '),
+        className: token.className,
+        color: getComputedStyle(token).color
+      }))
+    }))
+  )
+}
+
+async function expectHighlighted(editor: Locator): Promise<void> {
+  await expect(editor).toBeVisible()
+  await expect(editor.locator('.view-lines:not(.line-delete)')).toContainText('-- proof note')
+  await expect
+    .poll(
+      async () => {
+        const lines = await paintedTokens(editor)
+        const color = (lineText: string, text: string) =>
+          lines
+            .find((line) => line.text === lineText)
+            ?.tokens.find((token) => token.text.includes(text))?.color
+        const keyword = color('theorem identity (p : Prop) : p → p := by', 'theorem')
+        const type = color('theorem identity (p : Prop) : p → p := by', 'Prop')
+        const unicode = color('#check ∀ (α : Type), α → α', '∀')
+        const comment = color('-- proof note', 'proof note')
+        const string = color('#eval "hello"', 'hello')
+        const hidden = color('theorem hidden : True := by trivial', 'theorem')
+        const resumed = color('def answer : Nat := 42', 'def')
+        return (
+          [keyword, type, unicode, comment, string, hidden, resumed].every(Boolean) &&
+          new Set([keyword, type, comment, string]).size >= 4 &&
+          hidden === comment &&
+          resumed === keyword
+        )
+      },
+      { timeout: 25_000 }
+    )
+    .toBe(true)
+}
+
+test('renders lean source and source-control diffs in both themes', async ({
+  orcaPage,
+  electronApp,
+  testRepoPath,
+  registerPostElectronShutdownCleanup
+}, testInfo) => {
+  const fixture = createGoldenWorktree(testRepoPath, 'lean-highlighting')
+  registerPostElectronShutdownCleanup(async () => cleanupGoldenWorktree(testRepoPath, fixture))
+  writeFileSync(path.join(fixture.worktreePath, 'Main.lean'), source)
+  await waitForSessionReady(orcaPage)
+  await openGoldenSourceControl(orcaPage, testRepoPath, fixture)
+  const identity = await electronApp.evaluate(({ BrowserWindow }) => ({
+    cwd: process.cwd(),
+    windows: BrowserWindow.getAllWindows().map((window) => ({
+      visible: window.isVisible(),
+      focused: window.isFocused()
+    }))
+  }))
+  expect(identity.cwd).toBe(process.cwd())
+  expect(identity.windows.length).toBeGreaterThan(0)
+  expect(identity.windows.every((window) => !window.visible && !window.focused)).toBe(true)
+  await testInfo.attach('hidden-instance-identity', {
+    body: JSON.stringify(identity, null, 2),
+    contentType: 'application/json'
+  })
+
+  for (const filename of ['Main.lean']) {
+    await orcaPage.evaluate(() => window.__store?.getState().showRightSidebarFiles())
+    await orcaPage
+      .locator('button[data-explorer-draggable="true"]')
+      .filter({ has: orcaPage.getByText(filename, { exact: true }) })
+      .click()
+    await expect
+      .poll(() => orcaPage.evaluate(() => window.__monacoEditorE2E?.filePath))
+      .toBe(path.join(fixture.worktreePath, filename))
+    await expect
+      .poll(() => orcaPage.evaluate(() => window.__monacoEditorE2E?.snapshot().valueLength))
+      .toBe(source.length)
+
+    for (const theme of ['light', 'dark'] as const) {
+      await orcaPage.evaluate(
+        (theme) => window.__store?.getState().updateSettings({ theme }),
+        theme
+      )
+      const editor = orcaPage
+        .locator(theme === 'light' ? '.monaco-editor.vs' : '.monaco-editor.vs-dark')
+        .first()
+      await expectHighlighted(editor)
+      await testInfo.attach(`${filename}-source-${theme}-tokens`, {
+        body: JSON.stringify(await paintedTokens(editor), null, 2),
+        contentType: 'application/json'
+      })
+      await orcaPage.screenshot({ path: testInfo.outputPath(`${filename}-source-${theme}.png`) })
+    }
+
+    await orcaPage.getByRole('button', { name: /Source Control/ }).click()
+    await orcaPage
+      .locator('[data-testid="source-control-entry"]')
+      .filter({ hasText: filename })
+      .click()
+    for (const theme of ['light', 'dark'] as const) {
+      await orcaPage.evaluate(
+        (theme) => window.__store?.getState().updateSettings({ theme }),
+        theme
+      )
+      const editor = orcaPage.locator(
+        theme === 'light'
+          ? '.modified-in-monaco-diff-editor.vs'
+          : '.modified-in-monaco-diff-editor.vs-dark'
+      )
+      await expectHighlighted(editor)
+      await testInfo.attach(`${filename}-diff-${theme}-tokens`, {
+        body: JSON.stringify(await paintedTokens(editor), null, 2),
+        contentType: 'application/json'
+      })
+      await orcaPage.screenshot({ path: testInfo.outputPath(`${filename}-diff-${theme}.png`) })
+    }
+  }
+  expect(
+    await electronApp.evaluate(({ BrowserWindow }) =>
+      BrowserWindow.getAllWindows().every((window) => !window.isVisible() && !window.isFocused())
+    )
+  ).toBe(true)
+})