Neovim support for the Lean theorem prover
-
Updated
Nov 22, 2024 - Lua
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.
Neovim support for the Lean theorem prover
Readings on computational logic, interactive theorem proving and functional programming.
Ground Zero: Lean 4 HoTT Library
Category Theory & Cobordism Categories in Lean 4
IRC-bot written in Lean (https://leanprover.github.io/)
A decision procedure for the formal system MIU, written in Lean 3.18.4
Repository hosting resources for the "Lean Tutorial in Vienna" at TU Wien from September 18 to 20, 2024.
monoidal categories in the Lean theorem prover
Elaboración de demostraciones con Lean.
a Lean implementation of Jensen's Inequality
DAO (Demostración Asistida por Ordenador) con Lean
Programming language foundations in Lean
Created by Leonardo de Moura
Released 2013