formal-proofs | Topic | Ecosyste.ms: Repos

Topic: "formal-proofs"

leanprover-community/mathlib3 📦

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

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

niltok/magic-in-ten-mins

十分钟魔法练习

Language: HTML - Size: 31.5 MB - Last synced at: 2 months ago - Pushed at: almost 2 years ago - Stars: 800 - Forks: 38

statebox/idris-ct

formally verified category theory library

Language: Idris - Size: 376 KB - Last synced at: about 1 month ago - Pushed at: almost 5 years ago - Stars: 263 - Forks: 23

LogicalAtomist/principia

The Principia Rewrite

Language: TeX - Size: 12.1 MB - Last synced at: 10 days ago - Pushed at: 4 months ago - Stars: 222 - Forks: 5

rocq-community/hydra-battles

Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]

Language: Coq - Size: 20.9 MB - Last synced at: 9 days ago - Pushed at: 4 months ago - Stars: 75 - Forks: 12

data61/PSL

Language: Isabelle - Size: 175 MB - Last synced at: 29 days ago - Pushed at: 29 days ago - Stars: 68 - Forks: 9

aripiprazole/rinha

🧪 | Rinha de Backend Lean4

Language: Lean - Size: 11.4 MB - Last synced at: 8 days ago - Pushed at: over 1 year ago - Stars: 64 - Forks: 3

mo271/FormalBook

Formalizing "Proofs from THE BOOK"

Language: TeX - Size: 354 KB - Last synced at: 19 days ago - Pushed at: 6 months ago - Stars: 59 - Forks: 12

Gbury/archsat

A proof-producing SMT/McSat solver, handling polymorphic first-order logic, and using an SMT/McSat core extended using Tableaux, Superposition and Rewriting.

Language: OCaml - Size: 2.14 MB - Last synced at: about 19 hours ago - Pushed at: almost 2 years ago - Stars: 27 - Forks: 5

xamidi/pmGenerator

An exhaustive condensed detachment formal proof generator for Hilbert systems in proof theory.

Language: C++ - Size: 45.2 MB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 21 - Forks: 3

Matafou/LibHyps

A Coq library providing tactics to deal with hypothesis

Language: Coq - Size: 216 KB - Last synced at: 21 days ago - Pushed at: 6 months ago - Stars: 21 - Forks: 3

SKolodynski/IsarMathLib

IsarMathLib is a library of formalized mathematics for Isabelle/ZF.

Language: Isabelle - Size: 154 MB - Last synced at: 17 days ago - Pushed at: 17 days ago - Stars: 18 - Forks: 1

appliedfm/vstyle

A style guide for Coq

Size: 646 KB - Last synced at: about 2 months ago - Pushed at: over 3 years ago - Stars: 18 - Forks: 0

duckki/lean-quantum

Formalized quantum computing in Lean theorem prover

Language: Lean - Size: 196 KB - Last synced at: 10 months ago - Pushed at: about 4 years ago - Stars: 17 - Forks: 4

Metamath-lamp (Lite Assistant for Metamath Proofs) is a GUI-based proof assistant for creating formal mathematical proofs in Metamath that does not require installation (just run it directly using your web browser).

Language: ReScript - Size: 18.9 MB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 16 - Forks: 5

MixedMatched/juniper

A toy formally-specified Computer Algebra library written in Rust and formalized in Lean 4

Language: Rust - Size: 110 KB - Last synced at: 26 days ago - Pushed at: 5 months ago - Stars: 15 - Forks: 1

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

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: 9 days ago - Pushed at: 5 months ago - Stars: 9 - Forks: 2

acorrenson/automatik

A library of formalized automaton algorithms

Language: Coq - Size: 25.4 KB - Last synced at: about 2 months ago - Pushed at: almost 3 years ago - Stars: 9 - Forks: 1

unitb/temporal-logic

