Visual Studio Code Extension and Language Server Protocol for Coq
-
Updated
Jun 5, 2024 - OCaml
Visual Studio Code Extension and Language Server Protocol for Coq
A graphical web application for interactive theorem proving in Charles Peirce's alpha existential graph system.
My personal repository of formally verified mathematics.
[WIP] A formalised proof of a generalised Carleson's Theorem in the Lean proof assistant.
A formalised proof of Fermat's Last Theorem for exponent 3 in the Lean proof assistant.
Convex optimization modeling in Lean 4
Cicada Language (PLCT little team)
Cicada Language (solo version)
An interactive theorem prover based on lambda-tree syntax
LLMs + Lean, on your laptop or in the cloud
An open source graphical proof construction assistant for the creation of Natural Deduction proofs.
LeanInk is a command line helper tool for Alectryon which aims to ease the integration of Lean 4.
VirtualSlate is an in deveopment proof of concept for VR graphical interactive theorem proving with natural deduction.
A semester project for an introduction to interactive theorem proving using LEAN4 language and Mathlib library
Bringsjordian Natural Deduction soundness wrt truth in the Calculus of Constructions
Experiments with interactive theorem provers, LLMs and formal systems
Online maths contests powered by interactive theorem provers
Proof assistant created in the Plugin Oriented Programming paradigm
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."