#

lean4

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.

Here are 9 public repositories matching this topic...

lean-dojo / LeanCopilot

LLMs as Copilots for Theorem Proving in Lean

machine-learning theorem-proving lean formal-mathematics lean4 llm llm-inference

Updated Feb 17, 2026
C++

GaloisInc / lean4-balance-car

Lean4 port of Arduino balance car controller

lean4

Updated Mar 17, 2021
C++

bollu / lean-to

Jupyter notebook for the Lean4 programming language

lean4

Updated Apr 25, 2022
C++

lecopivo / HouLean

Lean 4 as a scripting language in Houdini

houdini houdini-plugin lean4

Updated Mar 13, 2024
C++

lecopivo / EigenLean

Lean 4 interface to Eigen

eigen3 lean4

Updated Dec 13, 2024
C++

bollu / elide

Elide: Elegant Metamodal Lean4 IDE.

ide text-editor lean4

Updated Feb 12, 2024
C++

alexf91 / lean4-ctypes

FFI for Lean 4

ffi lean lean4

Updated Dec 27, 2023
C++

PolyB / LeanPythonRaw

Raw Lean4 bindings to python C-API

lean4

Updated Jul 11, 2022
C++

LeninYasselTrinidadF / Arkhe

Visualizer for mathlib library inspired in https://github.com/Crispher/MathlibExplorer . The idea is to connect each topic based on standard curricula to each file in mathlib so new code and math topics can be implemented faster.

math graphics formalization mathlib lean4 mathlib4

Updated Apr 7, 2026
C++

Created by Leonardo de Moura

Released 2013

Followers: 42 followers
Repository: leanprover/lean
Website: github.com/topics/lean
Wikipedia: Wikipedia