My personal repository of formally verified mathematics.
-
Updated
Jun 13, 2024 - Coq
My personal repository of formally verified mathematics.
Visual Studio Code Extension and Language Server Protocol for Coq
Cicada Language (solo version)
Cicada Language (PLCT little team)
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.
A fast, easy-to-use ring solver for agda with step-by-step solutions
An experimental implementation of homotopy type theory in the interactive proof assistant Isabelle
Convex optimization modeling in Lean 4
The Slate Interactive Theorem Prover
Experiments with interactive theorem provers, LLMs and formal systems
A graphical web application for interactive theorem proving in Charles Peirce's alpha existential graph system.
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
An open source graphical proof construction assistant for the creation of Natural Deduction proofs.
Natural deduction proof assistant
Interactive theorem proving in ELPI
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."