51 skills found · Page 1 of 2
rocq-prover / RocqThe Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
FStarLang / FStarA Proof-oriented Programming Language
agda / AgdaAgda is a dependently typed programming language / interactive theorem prover.
stepchowfun / ProofsMy personal repository of formally verified mathematics.
rocq-community / Rocq LspVisual Studio Code Extension and Language Server Protocol for Rocq / Coq [maintainers=@gbdrt,@SkySkimmer,@tabareau]
the-lambda-church / CoquilleInteractive theorem proving with Coq in vim.
jesse-michael-han / Lean GptfInteractive neural theorem proving in Lean
cicada-lang / Cicada SoloCicada Language (solo version)
akissinger / ChypAn interactive theorem prover for string diagrams
abella-prover / AbellaAn interactive theorem prover based on lambda-tree syntax
cicada-lang / Cicada PlctCicada Language (PLCT little team)
jaalonso / Lecturas GLCReadings on computational logic, interactive theorem proving and functional programming.
data61 / PSLNo description available
verified-optimization / CvxLeanConvex optimization modeling in Lean 4
leanprover / LeanInkLeanInk is a command line helper tool for Alectryon which aims to ease the integration of Lean 4.
blanchette / Interactive Theorem Proving 2024Files associated with the course Interactive Theorem Proving at LMU SoSe 2024
oisdk / Agda Ring SolverA fast, easy-to-use ring solver for agda with step-by-step solutions
jaycech3n / Isabelle HoTTAn experimental implementation of homotopy type theory in the interactive proof assistant Isabelle
liamoc / HilbertAn intensely interactive, graphical theorem prover based on natural deduction
SReichelt / SlateThe Slate Interactive Theorem Prover