Language: Lean - Size: 254 KB - Last synced at: 6 months ago - Pushed at: over 6 years ago - Stars: 9 - Forks: 3

PragmaTwice/TNT

some simple&naive formal proof of trivial Number Theory, using Agda/Coq, just to practice skills

Language: Agda - Size: 8.79 KB - Last synced at: about 2 months ago - Pushed at: over 6 years ago - Stars: 8 - Forks: 1

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

xamidi/mmsolitaire

My contributions to Metamath's mmsolitaire project.

Size: 687 KB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 5 - Forks: 0

Zeta611/ebproofx

ebproof extended

Language: TeX - Size: 789 KB - Last synced at: about 2 months ago - Pushed at: over 1 year ago - Stars: 5 - Forks: 1

BSI-Bund/CafeOBJ-PACE

CafeOBJ proof of Key Secrecy of PACE with OTS/CafeOBJ.

Language: AMPL - Size: 58.6 KB - Last synced at: over 2 years ago - Pushed at: about 4 years ago - Stars: 5 - Forks: 0

unitb/lean-lib

Language: Lean - Size: 305 KB - Last synced at: 10 months ago - Pushed at: over 5 years ago - Stars: 5 - Forks: 0

logicalhacking/Featherweight_OCL

Local mirror of Featherweight OCL entry of the Archive of Formal Proofs (AFP).

Language: Isabelle - Size: 446 KB - Last synced at: 3 months ago - Pushed at: about 3 years ago - Stars: 4 - Forks: 0

Bram-Hub/aris-java Fork of garberlog/ARIS

Aris: a logic engine/formal proof interface; 2nd generation, successor to the C version of Aris.

Language: Java - Size: 14.8 MB - Last synced at: almost 2 years ago - Pushed at: almost 5 years ago - Stars: 4 - Forks: 2

liyang/thesis

Compiling Concurrency Correctly—Verifying Software Transactional Memory

Language: TeX - Size: 367 KB - Last synced at: about 2 years ago - Pushed at: almost 8 years ago - Stars: 4 - Forks: 0

jcpaik/erdos-tuza-valtr

A formal verification of a mathematics/combinatorics paper "On the Erdős-Tuza-Valtr Conjecture"

Language: Lean - Size: 198 KB - Last synced at: 1 day ago - Pushed at: 7 months ago - Stars: 3 - Forks: 0

bryangingechen/lean-matroids

matroids in lean

Language: Lean - Size: 58.6 KB - Last synced at: 6 months ago - Pushed at: over 4 years ago - Stars: 3 - Forks: 1

joonazan/justified-type-inference

An implementation of Algorithm W in Idris with a complete proof

Language: Idris - Size: 41 KB - Last synced at: over 2 years ago - Pushed at: about 6 years ago - Stars: 3 - Forks: 1

hvanz/PaxosInPluscal

Paxos algorithm specified and proved in TLA+/PlusCal, with separate processes and invariants for proposers and acceptors.

Language: TLA - Size: 69.3 KB - Last synced at: 10 days ago - Pushed at: over 6 years ago - Stars: 3 - Forks: 1

pthariensflame/agda-fumulas

An exploration of fumulas in Agda—a new perspective on ring theory

Language: Agda - Size: 185 KB - Last synced at: 10 days ago - Pushed at: 2 months ago - Stars: 2 - Forks: 0

Hacker-Code-J/Cryptol-CraftCodeLab

Mastering the Art of Cryptol Programming

Language: C - Size: 3.91 MB - Last synced at: about 1 month ago - Pushed at: 7 months ago - Stars: 2 - Forks: 0

markpock/fitch-proof-for-propositional-logic

A utility for proofs in the propositional calculus. Currently finished - a way of parsing (most) valid strings in the PC as Sentences which can be added to proofs. Working on a mechanism for machine proof.

Language: Python - Size: 59.6 KB - Last synced at: almost 2 years ago - Pushed at: over 2 years ago - Stars: 2 - Forks: 1