GitHub topics: interactive-theorem-proving
ejgallego/coq-lsp
Visual Studio Code Extension and Language Server Protocol for Rocq / Coq
Language: OCaml - Size: 29.6 MB - Last synced at: 7 days ago - Pushed at: 7 days ago - Stars: 170 - Forks: 43

stepchowfun/proofs
My personal repository of formally verified mathematics.
Language: Coq - Size: 1.28 MB - Last synced at: 17 days ago - Pushed at: 3 months ago - Stars: 299 - Forks: 14

leanprover/LeanInk 📦
LeanInk is a command line helper tool for Alectryon which aims to ease the integration of Lean 4.
Language: Lean - Size: 1.23 MB - Last synced at: 5 days ago - Pushed at: 11 months ago - Stars: 61 - Forks: 16

RAIRLab/lazyslate
An open source graphical proof construction assistant for the creation of Natural Deduction proofs.
Language: TypeScript - Size: 175 KB - Last synced at: 6 days ago - Pushed at: over 1 year ago - Stars: 18 - Forks: 0

data61/PSL
Language: Isabelle - Size: 175 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 68 - Forks: 9

abella-prover/abella
An interactive theorem prover based on lambda-tree syntax
Language: OCaml - Size: 4.51 MB - Last synced at: 26 days ago - Pushed at: 26 days ago - Stars: 95 - Forks: 19

RAIRLab/Peirce-My-Heart
A graphical web application for interactive theorem proving in Charles Peirce's alpha existential graph system.
Language: TypeScript - Size: 7.28 MB - Last synced at: 6 days ago - Pushed at: 5 months ago - Stars: 12 - Forks: 0

pitmonticone/LeanCHANGE
Repository hosting the resources for the Lean demo session of my talk presented at the weekly research seminar on CHallenges in ANalysis and GEometry (CHANGE) at the University of Trento on February 11, 2025.
Language: Lean - Size: 1.23 MB - Last synced at: 8 days ago - Pushed at: 4 months ago - Stars: 3 - Forks: 0

Seagat2011/Anthropic-Claude-Mathematical-Proof-Solver-
An elegant Anthropic Claude designed Mathematical Proof Solver, written in Javascript, HTML, and CSS.
Language: JavaScript - Size: 190 KB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 0 - Forks: 0

SReichelt/slate
The Slate Interactive Theorem Prover
Language: TypeScript - Size: 7.5 MB - Last synced at: 3 months ago - Pushed at: over 2 years ago - Stars: 24 - Forks: 2

HOLMS-lib/HOLMS
HOL-Light Library for Modal Systems
Language: OCaml - Size: 212 KB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 1 - Forks: 0

h2-math/coq-nahas-tutorial
Coq Tutorial from Mike Nahas's repo at https://github.com/mdnahas/mdnahas.github.io/doc/nahas_tutorial.v
Language: HTML - Size: 216 KB - Last synced at: 3 months ago - Pushed at: 5 months ago - Stars: 0 - Forks: 0

pitmonticone/LeanInVienna2024
Repository hosting resources for the "Lean Tutorial in Vienna" at TU Wien from September 18 to 20, 2024.
Language: Lean - Size: 1.58 MB - Last synced at: 4 days ago - Pushed at: 5 months ago - Stars: 9 - Forks: 2

cicada-lang/cicada-plct
Cicada Language (PLCT little team)
Language: TypeScript - Size: 2.51 MB - Last synced at: 6 months ago - Pushed at: 6 months ago - Stars: 92 - Forks: 7

cicada-lang/cicada-solo
Cicada Language (solo version)
Language: TypeScript - Size: 6.83 MB - Last synced at: 6 months ago - Pushed at: 6 months ago - Stars: 128 - Forks: 5

HOLMS-lib/holms-lib.github.io
HOL Light Library for Modal Systems
Size: 96.7 KB - Last synced at: 6 months ago - Pushed at: 6 months ago - Stars: 0 - Forks: 0

verified-optimization/CvxLean
Convex optimization modeling in Lean 4
Language: Lean - Size: 22.5 MB - Last synced at: 6 months ago - Pushed at: about 1 year ago - Stars: 41 - Forks: 4

RAIRLab/VirtualSlate
VirtualSlate is an in deveopment proof of concept for VR graphical interactive theorem proving with natural deduction.
Language: GDScript - Size: 68.8 MB - Last synced at: 6 days ago - Pushed at: over 1 year ago - Stars: 2 - Forks: 0

pitmonticone/carleson Fork of fpvandoorn/carleson
[WIP] A formalised proof of a generalised Carleson's Theorem in the Lean proof assistant.
Language: TeX - Size: 1.31 MB - Last synced at: 12 months ago - Pushed at: 12 months ago - Stars: 0 - Forks: 0

