From a6cdc6a66d5b7b66b4b2868dfa9d3ce4a2db63ca Mon Sep 17 00:00:00 2001
From: Francisco Giordano <fg@frang.io>
Date: Tue, 2 Jun 2026 14:19:29 -0300
Subject: [PATCH] Add Lean (#8737)

Fixes
https://github.com/compiler-explorer/compiler-explorer/issues/5634.

Adds the Lean 4 language and compiler.

> Lean is an open-source programming language and proof assistant that
enables correct, maintainable, and formally verified code

Since it was first requested in
https://github.com/compiler-explorer/compiler-explorer/issues/5634, it
has become increasingly relevant due to interest in AI-assisted theorem
proving, formalized mathematics, and verified software.

---

Lean compiles in two steps: first to C source code using the `lean`
executable, and then to assembly using the `leanc` compiler distributed
with Lean (I believe it's Clang).

The PR also includes a pane to visualize the emitted C source code that
was modelled after the panes for Rust and Haskell IRs and after the C
preprocessor pane for clang-format integration. Lean outputs mostly
unindented C code, so I enabled the formatter by default.

See companion infrastructure PR at
https://github.com/compiler-explorer/infra/pull/2130.



<img width="3024" height="1720" alt="image"
src="https://github.com/user-attachments/assets/5e7a1e91-e748-4599-8190-d3cb09fca503"
/>

---------

Co-authored-by: Matt Godbolt <matt@godbolt.org>
---
 .github/labeler.yml                         |   7 +
 etc/config/lean.amazon.properties           |  12 +
 etc/config/lean.defaults.properties         |   7 +
 examples/lean/default.lean                  |   4 +
 lib/base-compiler.ts                        |  29 ++
 lib/compilers/_all.ts                       |   1 +
 lib/compilers/lean.ts                       | 167 ++++++++++
 lib/languages.ts                            |  12 +
 public/logos/lean.png                       | Bin 0 -> 6202 bytes
 static/components.interfaces.ts             |  12 +
 static/components.ts                        |  34 ++
 static/event-map.ts                         |   4 +
 static/hub.ts                               |   7 +
 static/modes/_all.ts                        |   1 +
 static/modes/lean-mode.ts                   | 347 ++++++++++++++++++++
 static/panes/compiler.ts                    |  57 ++++
 static/panes/diff.interfaces.ts             |   1 +
 static/panes/diff.ts                        |   8 +
 static/panes/leanc-view.interfaces.ts       |  31 ++
 static/panes/leanc-view.ts                  | 151 +++++++++
 types/compilation/compilation.interfaces.ts |   3 +
 types/compilation/lean-c.interfaces.ts      |  27 ++
 types/compiler.interfaces.ts                |   1 +
 types/languages.interfaces.ts               |   1 +
 views/templates/panes/compiler.pug          |   1 +
 views/templates/panes/leanc.pug             |  10 +
 views/templates/templates.pug               |   2 +
 27 files changed, 937 insertions(+)
 create mode 100644 etc/config/lean.amazon.properties
 create mode 100644 etc/config/lean.defaults.properties
 create mode 100644 examples/lean/default.lean
 create mode 100644 lib/compilers/lean.ts
 create mode 100644 public/logos/lean.png
 create mode 100644 static/modes/lean-mode.ts
 create mode 100644 static/panes/leanc-view.interfaces.ts
 create mode 100644 static/panes/leanc-view.ts
 create mode 100644 types/compilation/lean-c.interfaces.ts
 create mode 100644 views/templates/panes/leanc.pug

diff --git a/.github/labeler.yml b/.github/labeler.yml
index 3d3936f0d..e84ddea93 100644
--- a/.github/labeler.yml
+++ b/.github/labeler.yml
@@ -246,6 +246,13 @@
           - 'lib/compilers/kotlin.ts'
           - 'etc/config/kotlin.*.properties'
 
+'lang-lean':
+  - changed-files:
+      - any-glob-to-any-file:
+          - 'lib/compilers/lean.ts'
+          - 'etc/config/lean.*.properties'
+          - 'static/modes/lean-mode.ts'
+
 'lang-llvm':
   - changed-files:
       - any-glob-to-any-file:
diff --git a/etc/config/lean.amazon.properties b/etc/config/lean.amazon.properties
new file mode 100644
index 000000000..0755571e1
--- /dev/null
+++ b/etc/config/lean.amazon.properties
@@ -0,0 +1,12 @@
+compilers=&lean
+defaultCompiler=lean_4_29_1
+compilerType=lean
+supportsBinary=false
+versionRe=^Lean \(version [^\n]+
+
+group.lean.compilers=lean_4_29_1
+group.lean.isSemVer=true
+group.lean.baseName=Lean
+
+compiler.lean_4_29_1.exe=/opt/compiler-explorer/lean-4.29.1/bin/lean
+compiler.lean_4_29_1.semver=4.29.1
diff --git a/etc/config/lean.defaults.properties b/etc/config/lean.defaults.properties
new file mode 100644
index 000000000..05a7fa1e5
--- /dev/null
+++ b/etc/config/lean.defaults.properties
@@ -0,0 +1,7 @@
+compilers=lean
+compilerType=lean
+supportsBinary=false
+versionRe=^Lean \(version [^\n]+
+
+compiler.lean.exe=lean
+compiler.lean.name=Lean
diff --git a/examples/lean/default.lean b/examples/lean/default.lean
new file mode 100644
index 000000000..7ed2624b4
--- /dev/null
+++ b/examples/lean/default.lean
@@ -0,0 +1,4 @@
+def add (x y : Nat) : Nat := x + y
+
+def main : IO Unit := do
+    IO.println (add 1 2)
diff --git a/lib/base-compiler.ts b/lib/base-compiler.ts
index 8ba4af6c6..359ff954f 100644
--- a/lib/base-compiler.ts
+++ b/lib/base-compiler.ts
@@ -1655,6 +1655,10 @@ export class BaseCompiler {
         return utils.changeExtension(inputFilename, '.dump-cmm');
     }
 
+    getLeanCOutputFilename(outputFilename: string) {
+        return utils.changeExtension(outputFilename, '.c');
+    }
+
     getYulOutputFilename(defaultOutputFilename: string) {
         return utils.changeExtension(defaultOutputFilename, '.yul');
     }
@@ -1737,6 +1741,25 @@ export class BaseCompiler {
         return [{text: 'Internal error; unable to open output path'}];
     }
 
+    async processLeanCOutput(
+        outputFilename: string,
+        output: CompilationResult,
+        options?: {['clang-format']: boolean} | null,
+    ): Promise<ResultLine[]> {
+        if (output.code !== 0) {
+            return [{text: 'Failed to run compiler to get Lean C output'}];
+        }
+        const outpath = this.getLeanCOutputFilename(outputFilename);
+        if (await utils.fileExists(outpath)) {
+            let content = await fs.readFile(outpath, 'utf8');
+            if (options?.['clang-format']) {
+                content = await this.applyClangFormat(content);
+            }
+            return content.split('\n').map(line => ({text: line}));
+        }
+        return [{text: 'Internal error; unable to open output path'}];
+    }
+
     async processYulOutput(
         defaultOutputFilename: string,
         result: CompilationResult,
@@ -2507,6 +2530,7 @@ export class BaseCompiler {
         const makeHaskellCore = backendOptions.produceHaskellCore && this.compiler.supportsHaskellCoreView;
         const makeHaskellStg = backendOptions.produceHaskellStg && this.compiler.supportsHaskellStgView;
         const makeHaskellCmm = backendOptions.produceHaskellCmm && this.compiler.supportsHaskellCmmView;
+        const makeLeanC = !!backendOptions.produceLeanC && this.compiler.supportsLeanCView;
         const makeGccDump = backendOptions.produceGccDump?.opened && this.compiler.supportsGccDump;
         const makeYul = backendOptions.produceYul && this.compiler.supportsYulView;
 
@@ -2575,6 +2599,10 @@ export class BaseCompiler {
             ? await this.processHaskellExtraOutput(this.getHaskellCmmOutputFilename(inputFilename), asmResult)
             : undefined;
 
+        const leanCResult = makeLeanC
+            ? await this.processLeanCOutput(outputFilename, asmResult, backendOptions.produceLeanC)
+            : undefined;
+
         const yulResult = makeYul
             ? await this.processYulOutput(outputFilename, asmResult, backendOptions.produceYul)
             : undefined;
@@ -2628,6 +2656,7 @@ export class BaseCompiler {
         asmResult.haskellCoreOutput = haskellCoreResult;
         asmResult.haskellStgOutput = haskellStgResult;
         asmResult.haskellCmmOutput = haskellCmmResult;
+        asmResult.leanCOutput = leanCResult;
 
         asmResult.clojureMacroExpOutput = clojureMacroExpResult;
 
diff --git a/lib/compilers/_all.ts b/lib/compilers/_all.ts
index 46325641f..7d355be55 100644
--- a/lib/compilers/_all.ts
+++ b/lib/compilers/_all.ts
@@ -103,6 +103,7 @@ export {JavaCompiler} from './java.js';
 export {JuliaCompiler} from './julia.js';
 export {KotlinCompiler} from './kotlin.js';
 export {LDCCompiler} from './ldc.js';
+export {LeanCompiler} from './lean.js';
 export {LFortranCompiler} from './lfortran.js';
 export {LLCCompiler} from './llc.js';
 export {LLVMmcaTool} from './llvm-mca.js';
diff --git a/lib/compilers/lean.ts b/lib/compilers/lean.ts
new file mode 100644
index 000000000..cd330bb81
--- /dev/null
+++ b/lib/compilers/lean.ts
@@ -0,0 +1,167 @@
+// Copyright (c) 2026, Compiler Explorer Authors
+// All rights reserved.
+//
+// Redistribution and use in source and binary forms, with or without
+// modification, are permitted provided that the following conditions are met:
+//
+//     * Redistributions of source code must retain the above copyright notice,
+//       this list of conditions and the following disclaimer.
+//     * Redistributions in binary form must reproduce the above copyright
+//       notice, this list of conditions and the following disclaimer in the
+//       documentation and/or other materials provided with the distribution.
+//
+// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+// AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+// IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+// ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS OR CONTRIBUTORS BE
+// LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
+// CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+// SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+// INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+// CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+// ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+// POSSIBILITY OF SUCH DAMAGE.
+
+import path from 'node:path';
+
+import {CompilationResult, ExecutionOptionsWithEnv} from '../../types/compilation/compilation.interfaces.js';
+import type {PreliminaryCompilerInfo} from '../../types/compiler.interfaces.js';
+import type {ParseFiltersAndOutputOptions} from '../../types/features/filters.interfaces.js';
+import {BaseCompiler} from '../base-compiler.js';
+import {CompilationEnvironment} from '../compilation-env.js';
+
+export class LeanCompiler extends BaseCompiler {
+    // Flags that will be forwarded to `lean` instead of `leanc`.
+    private readonly leanFlags = new Set(['--profile', '--stats']);
+
+    static get key() {
+        return 'lean';
+    }
+
+    constructor(info: PreliminaryCompilerInfo, env: CompilationEnvironment) {
+        super(info, env);
+        this.compiler.supportsLeanCView = true;
+    }
+
+    override optionsForFilter(filters: ParseFiltersAndOutputOptions, outputFilename: string) {
+        return [`--c=${this.getLeanCOutputFilename(outputFilename)}`];
+    }
+
+    override getSharedLibraryPathsAsArguments() {
+        return [];
+    }
+
+    private async getLeanPrefix(compiler: string, execOptions: ExecutionOptionsWithEnv): Promise<string | null> {
+        const prefixResult = await this.exec(compiler, ['--print-prefix'], execOptions);
+        const prefix = prefixResult.stdout.trim();
+        if (prefixResult.code === 0 && prefix) {
+            return prefix;
+        }
+
+        return null;
+    }
+
+    private async getLeancPath(compiler: string, execOptions: ExecutionOptionsWithEnv): Promise<string> {
+        const prefix = await this.getLeanPrefix(compiler, execOptions);
+        if (prefix) return path.join(prefix, 'bin', 'leanc');
+
+        return path.join(path.dirname(compiler), 'leanc');
+    }
+
+    private async doLeanBuildstep(
+        command: string,
+        args: string[],
+        execOptions: ExecutionOptionsWithEnv,
+        inputFilename: string,
+    ) {
+        const result = await this.exec(command, args, execOptions);
+        const processedResult = this.processExecutionResult(result, result.filenameTransform(inputFilename));
+
+        for (const output of [processedResult.stdout, processedResult.stderr]) {
+            for (const line of output) {
+                if (line.tag?.column !== undefined) {
+                    // Lean reports zero-based columns, Monaco diagnostics use one-based columns
+                    line.tag.column++;
+                }
+            }
+        }
+
+        return processedResult;
+    }
+
+    private partitionOptionsForSteps(
+        options: string[],
+        inputFilename: string,
+    ): {
+        leanOptions: string[];
+        leancOptions: string[];
+    } {
+        const leanOptions: string[] = [];
+        const leancOptions: string[] = [];
+
+        for (let i = 0; i < options.length; i++) {
+            const option = options[i];
+
+            if (option.startsWith('--c=')) {
+                leanOptions.push(option);
+            } else if (option === inputFilename) {
+                leanOptions.push(option);
+            } else if (this.leanFlags.has(option)) {
+                leanOptions.push(option);
+            } else {
+                leancOptions.push(option);
+            }
+        }
+
+        return {leanOptions, leancOptions};
+    }
+
+    override async runCompiler(
+        compiler: string,
+        options: string[],
+        inputFilename: string,
+        execOptions: ExecutionOptionsWithEnv,
+    ): Promise<CompilationResult> {
+        if (!execOptions) {
+            execOptions = this.getDefaultExecOptions();
+        }
+
+        const tmpDir = path.dirname(inputFilename);
+        if (!execOptions.customCwd) {
+            execOptions.customCwd = tmpDir;
+        }
+
+        const outputFilename = this.getOutputFilename(tmpDir, this.outputFilebase);
+
+        const cOutputOption = options.find(option => option.startsWith('--c='));
+        const cOutputFilename = cOutputOption?.substring('--c='.length) || this.getLeanCOutputFilename(outputFilename);
+
+        const {leanOptions, leancOptions} = this.partitionOptionsForSteps(options, inputFilename);
+
+        const leanResult = await this.doLeanBuildstep(compiler, leanOptions, execOptions, inputFilename);
+
+        if (leanResult.code !== 0) {
+            return {
+                ...leanResult,
+                inputFilename,
+                languageId: 'asm',
+            };
+        }
+
+        const leanc = await this.getLeancPath(compiler, execOptions);
+        const leancResult = await this.doBuildstep(
+            leanc,
+            [...leancOptions, '-S', cOutputFilename, '-o', outputFilename],
+            execOptions,
+        );
+
+        return {
+            ...leancResult,
+            okToCache: leanResult.okToCache && leancResult.okToCache,
+            stdout: leanResult.stdout.concat(leancResult.stdout),
+            stderr: leanResult.stderr.concat(leancResult.stderr),
+            inputFilename,
+            languageId: 'asm',
+        };
+    }
+}
diff --git a/lib/languages.ts b/lib/languages.ts
index 079e7809f..aa9e5f66e 100644
--- a/lib/languages.ts
+++ b/lib/languages.ts
@@ -584,6 +584,18 @@ const definitions: Record<LanguageKey, LanguageDefinition> = {
         monacoDisassembly: null,
         digitSeparator: '_',
     },
+    lean: {
+        name: 'Lean',
+        monaco: 'lean',
+        extensions: ['.lean'],
+        alias: [],
+        logoFilename: 'lean.png',
+        logoFilenameDark: null,
+        formatter: null,
+        previewFilter: null,
+        monacoDisassembly: null,
+        digitSeparator: '_',
+    },
     llvm: {
         name: 'LLVM IR',
         monaco: 'llvm-ir',
diff --git a/public/logos/lean.png b/public/logos/lean.png
new file mode 100644
index 0000000000000000000000000000000000000000..3882eed6f75794609929dd7633d3a4f2ee370a88
GIT binary patch
literal 6202
zcmb_gcTiJNmwyQf5RhI3=^$Mp28jfu2L+^yfb=TTlx7G5@&Y17K~WS?sRDwuU_m4x
z52PsgfdwJb5(^?y1rm^!FYfN_%<jz2d^7vq_s4y6?mOq)bI$Mm&Yhd-V0WC4XCDs$
z0DM-KcqagWv0q^THz#}YjIKVzp5y~8oooT%q6z?jmjPgtEdqZ6zy&k_{PG0={Q>~k
z8+pIg@hE$N)BnVAJiz+<l(s*-#g-_?TDZjq`o#w62Sf+4Cjf)SU=N~o4`MLR7_|N&
zJ$>CnnrO5>8a+7fuKYg~BF+bfoQeOx6*{hbEo3XG{kMnMkcgm|SigwK|E+`5*ZD6e
zoknFW_I?jq;Z2>1V+)h<EqgyD_5EH)Hh>u}eD5=O%l$?16N*;fYdmCa1B#u$-f_u3
zAsZInt$f`!Y)mD>NhBMa_35y#Mpg>t>_kfMK}S=^{VjqMk$XiC^{YfKEy&Sm0#{xw
zc`rr}-Y>+JjIJ)@le-Ibbb^h7@94~c8UM<_59iJFAG>~U^b5^i%6R|Rh8uMZ8BLVx
z(5gHU*fS9-cSSBLrYtU{fN_8A1y(#WBy36Btc1%{AT*UnS7HN>e#9L52c$?Jf@10M
z^pCny9ZAQxjvWn+tZVMe`DE#PqV)Vc#)TS9m+=)}-oJc?scnA6gbYM#4ExdzphHlO
zNeL(GjTv2tj-e}Hf?qapc17oW;)iM=H(!I&xcL?3K(S?wNRCM4vdfOPSrLaR9I9~$
z0DXWh!iupEVq3U{+ihR;x1gc`hAutPmpC7d(g9<@^f}|pdID`+;K?#3S3{SUDy3Yk
zMPfsN5MLq44dGk@NItNVY%i_T3w-oII%!kj<xr|OjJLyZ<YpY>dt?4wEWP4W$KhE?
zXOjmY@B24ChsXVA-sP0J2x<U#$s$B&fjjT_B+5x}qBqw@%@$IJBS5cEf@-yLn-C<4
z(06UuIviv5LL~BXx&=QnXHV0YngQurLsDa}*7ex42bSZPX~s&!Vo*M*-tgd@CIp&H
zi|Pqd4-*tB%su=BKDP6U0ZPBu!6>!XBYc&6$sY4&mJbm)I|X<tO5%G|JO`L<9^UqD
zPq-{a@PoQkn%miG;OED0m33adH_mH1jc`8g*1Ft%@`}ibB+{$Xqzk6E@wXL#{dKAV
zdriJN0<Tk{xh7tPC^bO%_N>#UaAd^%ilsCU0NaAEc2d)BY^wtZUn4X>QITM}--idh
zjPto;C?L&igSgY9b?>`5?1r8y!W(JV$$9RDq*URLlWQ8yj}r;h+?#i?mn@k|x2B;Y
zsGT}fZQ$$Gbk9*R)<ufUx6A=&&{r*B^3YvPl8s;;!n<ZCw_zNqCxQg?GLL!xdf}dN
z=j+4=9U%9zI)E3h0tBrJ;3oV1c>Ya-+y393-q@dUi<~XILq-1Fg9HIS`)wFx2Mt2v
zCNyf$fm|0~&C=xgl)CG1lZji&0rbf5V#pA*eP8b%qz(wr+}~CLSHZ^e)?9?l_scj{
zmJxItI@dIy{O5gT5ojA2ude^+)&t;%O1SVqQovsP%0s}?`NvA~UU~s_I#*8=h!$k_
zTMJhJmL4KxS9VR0@_<hxfN)8QpfKB|Gna5xYDu#gl)|n7Q4|OX<0#Jd;?6t{lNW%?
z{jF#jU^)EsxA`yDhN`dif7a|Y(i71pL6N^{%#P<RY!H~r@DhBJ5102V90$NH(l;>V
z?*<)#{evjdaZ(fXg8GCs-87);7jhKv8{1I$d_8pvdFe_vADTyMf8dEy907Ntf=>b=
z4O_eFRgj|wAlzb<Z=h0;(D0btZ0i^5Yik}r{rdbt(lPGET&D?dO`yVSa1}ONfk6hV
zJ6Yqq9Dt1dHZb{{Xe4OaB?>5_PX0dy{TQ{gym?_{3oGvv^YGYXlJHVV365}5gIk5P
zJ4r^ZGf*Rl8_WiM{GZfk<XMRD0Oxr+lq~u!^N0Tp&e8Igyl4@(%h`_=tN5rq60#Ke
zoEg${D@s%d2PZtiak(?RUl3>qrN9%`PE$vp`fUXr?coKHPzWStvP4bGtUyYjw)v??
z34Z!cS41A6^n_dXZJ-H$Jc0If_J8;uf<Z_&<83wZioDNaBlDUd>>ba6^|rT$By;c$
z@Ud3_MRDcP&^d5XBoc#liWbU7-T}UW*MAvTMNjk}PE4xadV0iAyHQe4mMYl)ES2Lk
z$Htj?v%0=0C>{c-$XsR`4=B0Of!N0}zn2gvn*VXL1Rv$Ws!IkgA=WN5oAM|+12!Dq
z%WZFA)KeyMmaUj<cus~_hTSjZeblyy{<*a8x&UUKxZ0$;{!%8(P{7jK%7fK<hVDs^
z4Q1FWI7lndK27no{fIBT$B`^Yers_gYvt+g=^c>OE$a#AA(b!70)@3;K4~1D_vbvR
zNFm#LxRgP|5DHsEl<0|c558twMbxB6nDEG<?uQXgmtZxYi=vx%Pv7%jJ=(C?Q7V|B
z84J9HFY=Km0>Dm(1)e<fIT}x0fBchXV3$j;x|3i%n1V3*fh|S0h;MYSY7i<5+UaJJ
zRs|!;*k%9A3!lX|#L%s~sb=yyM~$dNIFY)Fxkt`Xxo4)UX`ed6iYaz|58vh_YJX5!
zL~QS)Jd1jMI$HPufN_NlkZS>&Oe&L;pa0Y@oNY2#)*f~;W9!qD<pIQ%PstA4-!&Uk
zS%Axz#4%t_Vp#6csi^xSEPU6q-PKIi=f#&03qGz(y@WdOvvbH3nTW9IHVR;bB-2kQ
zJXd%;$^CJ2NdD4X$pwJv8_6)YOEWQAsRKHCIIk{;D9xWXIbVIOGOGCtKKz|Pi94uC
zN)uHD0DcZFPHb4Pk0sElY4SsZE<^7HYB!`X0yi}R_eVN|(?)y~vI*bDq7Gy4K+vWD
z4~e{T4t5Ui%|?}}b45ZVe|@qhVTolrAF%*gLH5;#<GJK$6!`WO<T*d}@%bx~Oc~~2
z@43riI}f|3S{P^HyFy!FwWLOj4X=8yA)T>tp49yC`($8D_|5>@##N3kO%K;tOMIB&
zkAQ5#$#~jJiv{)QH<|<7A1LeRE3}uFsHKV~v)98Erp1B6aqyH|U#W7j>mhi;O;3G3
zcUC7m|5=8AlI5&*v9v2xvVY$wJFy#LbGq;3NXI$C2cjSqhp{XSJVAJITqm!VF*Jr~
z$#^S~p={WkmKO#Dx))bcPeIm0wbZ?O=%I*T>JKp`CM_e$u)If%q0K#5?d~#$oGAQK
z_dGX7jH1n`(I&j03Rt^ZT@k5blvovzPOo4kTJ}gui>pokK3FlqA^#Dcl+iA<JZZRL
zGH+eFyzl9*M}oJ7m^-Vkj2g$0@VD@5HuDXoCqZ0s{)<D*1En?`4*Y$bxZe>fSZu)U
z`K%<<mav`lo6_IRvV?)cJ3kNB#g(2<_bUqF8K`+mQ?Z##7W>n@yA;q!O!E2kg4xx8
zxH7`F8f!nV36PgKrdHbC9(=vW=yW7SxQdZ{XWN5S=_c?}(7cP%3*_I5Kl@1VXX{xQ
zI_&E&g)cvVID}h|(6D<(`KfE1>$~GbZwo2HlCfNL`}+B=2KXRivEMH#-B)M7z$2E!
z(*Up7_i*3O<*vV2R8G%yR$+1+q*8O>u|s|G+XU7WHKK1FOpkV>xzWu+cZ^LG-icYX
zAb|uKVlp_rE3<rB&93rn<dR%Dqa$nEBYAWViX+Y9>gI@tg+iX=`9Pa#Pn2isr1|Dy
zVJYp>3__Xy`tHIXoss-x0{@)8*cQP=B$r_7*Z@GSoW^Y0Xm1+vlkaX6Wg{WNu(5n<
zvx6%we#w}Zmy{20e7HAK{BFk66XjecRX4RdTe-H1tG`~QQb`so@m+0|1;`2Egm1n@
z%kglE3{ht}^d2d>v)K4B$;>yYoD2MBG%q~z@RC~?1=d|FsNTG5Cwb|5QNb!lW3w^a
z>c`D)Ex^s9My5i5yx5tL;N4>i84aI1r0AMagc{wXNyog}_eR<SG-%?wknebJSosEt
zim$j@!?2PtJm;-o)^wIf2*??48tCye^m6F+@q1;%s3L?&SZOlP_*06tUccw`v?aN-
z4yYnj0v_O4aSO@jpZDC$h(%!)pP7}Cx)AK3+H#%+8n3lwJ!q=wF^@aBU@7v<LuhCh
z5A*n|*U;@g%PMD1pON?QU*$UhlSQO~wP%NbU+17JLhJ4IJ57#f{C8&UBd!@-|Fyom
zWcHhlQJc^1O|pr`uUG|wTDJHxk{QyZDy7Y2;j!&V7#4Yc=gIxDFN1w593gydV}8^=
zbEP?BHH1wWT>gRBob0yae2S=N$X_!!W8^N!Mu)Tu#o%s6tc(R80ID{*9{=#t>Dlgr
zTS_~nLo5A4cJDbZmyQ%$Lj=!Wpm4+wIbukRpT~$%KMfb(&Z}fJ#`JFqVYy6XIr3#Q
z3?(MYcg_1199n?Lqt_UUw=Voc<*l#AizqXClCLz@CGf1zagkg&l8vIC4aA)6gfPVh
z={z=KJfObi0flU^R4Q@<$mus~RTU?<@(P>cjxX{^0yzof^@+#FX8$8&-knCW7gf?v
zm0Y_ZwaE4Eq0j5V%pPYd@Y*>G2~|+1)eBJ2xWgjb<ma53CPCsMHfYF8A~%aNo|0ko
z7O^l%MDeR$$2w_M#2H`OMu#}@SrXYkW2oFy$tuC|C)-ZOsM_n`1|*u4^=$X_Al5J|
z>D3pCYjv%W&}<Du&Iv^_;{pRPUyPLxw)V68m>u^7?|l+WecFq|GE(sa1_^}^8*c0i
zHLrGUVhlw$FNw1W^cz$=iIDP*W%xcmB|z%p0#{*gbSuUUH!L*PzIW){7i{6&G8<lR
z$!##Drdy{ECs#*viy8sa_BZX1=PI`H6FDByHiLtjpYhH0Zi&?8pS4VFvO3PJWjTBj
zRI>o|CR0@fUy7;S%_j%TTlGt`#KYxtc~LZ6xEk}fL#3+XLH0MYH9J;s_J=mUatdWb
z<QV-Sn~KZ0;%c_>6={+}XOl2W{Res);QU>zpZcq$e99l%IqqwvBW2wWM#)jaLD@l2
zho5;?ktorNk!fiUc&CMCYdGHpB5it#x#mYdB5_mQob#TRqrLp$u$-Pn$0Q1AtYGt0
zP3+|K9!=(<5mK-cy&9^OP4$XOOm~;N_UN)n%{dsxU|VUvhP;#;Na!;QQfC%j3}zh;
z==@^fKtrfp^gdIAQ=K#mSNuSUabuK0%24nxW9Kh~(mGebHwkXX!CY>6dxqXU_IR&(
zU;Vi%xHLQw2Vtl18@tPu-#k%mR~a*MCL1W<mzkfg>VO?4e;N_i7mz?$(T!D<PS)E?
zvE_<E8gyX(1G#Y~x-Hdfx@G)e-4o*<ev`zKw|<{!y~lK>&`hJ{ve>`iDVU2d+-a%>
z2kkKN=;cvT^TG>Ypni`kg3XOb@-P5~YxhE^P6v^IF7&JLD&&}w3)@M$9$_q(@bUeR
z@J7A+Nvj74(S&tdyI@A|6|_P6O?$k1KRboJtcqJw0gXu)&C|K!lEbgzXjSy&obLW;
zGkVm@y^J-_`LLc3c6j$OfVi3UN#^Mf;5pK*XY}kccqrz^mVbT6QbMNyx$LEfX?=1q
zZfh1sj}1o`-q;NAy5+iVq2|GzhXq`;JPLM3GpVIFjria>bM&P?zz0PRiG$m7xt*KF
zDMWH%U-y+mwKCkEpsk^+ekC8!_XP5S-AT|R^SV6_{*c5`$B?78_cVtIjch&#-C2u~
z%+LGjB{l6I_|EEt=Y4tQe?HmuwmxwGI$p&g;mF*3?BU}6t*dT*g0w}>Dz+D=`+^&M
z%Sv5C+Kwd|Yan%;CRWK0^u^9k4LyHAQYcJbO3hZGWX>?Qk@s}t#HtxfHJl>3yZ4tx
za?hn-;G*5TxhKeH6Nvm#NZGgL(EZTQO@Q30?JK~Yv?aqtcpQyVQQX0e+&;2~uP_Mk
z5nL>M)q1gR4MrzQY?y=7vR7@DKV3HbJy{og)uYdU-su9enz8;SME=qq&)ip`>)lmG
z>pRz8Q>@viO?mCkV&ullVW~HFM^k9rWYoHdN=snG337T$ybZopch?{z-Zc}5oZvb-
z&F*pJt=*W{iF`laIMp$H_(ONh&!UB9*P8}i-qhLvf&43q;YOykb)N?$B@WRYh4~Q+
zc(j=>Y{c>BE_FJq9>c~K2TLw(t$ak6`e52^u0wQqGhIAN@k7@mXSVusLSBGG{c+Ul
zFQ>6Dm!SbRr_b8*dY-Id`!|bFt50z!J=>j=A>y~AnT!}}aCeM<zUGyFB&bv3o2&YP
zxF=y<TS!k~S(KoRW}l5#TwbstSB|~y(plGiaVKd{=uSWsb4!W(uzjgl%eDBCET9d4
z-lv7<_()3d-)lC4A|;T2?}`(`{FI&F0FhO<?pkgX22sk9TVK!To^;9V#&I6GHN>V7
z2lnbw^CtIkN$L@nle`_b4X}F~QB_(S4jkTaZsE?H%1R<XeW(6F6pWcB;;_imKQk>K
zJPK!%6W1j<iXatIwn$V_(6xINCG^Jzzt6Uk1NtKz4*$ZH_R~^oWK%n`Uj_NmSMkFD
z%2+5w^fntisgRsfLoyaS(vdfSnU9AqQ<12$71#}{)gG#;r&x{Js6#?u-AKpA{eZPY
z%ro>K)ajM_6?Ve+Ch(Lz-&^fFUDL|OSg~o-lp4cL7<L19L(ad1XC}$`NbVS3EOcj}
z2j{)y-;R{a^wRRV$qn?$d^ebx^6awlQNe`-D>~6q2l2Uoi~QAqdITQ-qIm4M3R`Oc
zM~ES7bDuDd5BpnQ6j3>y(PsV9PYH%oK#TB_-ihRL-u_!$dhPesn&rSyvB1qr^MLa&
ziSO9)edK1xhqgk30m1|W!G5X0V<iz`n%jcEKUlH*jleY}HfftyNCQJ6gg~m4Rcv0N
zsGb5EsV5~B)#7}U7nn)C9)?<7SRa2DM43Bq*JYa-bN)fO*BPm(oH@qjqKw0@FWG9b
z+e<)EY9a+m=~8RG?MCDFG3r#ISzZx=yZSy6NZa_a|8;@56(^_@Jb|eDx`~mSV~+o*
ztIcr#ZIHO>X-$-zI5~)~$OmS=Js*hYC0!(|uzPhM`3)}d1z&+!!h=@2!nRHA6sL{y
z)N^r1WN}8U7U_q!C6-N-;W)zVkASuOKUCk6`ayjj)sxMV)XeddPe>I1^R71bI~SjC
z8f*0};VWEEN==N!6<K2e>65d6@QMt_z~Y?tLtbm@%e)tvS_zVoFy``;cb$8k1|Eh@
zT50vl@-UxzPiE_CnC_PW1|b3CUKR0$hA`4qsRNWf#qdie>$2Pp-SF?dR4GRUpNgX4
zy~SkICU>Oxvv0!XcFHn9P8@iW%x~uP;<{JX<WiAE#6;(d^~590=Gd&0Whwz)9u&;I
z4`%dqD1MlE`b~;<#$Whkc_|$H^<D9ffBsIN2$4`*wH;^w`<m<#?X5-*@BtYuVX+m{
zrp;O9m%kI|cTmCM<t^y*t{1ojqXEt3Q8Ir76Np50Y=@r|)b*lcx^m0zdOI%d%lxP}
zbO}O1yU>gq<y<{5#Z?S7s66z49&FO0UkOx4@ry%epeg7j#DqAX(enLjj`B%GC)Vf4
z1sVJq|GewXz5&YzCrSTkYF$BLKlgv5ns?B}p3d(ZuJwkn5ZV|0PR`&D?Nu>zNa<sN
z2{ow}h&-(4dx4SkiG18e%nr<ZZupd+89`a0Hu8XkwMn8BQ}2s_%x>}{&)=i2ezk22
fivQBU{YidMc9+g=h@D|ywgXlccK8M}-;{p>EGsd*

literal 0
HcmV?d00001

diff --git a/static/components.interfaces.ts b/static/components.interfaces.ts
index e605450f1..cf3b0b095 100644
--- a/static/components.interfaces.ts
+++ b/static/components.interfaces.ts
@@ -27,6 +27,7 @@ import GoldenLayout from 'golden-layout';
 import {ConfiguredOverrides} from '../types/compilation/compiler-overrides.interfaces.js';
 import {ConfiguredRuntimeTools} from '../types/execution/execution.interfaces.js';
 import {CompilerOutputOptions} from '../types/features/filters.interfaces.js';
+import {ResultLine} from '../types/resultline/resultline.interfaces.js';
 import {CfgState} from './panes/cfg-view.interfaces.js';
 import {ClangirState} from './panes/clangir-view.interfaces.js';
 import {GccDumpViewState} from './panes/gccdump-view.interfaces.js';
@@ -71,6 +72,7 @@ export const RUST_MIR_VIEW_COMPONENT_NAME = 'rustmir' as const;
 export const HASKELL_CORE_VIEW_COMPONENT_NAME = 'haskellCore' as const;
 export const HASKELL_STG_VIEW_COMPONENT_NAME = 'haskellStg' as const;
 export const HASKELL_CMM_VIEW_COMPONENT_NAME = 'haskellCmm' as const;
+export const LEAN_C_VIEW_COMPONENT_NAME = 'leanC' as const;
 export const GNAT_DEBUG_TREE_VIEW_COMPONENT_NAME = 'gnatdebugtree' as const;
 export const GNAT_DEBUG_VIEW_COMPONENT_NAME = 'gnatdebug' as const;
 export const RUST_MACRO_EXP_VIEW_COMPONENT_NAME = 'rustmacroexp' as const;
@@ -297,6 +299,15 @@ export type PopulatedHaskellCmmViewState = StateWithId & {
     treeid: number;
 };
 
+export type EmptyLeanCViewState = EmptyState;
+export type PopulatedLeanCViewState = StateWithId & {
+    source: string;
+    leanCOutput: ResultLine[];
+    compilerName: string;
+    editorid: number;
+    treeid: number;
+};
+
 export type EmptyGnatDebugTreeViewState = EmptyState;
 export type PopulatedGnatDebugTreeViewState = StateWithId & {
     source: string;
@@ -396,6 +407,7 @@ export interface ComponentStateMap {
     [HASKELL_CORE_VIEW_COMPONENT_NAME]: EmptyHaskellCoreViewState | PopulatedHaskellCoreViewState;
     [HASKELL_STG_VIEW_COMPONENT_NAME]: EmptyHaskellStgViewState | PopulatedHaskellStgViewState;
     [HASKELL_CMM_VIEW_COMPONENT_NAME]: EmptyHaskellCmmViewState | PopulatedHaskellCmmViewState;
+    [LEAN_C_VIEW_COMPONENT_NAME]: EmptyLeanCViewState | PopulatedLeanCViewState;
     [GNAT_DEBUG_TREE_VIEW_COMPONENT_NAME]: EmptyGnatDebugTreeViewState | PopulatedGnatDebugTreeViewState;
     [GNAT_DEBUG_VIEW_COMPONENT_NAME]: EmptyGnatDebugViewState | PopulatedGnatDebugViewState;
     [RUST_MACRO_EXP_VIEW_COMPONENT_NAME]: EmptyRustMacroExpViewState | PopulatedRustMacroExpViewState;
diff --git a/static/components.ts b/static/components.ts
index 6d7312665..931775c68 100644
--- a/static/components.ts
+++ b/static/components.ts
@@ -28,6 +28,7 @@ import {ConfiguredOverrides} from '../types/compilation/compiler-overrides.inter
 import {ConfiguredRuntimeTools} from '../types/execution/execution.interfaces.js';
 import {ParseFiltersAndOutputOptions} from '../types/features/filters.interfaces.js';
 import {LanguageKey} from '../types/languages.interfaces.js';
+import {ResultLine} from '../types/resultline/resultline.interfaces.js';
 import {
     AnyComponentConfig,
     AST_VIEW_COMPONENT_NAME,
@@ -55,6 +56,7 @@ import {
     IR_VIEW_COMPONENT_NAME,
     ItemConfig,
     LayoutItem,
+    LEAN_C_VIEW_COMPONENT_NAME,
     LLVM_OPT_PIPELINE_VIEW_COMPONENT_NAME,
     OPT_PIPELINE_VIEW_COMPONENT_NAME,
     OPT_VIEW_COMPONENT_NAME,
@@ -816,6 +818,38 @@ export function getYulViewWith(
     };
 }
 
+/** Get an empty Lean C view component. */
+export function getLeanCView(): ComponentConfig<typeof LEAN_C_VIEW_COMPONENT_NAME> {
+    return {
+        type: 'component',
+        componentName: LEAN_C_VIEW_COMPONENT_NAME,
+        componentState: {},
+    };
+}
+
+/** Get a Lean C view with the given configuration. */
+export function getLeanCViewWith(
+    id: number,
+    source: string,
+    leanCOutput: ResultLine[] | undefined,
+    compilerName: string,
+    editorid: number,
+    treeid: number,
+): ComponentConfig<typeof LEAN_C_VIEW_COMPONENT_NAME> {
+    return {
+        type: 'component',
+        componentName: LEAN_C_VIEW_COMPONENT_NAME,
+        componentState: {
+            id,
+            source,
+            leanCOutput,
+            compilerName,
+            editorid,
+            treeid,
+        },
+    };
+}
+
 /** Get an empty gnat debug tree view component. */
 export function getGnatDebugTreeView(): ComponentConfig<typeof GNAT_DEBUG_TREE_VIEW_COMPONENT_NAME> {
     return {
diff --git a/static/event-map.ts b/static/event-map.ts
index 138e82d80..5dde3f187 100644
--- a/static/event-map.ts
+++ b/static/event-map.ts
@@ -35,6 +35,7 @@ import {MessageWithLocation} from '../types/resultline/resultline.interfaces.js'
 import {NewToolSettings, ToolState} from './components.interfaces.js';
 import {Motd} from './motd.interfaces.js';
 import {GccDumpFiltersState, GccDumpViewSelectedPass} from './panes/gccdump-view.interfaces.js';
+import {LeanCOptions} from './panes/leanc-view.interfaces.js';
 import {PPOptions} from './panes/pp-view.interfaces.js';
 import {SiteSettings} from './settings.js';
 import {Theme} from './themes.js';
@@ -114,6 +115,9 @@ export type EventMap = {
     haskellCoreViewOpened: (compilerId: number) => void;
     haskellStgViewClosed: (compilerId: number) => void;
     haskellStgViewOpened: (compilerId: number) => void;
+    leanCViewClosed: (compilerId: number) => void;
+    leanCViewOpened: (compilerId: number) => void;
+    leanCViewOptionsUpdated: (compilerId: number, options: LeanCOptions, recompile: boolean) => void;
     initialised: () => void;
     irViewClosed: (compilerId: number) => void;
     irViewOpened: (compilerId: number) => void;
diff --git a/static/hub.ts b/static/hub.ts
index 15f66e0f7..23b467ad1 100644
--- a/static/hub.ts
+++ b/static/hub.ts
@@ -48,6 +48,7 @@ import {
     HASKELL_STG_VIEW_COMPONENT_NAME,
     InferComponentState,
     IR_VIEW_COMPONENT_NAME,
+    LEAN_C_VIEW_COMPONENT_NAME,
     LLVM_OPT_PIPELINE_VIEW_COMPONENT_NAME,
     OPT_PIPELINE_VIEW_COMPONENT_NAME,
     OPT_VIEW_COMPONENT_NAME,
@@ -84,6 +85,7 @@ import {HaskellCmm as HaskellCmmView} from './panes/haskellcmm-view.js';
 import {HaskellCore as HaskellCoreView} from './panes/haskellcore-view.js';
 import {HaskellStg as HaskellStgView} from './panes/haskellstg-view.js';
 import {Ir as IrView} from './panes/ir-view.js';
+import {LeanC as LeanCView} from './panes/leanc-view.js';
 import {OptPipeline} from './panes/opt-pipeline.js';
 import {Opt as OptView} from './panes/opt-view.js';
 import {Output} from './panes/output.js';
@@ -159,6 +161,7 @@ export class Hub {
         );
         layout.registerComponent(HASKELL_STG_VIEW_COMPONENT_NAME, (c: GLC, s: any) => this.haskellStgViewFactory(c, s));
         layout.registerComponent(HASKELL_CMM_VIEW_COMPONENT_NAME, (c: GLC, s: any) => this.haskellCmmViewFactory(c, s));
+        layout.registerComponent(LEAN_C_VIEW_COMPONENT_NAME, (c: GLC, s: any) => this.leanCViewFactory(c, s));
         layout.registerComponent(GNAT_DEBUG_TREE_VIEW_COMPONENT_NAME, (c: GLC, s: any) =>
             this.gnatDebugTreeViewFactory(c, s),
         );
@@ -583,6 +586,10 @@ export class Hub {
         return new HaskellCmmView(this, container, state);
     }
 
+    public leanCViewFactory(container: GoldenLayout.Container, state: InferComponentState<LeanCView>): LeanCView {
+        return new LeanCView(this, container, state);
+    }
+
     public clojureMacroExpViewFactory(
         container: GoldenLayout.Container,
         state: InferComponentState<ClojureMacroExpView>,
diff --git a/static/modes/_all.ts b/static/modes/_all.ts
index 5f0577572..d6c3a1c24 100644
--- a/static/modes/_all.ts
+++ b/static/modes/_all.ts
@@ -52,6 +52,7 @@ import './hook-mode';
 import './hylo-mode';
 import './ispc-mode';
 import './jakt-mode';
+import './lean-mode';
 import './llvm-ir-mode';
 import './mlir-mode';
 import './modula2-mode';
diff --git a/static/modes/lean-mode.ts b/static/modes/lean-mode.ts
new file mode 100644
index 000000000..5604ba219
--- /dev/null
+++ b/static/modes/lean-mode.ts
@@ -0,0 +1,347 @@
+// Copyright (c) 2026, Compiler Explorer Authors
+// All rights reserved.
+//
+// Redistribution and use in source and binary forms, with or without
+// modification, are permitted provided that the following conditions are met:
+//
+//     * Redistributions of source code must retain the above copyright notice,
+//       this list of conditions and the following disclaimer.
+//     * Redistributions in binary form must reproduce the above copyright
+//       notice, this list of conditions and the following disclaimer in the
+//       documentation and/or other materials provided with the distribution.
+//
+// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+// AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+// IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+// ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE
+// LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
+// CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+// SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+// INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+// CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+// ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+// POSSIBILITY OF SUCH DAMAGE.
+
+import * as monaco from 'monaco-editor';
+
+// Based on https://github.com/leanprover/vscode-lean4/blob/bbe3ff12/vscode-lean4/syntaxes/lean4.json.
+function definition(): monaco.languages.IMonarchLanguage {
+    return {
+        escapes: /\\(?:[\\'"ntr]|x[0-9A-Fa-f]{2}|u[0-9A-Fa-f]{4})/,
+        keywords: [
+            'local',
+            'scoped',
+            'partial',
+            'unsafe',
+            'nonrec',
+            'public',
+            'private',
+            'protected',
+            'noncomputable',
+            'meta',
+            'deriving',
+            'instance',
+            'inductive',
+            'coinductive',
+            'structure',
+            'theorem',
+            'axiom',
+            'abbrev',
+            'lemma',
+            'def',
+            'instance',
+            'class',
+            'with',
+            'extends',
+            'where',
+            'theorem',
+            'show',
+            'have',
+            'using',
+            'haveI',
+            'from',
+            'suffices',
+            'nomatch',
+            'nofun',
+            'no_index',
+            'def',
+            'class',
+            'structure',
+            'instance',
+            'elab',
+            'set_option',
+            'initialize',
+            'builtin_initialize',
+            'example',
+            'inductive_fixpoint',
+            'inductive',
+            'coinductive_fixpoint',
+            'coinductive',
+            'termination_by?',
+            'termination_by',
+            'decreasing_by',
+            'partial_fixpoint',
+            'axiom',
+            'universe',
+            'variable',
+            'module',
+            'import all',
+            'import',
+            'open',
+            'export',
+            'prelude',
+            'renaming',
+            'hiding',
+            'do',
+            'by?',
+            'by',
+            'let',
+            'letI',
+            'let_expr',
+            'extends',
+            'mutual',
+            'mut',
+            'where',
+            'rec',
+            'declare_syntax_cat',
+            'syntax',
+            'macro_rules',
+            'macro',
+            'max_prec',
+            'leading_parser',
+            'elab_rules',
+            'deriving',
+            'fun',
+            'section',
+            'namespace',
+            'end',
+            'prefix',
+            'postfix',
+            'infixl',
+            'infixr',
+            'infix',
+            'notation',
+            'abbrev',
+            'if',
+            'bif',
+            'then',
+            'else',
+            'calc',
+            'matches',
+            'match_expr',
+            'match',
+            'with',
+            'forall',
+            'for',
+            'while',
+            'repeat',
+            'unless',
+            'until',
+            'panic!',
+            'unreachable!',
+            'assert!',
+            'try',
+            'catch',
+            'finally',
+            'return',
+            'continue',
+            'break',
+            'exists',
+            'mod_cast',
+            'include_str',
+            'include',
+            'in',
+            'trailing_parser',
+            'tactic_tag',
+            'tactic_alt',
+            'tactic_extension',
+            'register_tactic_tag',
+            'binder_predicate',
+            'grind_propagator',
+            'builtin_grind_propagator',
+            'grind_pattern',
+            'simproc',
+            'builtin_simproc',
+            'simproc_decl',
+            'builtin_simproc_decl',
+            'dsimproc',
+            'builtin_dsimproc',
+            'dsimproc_decl',
+            'builtin_dsimproc_decl',
+            'show_panel_widgets',
+            'show_term',
+            'seal',
+            'unseal',
+            'nat_lit',
+            'norm_cast_add_elim',
+            'println!',
+            'declare_config_elab',
+            'register_error_explanation',
+            'register_builtin_option',
+            'register_option',
+            'register_parser_alias',
+            'register_simp_attr',
+            'register_linter_set',
+            'register_label_attr',
+            'recommended_spelling',
+            'reportIssue!',
+            'reprove',
+            'run_elab',
+            'run_cmd',
+            'run_meta',
+            'add_decl_doc',
+            'omit',
+            'opaque',
+            'dbg_trace',
+            'trace_goal',
+            'trace',
+            'throwErrorAt',
+            'throwError',
+            'throwNamedErrorAt',
+            'throwNamedError',
+            'logNamedWarningAt',
+            'logNamedWarning',
+            'logNamedErrorAt',
+            'logNamedError',
+        ],
+        types: ['Prop', 'Type', 'Sort'],
+        invalidKeywords: ['sorry', 'admit'],
+        commands: [
+            '#print',
+            '#eval',
+            '#eval!',
+            '#reduce',
+            '#synth',
+            '#widget',
+            '#where',
+            '#version',
+            '#with_exporting',
+            '#check',
+            '#check_tactic',
+            '#check_tactic_failure',
+            '#check_failure',
+            '#check_simp',
+            '#discr_tree_key',
+            '#discr_tree_simp_key',
+            '#guard',
+            '#guard_expr',
+            '#guard_msgs',
+        ],
+        invalidCommands: ['#exit'],
+
+        tokenizer: {
+            root: [
+                [/r(#*)"/, {token: 'string.quote', bracket: '@open', next: '@stringraw.$1'}],
+                {include: '@whitespace'},
+
+                [/"/, 'string', '@string'],
+                [/(?<![\]\w])'[^\\']'/, 'string'],
+                [/(?<![\]\w])(')(@escapes)(')/, ['string', 'string.escape', 'string']],
+
+                [/\b(0[xX][0-9a-fA-F]+|[0-9]+|-?(0|[1-9][0-9]*)(\.[0-9]+)?([eE][+-]?[0-9]+)?)\b/, 'number'],
+                [/«/, 'identifier', '@escapedIdentifier'],
+                [/\battribute\b\s*\[[^\]\s]*\]/, 'keyword.modifier'],
+                [/@\[[^\]\s]*\]/, 'keyword.modifier'],
+                [
+                    /#[a-zA-Z_][a-zA-Z0-9_!]*/,
+                    {
+                        cases: {
+                            '@invalidCommands': 'invalid',
+                            '@commands': 'keyword',
+                            '@default': '',
+                        },
+                    },
+                ],
+                [/[{}()[\]]/, '@brackets'],
+                [
+                    /[a-zA-Z_][a-zA-Z0-9_'?!]*/,
+                    {
+                        cases: {
+                            '@invalidKeywords': 'invalid',
+                            '@keywords': 'keyword',
+                            '@types': 'keyword.type',
+                            '@default': 'identifier',
+                        },
+                    },
+                ],
+            ],
+
+            whitespace: [
+                [/[ \t\r\n]+/, 'white'],
+                [/--.*$/, 'comment'],
+                [/\/--/, 'comment.doc', '@docComment'],
+                [/\/-!/, 'comment.doc', '@docComment'],
+                [/\/-/, 'comment', '@blockComment'],
+            ],
+
+            docComment: [
+                [/[^/-]+/, 'comment.doc'],
+                [/\/-/, 'comment.doc', '@blockComment'],
+                [/-\//, 'comment.doc', '@pop'],
+                [/[/-]/, 'comment.doc'],
+            ],
+
+            blockComment: [
+                [/[^/-]+/, 'comment'],
+                [/\/-/, 'comment', '@push'],
+                [/-\//, 'comment', '@pop'],
+                [/[/-]/, 'comment'],
+            ],
+
+            string: [
+                [/[^\\"]+/, 'string'],
+                [/@escapes/, 'string.escape'],
+                [/\\./, 'string.escape.invalid'],
+                [/"/, 'string', '@pop'],
+            ],
+
+            escapedIdentifier: [
+                [/[^»]+/, 'identifier'],
+                [/»/, 'identifier', '@pop'],
+            ],
+
+            stringraw: [
+                [/[^"#]+/, {token: 'string'}],
+                [
+                    /"(#*)/,
+                    {
+                        cases: {
+                            '$1==$S2': {token: 'string.quote', bracket: '@close', next: '@pop'},
+                            '@default': {token: 'string'},
+                        },
+                    },
+                ],
+                [/["#]/, {token: 'string'}],
+            ],
+        },
+    };
+}
+
+monaco.languages.register({id: 'lean'});
+monaco.languages.setMonarchTokensProvider('lean', definition());
+monaco.languages.setLanguageConfiguration('lean', {
+    comments: {
+        lineComment: '--',
+        blockComment: ['/-', '-/'],
+    },
+
+    brackets: [
+        ['(', ')'],
+        ['[', ']'],
+        ['{', '}'],
+    ],
+
+    autoClosingPairs: [
+        {open: '(', close: ')'},
+        {open: '[', close: ']'},
+        {open: '{', close: '}'},
+        {open: '"', close: '"', notIn: ['string', 'comment']},
+    ],
+
+    surroundingPairs: [
+        {open: '(', close: ')'},
+        {open: '[', close: ']'},
+        {open: '{', close: '}'},
+        {open: '"', close: '"'},
+    ],
+});
diff --git a/static/panes/compiler.ts b/static/panes/compiler.ts
index 0cc0c3417..c74444db2 100644
--- a/static/panes/compiler.ts
+++ b/static/panes/compiler.ts
@@ -66,6 +66,7 @@ import * as TimingWidget from '../widgets/timing-info-widget.js';
 import {Toggles} from '../widgets/toggles.js';
 import {CompilerCurrentState, CompilerState} from './compiler.interfaces.js';
 import {GccDumpFiltersState, GccDumpViewSelectedPass} from './gccdump-view.interfaces.js';
+import {LeanCOptions} from './leanc-view.interfaces.js';
 import {MonacoPaneState} from './pane.interfaces.js';
 import {MonacoPane} from './pane.js';
 import {PPOptions} from './pp-view.interfaces.js';
@@ -197,6 +198,7 @@ export class Compiler extends MonacoPane<monaco.editor.IStandaloneCodeEditor, Co
     private haskellCoreButton: JQuery<HTMLButtonElement>;
     private haskellStgButton: JQuery<HTMLButtonElement>;
     private haskellCmmButton: JQuery<HTMLButtonElement>;
+    private leanCButton: JQuery<HTMLButtonElement>;
     private clojureMacroExpButton: JQuery<HTMLButtonElement>;
     private yulButton: JQuery<HTMLButtonElement>;
     private gccDumpButton: JQuery<HTMLButtonElement>;
@@ -276,6 +278,8 @@ export class Compiler extends MonacoPane<monaco.editor.IStandaloneCodeEditor, Co
     private haskellCoreViewOpen: boolean;
     private haskellStgViewOpen: boolean;
     private haskellCmmViewOpen: boolean;
+    private leanCViewOpen: boolean;
+    private leanCOptions: LeanCOptions;
     private clojureMacroExpViewOpen: boolean;
     private yulViewOpen: boolean;
     private ppOptions: PPOptions;
@@ -633,6 +637,17 @@ export class Compiler extends MonacoPane<monaco.editor.IStandaloneCodeEditor, Co
             );
         };
 
+        const createLeanCView = () => {
+            return Components.getLeanCViewWith(
+                this.id,
+                this.source,
+                this.lastResult?.leanCOutput,
+                this.getCompilerName(),
+                this.sourceEditorId ?? 0,
+                this.sourceTreeId ?? 0,
+            );
+        };
+
         const createClojureMacroExpView = () => {
             return Components.getClojureMacroExpViewWith(
                 this.id,
@@ -904,6 +919,18 @@ export class Compiler extends MonacoPane<monaco.editor.IStandaloneCodeEditor, Co
             insertPoint.addChild(createHaskellCmmView());
         });
 
+        createDragSource(this.container.layoutManager, this.leanCButton, () => createLeanCView()).on(
+            'dragStart',
+            hidePaneAdder,
+        );
+
+        this.leanCButton.on('click', () => {
+            const insertPoint =
+                this.hub.findParentRowOrColumn(this.container.parent) ||
+                this.container.layoutManager.root.contentItems[0];
+            insertPoint.addChild(createLeanCView());
+        });
+
         createDragSource(this.container.layoutManager, this.rustMacroExpButton, () => createRustMacroExpView()).on(
             'dragStart',
             hidePaneAdder,
@@ -1346,6 +1373,7 @@ export class Compiler extends MonacoPane<monaco.editor.IStandaloneCodeEditor, Co
                 produceHaskellCore: this.haskellCoreViewOpen,
                 produceHaskellStg: this.haskellStgViewOpen,
                 produceHaskellCmm: this.haskellCmmViewOpen,
+                produceLeanC: this.leanCViewOpen ? this.leanCOptions : null,
                 produceClojureMacroExp: this.clojureMacroExpViewOpen,
                 produceYul: this.yulViewOpen ? this.yulOptions : null,
                 overrides: this.getCurrentState().overrides,
@@ -2216,6 +2244,29 @@ export class Compiler extends MonacoPane<monaco.editor.IStandaloneCodeEditor, Co
         }
     }
 
+    onLeanCViewOpened(id: number): void {
+        if (this.id === id) {
+            this.leanCButton.prop('disabled', true);
+            this.leanCViewOpen = true;
+        }
+    }
+
+    onLeanCViewClosed(id: number): void {
+        if (this.id === id) {
+            this.leanCButton.prop('disabled', false);
+            this.leanCViewOpen = false;
+        }
+    }
+
+    onLeanCViewOptionsUpdated(id: number, options: LeanCOptions, recompile: boolean): void {
+        if (this.id === id) {
+            this.leanCOptions = options;
+            if (recompile) {
+                this.compile();
+            }
+        }
+    }
+
     onGnatDebugTreeViewOpened(id: number): void {
         if (this.id === id) {
             this.gnatDebugTreeButton.prop('disabled', true);
@@ -2503,6 +2554,7 @@ export class Compiler extends MonacoPane<monaco.editor.IStandaloneCodeEditor, Co
         this.haskellCoreButton = this.domRoot.find('.btn.view-haskellCore');
         this.haskellStgButton = this.domRoot.find('.btn.view-haskellStg');
         this.haskellCmmButton = this.domRoot.find('.btn.view-haskellCmm');
+        this.leanCButton = this.domRoot.find('.btn.view-leanC');
         this.clojureMacroExpButton = this.domRoot.find('.btn.view-clojuremacroexp');
         this.yulButton = this.domRoot.find('.btn.view-yul');
         this.gccDumpButton = this.domRoot.find('.btn.view-gccdump');
@@ -2794,6 +2846,7 @@ export class Compiler extends MonacoPane<monaco.editor.IStandaloneCodeEditor, Co
         this.haskellCoreButton.prop('disabled', this.haskellCoreViewOpen);
         this.haskellStgButton.prop('disabled', this.haskellStgViewOpen);
         this.haskellCmmButton.prop('disabled', this.haskellCmmViewOpen);
+        this.leanCButton.prop('disabled', this.leanCViewOpen);
         this.rustMacroExpButton.prop('disabled', this.rustMacroExpViewOpen);
         this.rustHirButton.prop('disabled', this.rustHirViewOpen);
         this.clojureMacroExpButton.prop('disabled', this.clojureMacroExpViewOpen);
@@ -2818,6 +2871,7 @@ export class Compiler extends MonacoPane<monaco.editor.IStandaloneCodeEditor, Co
         this.haskellCoreButton.toggle(!!this.compiler.supportsHaskellCoreView);
         this.haskellStgButton.toggle(!!this.compiler.supportsHaskellStgView);
         this.haskellCmmButton.toggle(!!this.compiler.supportsHaskellCmmView);
+        this.leanCButton.toggle(!!this.compiler.supportsLeanCView);
         this.clojureMacroExpButton.toggle(!!this.compiler.supportsClojureMacroExpView);
         this.yulButton.toggle(!!this.compiler.supportsYulView);
         // TODO(jeremy-rifkin): Disable cfg button when binary mode is set?
@@ -3000,6 +3054,9 @@ export class Compiler extends MonacoPane<monaco.editor.IStandaloneCodeEditor, Co
         this.eventHub.on('haskellStgViewClosed', this.onHaskellStgViewClosed, this);
         this.eventHub.on('haskellCmmViewOpened', this.onHaskellCmmViewOpened, this);
         this.eventHub.on('haskellCmmViewClosed', this.onHaskellCmmViewClosed, this);
+        this.eventHub.on('leanCViewOpened', this.onLeanCViewOpened, this);
+        this.eventHub.on('leanCViewClosed', this.onLeanCViewClosed, this);
+        this.eventHub.on('leanCViewOptionsUpdated', this.onLeanCViewOptionsUpdated, this);
         this.eventHub.on('clojureMacroExpViewOpened', this.onClojureMacroExpViewOpened, this);
         this.eventHub.on('clojureMacroExpViewClosed', this.onClojureMacroExpViewClosed, this);
         this.eventHub.on('yulViewOpened', this.onYulViewOpened, this);
diff --git a/static/panes/diff.interfaces.ts b/static/panes/diff.interfaces.ts
index 829e7c380..768be9489 100644
--- a/static/panes/diff.interfaces.ts
+++ b/static/panes/diff.interfaces.ts
@@ -39,6 +39,7 @@ export enum DiffType {
     RustHirOutput = 12,
     ClojureMacroExpOutput = 13,
     YulOutput = 14,
+    LeanCOutput = 15,
 }
 
 export type DiffState = {
diff --git a/static/panes/diff.ts b/static/panes/diff.ts
index 59a00b122..130b2bd65 100644
--- a/static/panes/diff.ts
+++ b/static/panes/diff.ts
@@ -181,6 +181,11 @@ class DiffStateObject {
                         {text: "<select 'Add new...' → 'Yul (Solidity IR)' in this compiler's pane>"},
                     ];
                     break;
+                case DiffType.LeanCOutput:
+                    output = this.result.leanCOutput || [
+                        {text: "<select 'Add new...' → 'Lean C Output' in this compiler's pane>"},
+                    ];
+                    break;
             }
         }
         this.model.setValue(output.map(x => x.text).join('\n'));
@@ -490,6 +495,9 @@ export class Diff extends MonacoPane<monaco.editor.IStandaloneDiffEditor, DiffSt
             if (compiler.supportsYulView) {
                 options.push({id: DiffType.YulOutput.toString(), name: 'Yul (Solidity IR)'});
             }
+            if (compiler.supportsLeanCView) {
+                options.push({id: DiffType.LeanCOutput.toString(), name: 'Lean C Output'});
+            }
         }
 
         const lhsoptions = this.getDiffableOptions(this.selectize.lhs, lhsextraoptions);
diff --git a/static/panes/leanc-view.interfaces.ts b/static/panes/leanc-view.interfaces.ts
new file mode 100644
index 000000000..8f5fd1464
--- /dev/null
+++ b/static/panes/leanc-view.interfaces.ts
@@ -0,0 +1,31 @@
+// Copyright (c) 2026, Compiler Explorer Authors
+// All rights reserved.
+//
+// Redistribution and use in source and binary forms, with or without
+// modification, are permitted provided that the following conditions are met:
+//
+//     * Redistributions of source code must retain the above copyright notice,
+//       this list of conditions and the following disclaimer.
+//     * Redistributions in binary form must reproduce the above copyright
+//       notice, this list of conditions and the following disclaimer in the
+//       documentation and/or other materials provided with the distribution.
+//
+// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+// AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+// IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+// ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS OR CONTRIBUTORS BE
+// LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
+// CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+// SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+// INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+// CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+// ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+// POSSIBILITY OF SUCH DAMAGE.
+
+import {ResultLine} from '../../types/resultline/resultline.interfaces.js';
+
+export interface LeanCState {
+    leanCOutput: ResultLine[];
+}
+
+export type {LeanCOptions} from '../../types/compilation/lean-c.interfaces.js';
diff --git a/static/panes/leanc-view.ts b/static/panes/leanc-view.ts
new file mode 100644
index 000000000..d8b94b461
--- /dev/null
+++ b/static/panes/leanc-view.ts
@@ -0,0 +1,151 @@
+// Copyright (c) 2026, Compiler Explorer Authors
+// All rights reserved.
+//
+// Redistribution and use in source and binary forms, with or without
+// modification, are permitted provided that the following conditions are met:
+//
+//     * Redistributions of source code must retain the above copyright notice,
+//       this list of conditions and the following disclaimer.
+//     * Redistributions in binary form must reproduce the above copyright
+//       notice, this list of conditions and the following disclaimer in the
+//       documentation and/or other materials provided with the distribution.
+//
+// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+// AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+// IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+// ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS OR CONTRIBUTORS BE
+// LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
+// CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+// SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+// INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+// CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+// ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+// POSSIBILITY OF SUCH DAMAGE.
+
+import {Container} from 'golden-layout';
+import $ from 'jquery';
+import * as monaco from 'monaco-editor';
+import _ from 'underscore';
+
+import {CompilationResult} from '../../types/compilation/compilation.interfaces.js';
+import {CompilerInfo} from '../../types/compiler.interfaces.js';
+import {Hub} from '../hub.js';
+import {extendConfig} from '../monaco-config.js';
+import {Toggles} from '../widgets/toggles.js';
+import {LeanCOptions, LeanCState} from './leanc-view.interfaces.js';
+import {MonacoPaneState} from './pane.interfaces.js';
+import {MonacoPane} from './pane.js';
+
+export class LeanC extends MonacoPane<monaco.editor.IStandaloneCodeEditor, LeanCState> {
+    private options: Toggles;
+
+    constructor(hub: Hub, container: Container, state: LeanCState & MonacoPaneState) {
+        super(hub, container, state);
+        if (state.leanCOutput) {
+            this.showLeanCResults(state.leanCOutput);
+        }
+
+        this.onOptionsChange();
+    }
+
+    override getInitialHTML(): string {
+        return $('#leanC').html();
+    }
+
+    override createEditor(editorRoot: HTMLElement): void {
+        this.editor = monaco.editor.create(
+            editorRoot,
+            extendConfig({
+                language: 'c',
+                readOnly: true,
+                glyphMargin: true,
+                lineNumbersMinChars: 3,
+            }),
+        );
+    }
+
+    override getPrintName() {
+        return 'Lean C Output';
+    }
+
+    override getDefaultPaneName(): string {
+        return 'Lean C Output';
+    }
+
+    override registerButtons(state: LeanCState & MonacoPaneState): void {
+        super.registerButtons(state);
+        this.options = new Toggles(this.domRoot.find('.options'), state as unknown as Record<string, boolean>);
+        this.options.on('change', this.onOptionsChange.bind(this));
+    }
+
+    override registerCallbacks(): void {
+        const throttleFunction = _.throttle(
+            (event: monaco.editor.ICursorSelectionChangedEvent) => this.onDidChangeCursorSelection(event),
+            500,
+        );
+        this.editor.onDidChangeCursorSelection(event => throttleFunction(event));
+        this.eventHub.emit('leanCViewOpened', this.compilerInfo.compilerId);
+        this.eventHub.emit('requestSettings');
+    }
+
+    override getCurrentState(): MonacoPaneState {
+        return {
+            ...super.getCurrentState(),
+            ...this.options.get(),
+        };
+    }
+
+    onOptionsChange(): void {
+        const options = this.options.get() as LeanCOptions;
+        this.updateState();
+        this.showLeanCResults([{text: '<Compiling...>'}]);
+        this.eventHub.emit('leanCViewOptionsUpdated', this.compilerInfo.compilerId, options, true);
+    }
+
+    override onCompileResult(compilerId: number, compiler: CompilerInfo, result: CompilationResult): void {
+        if (this.compilerInfo.compilerId !== compilerId) return;
+        if (result.leanCOutput) {
+            this.showLeanCResults(result.leanCOutput);
+        } else if (compiler.supportsLeanCView) {
+            this.showLeanCResults([{text: '<No output>'}]);
+        }
+    }
+
+    override onCompiler(
+        compilerId: number,
+        compiler: CompilerInfo | null,
+        options: string,
+        editorId?: number,
+        treeId?: number,
+    ): void {
+        if (this.compilerInfo.compilerId === compilerId) {
+            this.compilerInfo.compilerName = compiler ? compiler.name : '';
+            this.compilerInfo.editorId = editorId;
+            this.compilerInfo.treeId = treeId;
+            this.updateTitle();
+            if (compiler && !compiler.supportsLeanCView) {
+                this.showLeanCResults([{text: '<Lean C output is not supported for this compiler>'}]);
+            }
+        }
+    }
+
+    showLeanCResults(result: Record<'text', string>[]): void {
+        this.editor
+            .getModel()
+            ?.setValue(result.length ? _.pluck(result, 'text').join('\n') : '<No Lean C output generated>');
+
+        if (!this.isAwaitingInitialResults) {
+            if (this.selection) {
+                this.editor.setSelection(this.selection);
+                this.editor.revealLinesInCenter(this.selection.selectionStartLineNumber, this.selection.endLineNumber);
+            }
+            this.isAwaitingInitialResults = true;
+        }
+    }
+
+    override close(): void {
+        this.eventHub.unsubscribe();
+        this.eventHub.emit('leanCViewClosed', this.compilerInfo.compilerId);
+        this.editor.dispose();
+    }
+}
diff --git a/types/compilation/compilation.interfaces.ts b/types/compilation/compilation.interfaces.ts
index 0546c758c..569bb6258 100644
--- a/types/compilation/compilation.interfaces.ts
+++ b/types/compilation/compilation.interfaces.ts
@@ -41,6 +41,7 @@ import {CFGResult} from './cfg.interfaces.js';
 import {ClangirBackendOptions} from './clangir.interfaces.js';
 import {ConfiguredOverrides} from './compiler-overrides.interfaces.js';
 import {LLVMIrBackendOptions} from './ir.interfaces.js';
+import type {LeanCOptions} from './lean-c.interfaces.js';
 import {OptPipelineBackendOptions, OptPipelineOutput} from './opt-pipeline-output.interfaces.js';
 import {YulBackendOptions} from './yul.interfaces.js';
 
@@ -117,6 +118,7 @@ export type CompilationRequestOptions = {
         produceHaskellCore?: boolean;
         produceHaskellStg?: boolean;
         produceHaskellCmm?: boolean;
+        produceLeanC?: LeanCOptions | null;
         produceClojureMacroExp?: boolean;
         produceYul?: YulBackendOptions | null;
         cmakeArgs?: string;
@@ -216,6 +218,7 @@ export type CompilationResult = {
     haskellCoreOutput?: ResultLine[];
     haskellStgOutput?: ResultLine[];
     haskellCmmOutput?: ResultLine[];
+    leanCOutput?: ResultLine[];
 
     clojureMacroExpOutput?: ResultLine[];
 
diff --git a/types/compilation/lean-c.interfaces.ts b/types/compilation/lean-c.interfaces.ts
new file mode 100644
index 000000000..d2a72b31c
--- /dev/null
+++ b/types/compilation/lean-c.interfaces.ts
@@ -0,0 +1,27 @@
+// Copyright (c) 2026, Compiler Explorer Authors
+// All rights reserved.
+//
+// Redistribution and use in source and binary forms, with or without
+// modification, are permitted provided that the following conditions are met:
+//
+//     * Redistributions of source code must retain the above copyright notice,
+//       this list of conditions and the following disclaimer.
+//     * Redistributions in binary form must reproduce the above copyright
+//       notice, this list of conditions and the following disclaimer in the
+//       documentation and/or other materials provided with the distribution.
+//
+// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+// AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+// IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+// ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE
+// LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
+// CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+// SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+// INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+// CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+// ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+// POSSIBILITY OF SUCH DAMAGE.
+
+export type LeanCOptions = {
+    'clang-format': boolean;
+};
diff --git a/types/compiler.interfaces.ts b/types/compiler.interfaces.ts
index 6a9557b56..8aabe4bd1 100644
--- a/types/compiler.interfaces.ts
+++ b/types/compiler.interfaces.ts
@@ -103,6 +103,7 @@ export type CompilerInfo = {
     supportsHaskellCoreView?: boolean;
     supportsHaskellStgView?: boolean;
     supportsHaskellCmmView?: boolean;
+    supportsLeanCView?: boolean;
     supportsClojureMacroExpView?: boolean;
     supportsYulView?: boolean;
     supportsCfg?: boolean;
diff --git a/types/languages.interfaces.ts b/types/languages.interfaces.ts
index eb4f9c067..a01713d20 100644
--- a/types/languages.interfaces.ts
+++ b/types/languages.interfaces.ts
@@ -72,6 +72,7 @@ export type LanguageKey =
     | 'julia'
     | 'javascript'
     | 'kotlin'
+    | 'lean'
     | 'llvm'
     | 'llvm_mir'
     | 'mlir'
diff --git a/views/templates/panes/compiler.pug b/views/templates/panes/compiler.pug
index 7fa23f8c1..ccb919b38 100644
--- a/views/templates/panes/compiler.pug
+++ b/views/templates/panes/compiler.pug
@@ -64,6 +64,7 @@ mixin newPaneButton(classId, text, title, icon)
         +newPaneButton("view-haskellCore", "GHC Core", "Show GHC Core Intermediate Representation", "fas fa-water")
         +newPaneButton("view-haskellStg", "GHC STG", "Show GHC STG Intermediate Representation", "fas fa-water")
         +newPaneButton("view-haskellCmm", "GHC Cmm", "Show GHC Cmm Intermediate Representation", "fas fa-water")
+        +newPaneButton("view-leanC", "Lean C Output", "Show generated Lean C output", "fas fa-align-center")
         +newPaneButton("view-clojuremacroexp", "Clojure Macro Expansion", "Show Clojure macro expansion", "fas fa-arrows-alt")
         +newPaneButton("view-yul", "Yul (Solidity IR)", "Show Solidity Intermediate Representation", "fas fa-align-center")
         +newPaneButton("view-gccdump", "GCC Tree/RTL", "Show GCC Tree/RTL dump", "fas fa-tree")
diff --git a/views/templates/panes/leanc.pug b/views/templates/panes/leanc.pug
new file mode 100644
index 000000000..a5ef53594
--- /dev/null
+++ b/views/templates/panes/leanc.pug
@@ -0,0 +1,10 @@
+#leanC
+  .top-bar.btn-toolbar.bg-light(role="toolbar")
+    include ../../font-size
+    .btn-group.btn-group-sm.options(role="group" aria-label="Panel options")
+      .input-group.input-group-sm.mb-auto
+        .button-checkbox
+          button.btn.btn-sm.btn-light.clang-format(type="button" title="Apply clang-format to output" data-bind="clang-format" aria-pressed="true" aria-label="Apply clang-format")
+            span Apply clang-format
+          input.d-none(type="checkbox" checked=true)
+  .monaco-placeholder
diff --git a/views/templates/templates.pug b/views/templates/templates.pug
index f2bb82236..5e40b407a 100644
--- a/views/templates/templates.pug
+++ b/views/templates/templates.pug
@@ -20,6 +20,8 @@ mixin monacopane(id)
 
   include panes/pp
 
+  include panes/leanc
+
   include panes/ir
 
   include panes/clangir