Lean 4 for Software Engineers

Abstract

Lean 4 is best known as a theorem prover for mathematics. It's also a compiled functional language you can build real software with today.

Leangineering is a community for people who use Lean for software engineering and computer science.

Start with the directory of Lean libraries and tools, or read writing about real projects built with them.

1Repos

Awesome Lean Programming is a directory of 382 libraries, tools and projects for building software in Lean.

Recent projects

TodoMVC Maxpetrolheadpb · October 27, 2026paulbutcher/lean-authentication
Lean community style guide (Draft)a2svior · October 21, 2026saviorand/lean-style-guide
Dependabot-ish for Leanpetrolheadpb · October 20, 2026paulbutcher/lean-bump

Built something in Lean? Share it in #projects-and-repos on the Discord.

Browse the repos

2Articles

Sungrow in Lean, part 3carlo_h_ · carlo-hamalainen.net · October 25, 2026
In part 2 we implemented metrics and basic register reads (one at a time). Now we will implement chunked (block) reads since this is more efficient as it involves fewer TCP round trips. At the end, we’ll also try writing to the inverter’s control registers to force the battery to charge and stop.…
Sungrow in Lean, part 2carlo_h_ · carlo-hamalainen.net · October 18, 2026
In part 1 we implemented a simple Modbus TCP library and read a single sensor from the Sungrow inverter. Our next step is to parse the full list of registers so that we can read all the values of interest like real time solar production, battery state of charge, grid draw, etc. YAML and JSON data…
Sungrow in Lean, part 1carlo_h_ · carlo-hamalainen.net · October 16, 2026
What better way to learn Lean, than to implement a bespoke home battery management system? I’m going to do that in this series of blog posts, porting my Go implementation over to Lean4. The UI will naturally use the Lean Datastar SDK that I developed with Valentin Erokhin. Also check out…

Written about Lean? Share it in #blog-posts on the Discord.

All articles

3How this site is built

Theorem 1 (Written in Lean). Every page on this site is a typed HTML value produced by a Lean program.

Proof. Pages are built with lean-html, so a <div> inside a <p> is a compile error. The directory comes from the awesome-lean-programming readme, which the site sanitizes and turns into lean-html nodes as well. Search streams results from the server with Datastar, so there's no frontend build step. Figure 1 shows part of the code.∎

Main.lean

-- the routes this page was served from
route_table Site
  [ home     := "/",
    blog     := "/blog",
    awesome  := "/awesome",
    category := "/awesome/:slug:String" ]

def hero : Node .flow :=
  h1 [ "Lean 4 for Software Engineers" ]

-- what lean-html proves about escaping
#check escape_safe

Lean Infoview

▼ Main.lean:12:0

Html.escape_safe (s : String) (c : Char) : c ∈ (escape s).toList → c ≠ '<' ∧ c ≠ '>' ∧ c ≠ '\"'

Figure 1. Some of the code behind this page. On the right, Lean's infoview shows the theorem lean-html proves about escaping.

The site's code is open source if you want to see how it's done or improve it.

4Community

Most of the conversation happens on the Discord. Beginners and people without a maths background are welcome.

Join the Discord