James-Oswald/Lazycore
Bringsjordian Natural Deduction soundness wrt truth in the Calculus of Constructions
Language: Lean - Size: 17.6 KB - Last synced at: 6 days ago - Pushed at: almost 2 years ago - Stars: 1 - Forks: 0

jaalonso/Matematicas_en_Lean
Matemáticas en Lean
Language: Lean - Size: 354 KB - Last synced at: 2 months ago - Pushed at: almost 2 years ago - Stars: 4 - Forks: 1

pitmonticone/FLT3 Fork of riccardobrasca/flt3
A formalised proof of Fermat's Last Theorem for exponent 3 in the Lean proof assistant.
Language: TeX - Size: 550 KB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 1 - Forks: 1

jaycech3n/Isabelle-HoTT
An experimental implementation of homotopy type theory in the interactive proof assistant Isabelle
Language: Standard ML - Size: 405 KB - Last synced at: 3 months ago - Pushed at: over 2 years ago - Stars: 34 - Forks: 3

oisdk/agda-ring-solver 📦
A fast, easy-to-use ring solver for agda with step-by-step solutions
Language: Agda - Size: 6.07 MB - Last synced at: about 1 year ago - Pushed at: about 3 years ago - Stars: 38 - Forks: 4

shangsuru/concrete-semantics
Solutions to the problems in the book Concrete Semantics by Gerwin Klein and Tobias Nipkow
Language: Isabelle - Size: 313 KB - Last synced at: about 1 year ago - Pushed at: over 2 years ago - Stars: 0 - Forks: 0

RiccardoBiosas/LeanGPT
Experiments with interactive theorem provers, LLMs and formal systems
Language: Coq - Size: 7.81 KB - Last synced at: about 1 year ago - Pushed at: almost 2 years ago - Stars: 12 - Forks: 2

James-Oswald/SlateCore
A Core for Slate Applications
Language: C++ - Size: 78.1 KB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0

sumantchopdata/intro_to_automated_proof_checking
A semester project for an introduction to interactive theorem proving using LEAN4 language and Mathlib library
Language: Lean - Size: 33.2 KB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0

SReichelt/slate-hlm
HLM mathematical library for the Slate interactive theorem prover
Language: Shell - Size: 1.85 MB - Last synced at: almost 2 years ago - Pushed at: over 2 years ago - Stars: 2 - Forks: 1

mathsforces/mathsforces
Online maths contests powered by interactive theorem provers
Language: Lean - Size: 10.7 KB - Last synced at: about 2 years ago - Pushed at: about 2 years ago - Stars: 0 - Forks: 0

jaalonso/Explorando-con-Lean
Explorando formalizaciones con Lean
Language: Lean - Size: 37.1 KB - Last synced at: 2 months ago - Pushed at: almost 3 years ago - Stars: 1 - Forks: 0

jaycech3n/Isabelle-Spartan 📦
A dependent type theory logic for Isabelle
Language: Standard ML - Size: 361 KB - Last synced at: about 2 years ago - Pushed at: over 4 years ago - Stars: 6 - Forks: 1

shisharka/interactive_deduction
Natural deduction proof assistant
Language: C++ - Size: 919 KB - Last synced at: over 2 years ago - Pushed at: over 7 years ago - Stars: 2 - Forks: 0

jaalonso/Cursos_de_RA
Recopilación de cursos de razonamiento automático.
Size: 15.6 KB - Last synced at: 2 months ago - Pushed at: almost 3 years ago - Stars: 0 - Forks: 0

jaalonso/DAO_con_Lean
DAO (Demostración Asistida por Ordenador) con Lean
Language: Lean - Size: 1.92 MB - Last synced at: 2 months ago - Pushed at: almost 3 years ago - Stars: 0 - Forks: 0

Larch-Team/Larch
Proof assistant created in the Plugin Oriented Programming paradigm
Language: Python - Size: 15.3 MB - Last synced at: 25 days ago - Pushed at: 25 days ago - Stars: 0 - Forks: 1

jaycech3n/Pure_Logic
Isabelle's Pure logic, directly extended to FOL/HOL
Language: Isabelle - Size: 5.86 KB - Last synced at: 3 months ago - Pushed at: about 6 years ago - Stars: 1 - Forks: 0

cpiemontese/tlc-elpi
Interactive theorem proving in ELPI
Size: 344 KB - Last synced at: about 2 years ago - Pushed at: over 6 years ago - Stars: 2 - Forks: 0

cluesurfback/math
Math in XO
Size: 22.5 KB - Last synced at: 2 months ago - Pushed at: almost 4 years ago - Stars: 0 - Forks: 0

rizaldialbert/vhdl-semantics
Language: Isabelle - Size: 2.34 MB - Last synced at: about 2 years ago - Pushed at: over 4 years ago - Stars: 0 - Forks: 0
