Lean to .NET

Prove a function in Lean 4, call it from C#, and see the proofs behind every call.

This is the editor half of lean-to-dot-net. Its compiler, lean2il, re-checks a Lean project with Tenet, an independent Lean kernel, compiles the definitions you mark with @[export] to a .NET assembly, and writes the documentation from the Lean. This extension builds it for you and puts what was proved wherever you are looking.

What it does

In C#. Every call to a compiled function carries a lens, proved in Lean, 9 theorems, re-checked by Tenet, that opens the Lean definition. Hover it for the signatures, the docstring, the proved examples and the theorems, each a link to its line. Type Proven. for completions that say what is proved about each method.

In Lean. A lens over each @[export] definition gives the C# signature it became and how many theorems and replayed examples stand behind it. A lens over each documented theorem names the .NET methods whose docs it appears in; over a proved example, the C# call and the value it returned.

The Proofs view. An Activity Bar view lists each assembly with Tenet's verdict, each compiled function, its proved examples (copy one as a C# call) and its theorems (hover for the statement and the axioms under it, open it in LeanViz). Click anything to go to the Lean.

The Proof Dashboard. One page per assembly: the verdict, the counts, and for each function its signatures, its examples with a check for each one replayed on the IL, and every theorem with its statement and the axioms it rests on.

Building. Lean to .NET: Build .NET Assembly (or the package icon over a Lean file) runs lake build and lean2il in its own terminal. Lean's errors, lean2il's refusals and anything Tenet rejects land in the Problems panel on the line they are about. Turn on lean2dotnet.buildOnSave to rebuild on every save.

Getting started. A walkthrough on the Welcome page goes from installing Lean to calling a proved function from C#. Type export in a Lean file for a snippet of an exported definition with its docstring, or proved-example for an example lean2il will turn into a tested C# call.

What is Tenet?

Lean checks every proof with its kernel, a small program everything else rests on. Tenet is a second, independent implementation of that kernel, written in C# from the type theory, sharing no code with Lean. It re-checks all of Mathlib. When lean2il builds an assembly, Tenet re-checks every declaration first, and if it rejects anything, nothing is emitted. A proof that two independent kernels accept is one you can trust a little more.

Requirements

The extension brings lean2il and Tenet with it; there is nothing to clone or build. It needs:

• The .NET 10 runtime (or SDK) and Lean 4 (through elan). The first time you build, the extension checks for both and, for whichever is missing, offers a terminal with the official installer's command typed in, ready to run.
• The official Lean 4 extension for Lean syntax and the infoview (recommended, not required).

macOS, Linux and Windows. The compiled assembly works from C#, F# and VB.NET.

Settings

Everything the extension shows comes from the .proof.json lean2il writes beside the assembly, so it is exactly what the last build proved. When the Lean has changed since, or the last build failed, the status bar, the lenses and the dashboard say the information is from the last successful build.