Visual Studio Code Extension and Language Server Protocol for Coq
-
Updated
May 31, 2024 - OCaml
Visual Studio Code Extension and Language Server Protocol for Coq
An interactive theorem prover based on lambda-tree syntax
LeanInk is a command line helper tool for Alectryon which aims to ease the integration of Lean 4.
My personal repository of formally verified mathematics.
Cicada Language (PLCT little team)
Cicada Language (solo version)
An experimental implementation of homotopy type theory in the interactive proof assistant Isabelle
A fast, easy-to-use ring solver for agda with step-by-step solutions
Convex optimization modeling in Lean 4
Experiments with interactive theorem provers, LLMs and formal systems
A dependent type theory logic for Isabelle
A formalised proof of Fermat's Last Theorem for exponent 3 in the Lean proof assistant.
HLM mathematical library for the Slate interactive theorem prover
The Slate Interactive Theorem Prover
Recopilación de cursos de razonamiento automático.
Math in XO
Natural deduction proof assistant
LLMs + Lean, on your laptop or in the cloud
Add a description, image, and links to the interactive-theorem-proving topic page so that developers can more easily learn about it.
To associate your repository with the interactive-theorem-proving topic, visit your repo's landing page and select "manage topics."