ejgallego/coq-lsp

Visual Studio Code Extension and Language Server Protocol for Rocq / Coq

Language: OCaml - Size: 30.2 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 172 - Forks: 43

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: 6 days ago - Pushed at: 11 months ago - Stars: 62 - Forks: 16

stepchowfun/proofs

My personal repository of formally verified mathematics.

Language: Coq - Size: 1.28 MB - Last synced at: 25 days ago - Pushed at: 3 months ago - Stars: 299 - Forks: 14

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: about 1 month ago - Pushed at: about 1 month 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: 5 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: 4 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: 5 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: 7 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: 3 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: over 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: 3 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: 3 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: 3 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: about 1 month ago - Pushed at: about 1 month 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: about 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