My personal repository of formally verified mathematics.
-
Updated
Dec 23, 2024 - Coq
#
interactive-theorem-proving
Here are 39 public repositories matching this topic...
Visual Studio Code Extension and Language Server Protocol for Coq
-
Updated
Dec 19, 2024 - OCaml
Cicada Language (solo version)
language programming-language dependent-types repl type-theory type-system cicada prover interactive-theorem-proving theorem-prover dependent-record-types dependent-type-theory
-
Updated
Dec 25, 2024 - TypeScript
Cicada Language (PLCT little team)
language programming-language dependent-types repl type-theory type-system cicada prover interactive-theorem-proving theorem-prover dependent-record-types dependent-type-theory
-
Updated
Dec 25, 2024 - TypeScript
An interactive theorem prover based on lambda-tree syntax
-
Updated
Nov 27, 2024 - OCaml
LeanInk is a command line helper tool for Alectryon which aims to ease the integration of Lean 4.
-
Updated
Jul 18, 2024 - Lean
Convex optimization modeling in Lean 4
-
Updated
May 31, 2024 - Lean
A fast, easy-to-use ring solver for agda with step-by-step solutions
-
Updated
Mar 12, 2022 - Agda
An experimental implementation of homotopy type theory in the interactive proof assistant Isabelle
-
Updated
Nov 30, 2022 - Standard ML
The Slate Interactive Theorem Prover
web-app collaboration proof-assistant mathematical-expressions mathematical-logic formal-mathematics interactive-theorem-proving
-
Updated
Jan 9, 2023 - TypeScript
Experiments with interactive theorem provers, LLMs and formal systems
math interactive-theorem-proving theorem-prover ai-agents formal-proofs lean-theorem-prover ai-assisted-development gpt-3 llm chatgpt langchain
-
Updated
Jul 10, 2023 - Coq
An open source graphical proof construction assistant for the creation of Natural Deduction proofs.
-
Updated
Feb 3, 2024 - TypeScript
A graphical web application for interactive theorem proving in Charles Peirce's alpha existential graph system.
typescript interactive-theorem-proving vite existential-graphs charles-sanders-peirce charles-peirce
-
Updated
Dec 22, 2024 - TypeScript
Repository hosting resources for the "Lean Tutorial in Vienna" at TU Wien from September 18 to 20, 2024.
tutorial research logic mathematics proof-assistant lean formal-methods formal-mathematics interactive-theorem-proving tu-wien formal-proofs formalisation leanprover lean4 formalized-mathematics formalisation-mathematics
-
Updated
Oct 2, 2024 - Lean
A dependent type theory logic for Isabelle
dependent-types proof-assistant type-theory isabelle interactive-theorem-proving logical-framework dependent-type-theory
-
Updated
Feb 8, 2021 - Standard ML
HLM mathematical library for the Slate interactive theorem prover
web-app mathematics collaboration proof-assistant mathematical-expressions mathematical-logic formal-mathematics interactive-theorem-proving
-
Updated
Nov 5, 2022 - Shell
A formalised proof of Fermat's Last Theorem for exponent 3 in the Lean proof assistant.
algebra mathematics proof-assistant lean formal-methods formalization number-theory formal-mathematics interactive-theorem-proving theorem-prover formal-proofs mathematical-programming lean4
-
Updated
Aug 21, 2024 - TeX
VirtualSlate is an in deveopment proof of concept for VR graphical interactive theorem proving with natural deduction.
-
Updated
Dec 9, 2023 - GDScript
Improve this page
Add a description, image, and links to the interactive-theorem-proving topic page so that developers can more easily learn about it.
Add this topic to your repo
To associate your repository with the interactive-theorem-proving topic, visit your repo's landing page and select "manage topics."