Lean is a functional programming language that makes it easy to write correct

and maintainable code. You can also use Lean as an interactive theorem prover.

Lean programming primarily involves defining types and functions. This allows

your focus to remain on the problem domain and manipulating its data, rather

than the details of programming.

Lean 4 programming language and theorem prover

• UpdatedMar 18, 2025
• Lean

The math library of Lean 4

• UpdatedMar 18, 2025
• Lean

LLMs as Copilots for Theorem Proving in Lean

• UpdatedMar 4, 2025
• C++

Tool for data extraction and interacting with Lean programmatically.

• UpdatedMar 10, 2025
• Python

Lean theorem proving interface which feels like pen-and-paper proofs.

• UpdatedFeb 19, 2025
• TypeScript

Scientific computing in Lean 4

• UpdatedMar 18, 2025
• Lean

Neovim support for the Lean theorem prover

• UpdatedMar 17, 2025
• Lua

The "batteries included" extended library for the Lean programming language and theorem prover

• UpdatedMar 18, 2025
• Lean

Retrieval-Augmented Theorem Provers for Lean

• UpdatedJan 30, 2025
• Python

White-box automation for Lean 4

• UpdatedMar 17, 2025
• Lean

Server to host lean games.

• UpdatedMar 14, 2025
• TypeScript

• UpdatedFeb 28, 2025
• Lean

Lecture notes for a course on writing proofs, on paper and in the Lean proof assistant

• UpdatedDec 9, 2024
• HTML

Theorem Proving in Lean 4

• UpdatedOct 14, 2024
• JavaScript

Tactics for discharging Lean goals into SMT solvers.

• UpdatedMar 14, 2025
• Lean

Natural Number Game

• UpdatedMar 14, 2025
• Lean

Catalog Of Math Problems Formalized In Lean

• UpdatedMar 17, 2025
• Lean

A simple raytracer written in Lean 4

• UpdatedMay 16, 2024
• Lean

Helper toolkit for creating your own Lean 4 UserWidgets

• UpdatedMar 14, 2025
• Lean

llmstep: [L]LM proofstep suggestions in Lean 4.

• UpdatedNov 11, 2023
• Python