A Proof-oriented Programming Language
My personal repository of formally verified mathematics.
Visual Studio Code Extension and Language Server Protocol for Rocq / Coq
Cicada Language (solo version)
An interactive theorem prover based on lambda-tree syntax
Cicada Language (PLCT little team)
Convex optimization modeling in Lean 4
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
The Slate Interactive Theorem Prover
Experiments with interactive theorem provers, LLMs and formal systems
An open source graphical proof construction assistant for the creation of Propositional Natural Deduction proofs.
Repository hosting resources for the "Lean Tutorial in Vienna" at TU Wien from September 18 to 20, 2024.
A graphical web application for interactive theorem proving in Charles Peirce's alpha existential graph system.
A formalised proof of Fermat's Last Theorem for exponent 3 in the Lean proof assistant.
A dependent type theory logic for Isabelle
HLM mathematical library for the Slate interactive theorem prover
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."