A Proof-oriented Programming Language
My personal repository of formally verified mathematics.
Visual Studio Code Extension and Language Server Protocol for Rocq / Coq [maintainers=@gbdrt,@SkySkimmer,@tabareau]
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
Experiments with interactive theorem provers, LLMs and formal systems
The Slate Interactive Theorem Prover
A curated list of awesome interactive theorem prover frameworks
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.
The open workbench for AI safety, made formal. Turn safety questions into machine-checked Lean proofs — a shared launchpad where researchers and AI agents build provable safety together.
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 formal verification of an abstract SAT solving transition system.
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."