leanprover-community/mathlib3 📦

Lean 3's obsolete mathematical components library: please use mathlib4

Language: Lean - Size: 213 MB - Last synced at: 4 days ago - Pushed at: 12 months ago - Stars: 1,667 - Forks: 294

awslabs/AutoCorrode

Verification infrastructure for the Isabelle/HOL interactive proof assistant

Language: Isabelle - Size: 387 KB - Last synced at: 20 days ago - Pushed at: about 1 month ago - Stars: 37 - Forks: 5

math-comp/algebra-tactics

Ring, field, lra, nra, and psatz tactics for Mathematical Components

Language: Coq - Size: 292 KB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 33 - Forks: 3

TOTBWF/refinery

⛏️ A refinement proof framework for haskell

Language: Haskell - Size: 142 KB - Last synced at: 3 days ago - Pushed at: about 2 years ago - Stars: 69 - Forks: 3

math-comp/mczify

Micromega tactics for Mathematical Components

Language: Coq - Size: 106 KB - Last synced at: 2 months ago - Pushed at: 6 months ago - Stars: 25 - Forks: 8

uwplse/PUMPKIN-PATCH

Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker

Language: OCaml - Size: 1.73 MB - Last synced at: 9 days ago - Pushed at: 11 months ago - Stars: 51 - Forks: 2

dtumad/lean-crypto-formalization

Library for formalizing cryptography proofs in Lean 3 (Deprecated)

Language: Lean - Size: 2.13 MB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 7 - Forks: 0

proof-tree-builder/proof-tree-builder.github.io

A web-based graphical proof assistant for LK and Hoare logic.

Language: JavaScript - Size: 5.39 MB - Last synced at: almost 2 years ago - Pushed at: over 2 years ago - Stars: 24 - Forks: 2

owings1/pytableaux

multi-logic proof generator

Language: Python - Size: 13 MB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 8 - Forks: 0

wenkokke/AutoInAgda 📦

Proof automation – for Agda, in Agda.

Language: Agda - Size: 1.11 MB - Last synced at: about 2 years ago - Pushed at: almost 5 years ago - Stars: 38 - Forks: 7

wenkokke/swillprover 📦

a linear logic prover based on Naoyuki Tamura's llprover that works under SWI Prolog

Language: Prolog - Size: 11.7 KB - Last synced at: about 2 years ago - Pushed at: over 6 years ago - Stars: 9 - Forks: 1

marnix/zigmmverify

Language: Zig - Size: 250 KB - Last synced at: about 2 years ago - Pushed at: over 3 years ago - Stars: 10 - Forks: 0