A Proof-oriented Programming Language
Visual Studio Code Extension and Language Server Protocol for Rocq / Coq [maintainers=@gbdrt,@SkySkimmer,@tabareau]
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.
Convex optimization modeling in Lean 4
Cicada Language (PLCT little team)
Cicada Language (solo version)
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
Repository hosting resources for the "Lean Tutorial in Vienna" at TU Wien from September 18 to 20, 2024.
The Slate Interactive Theorem Prover
Experiments with interactive theorem provers, LLMs and formal systems
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
Proof assistant created in the Plugin Oriented Programming paradigm
A dependent type theory logic for Isabelle
An elegant Anthropic Claude designed Mathematical Proof Solver, written in Javascript, HTML, and CSS.
Lean 4 workshop: tutorials, proofs, and learning resources
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."