Stars
Lean 4 port of Iris, a higher-order concurrent separation logic framework
LeanHammer is an automated reasoning tool for Lean that brings together multiple proof search and reconstruction techniques and combines them into one tool.
Definitional implementation of Cedar language and utilities for DRT
Lean 4 kernel / 'external checker' written in Lean 4
Lean 4 programming language and theorem prover
Public reference documents for the SMT-LIB standard
Tactics for discharging Lean goals into SMT solvers.
cvc5 is an open-source automatic theorem prover for Satisfiability Modulo Theories (SMT) problems.
A Foreign Function Interface (FFI) to cvc5 solver in Lean.