formal-proofs
There are 59 repositories under formal-proofs topic.
leanprover-community/mathlib3
Lean 3's obsolete mathematical components library: please use mathlib4
niltok/magic-in-ten-mins
十分钟魔法练习
statebox/idris-ct
formally verified category theory library
LogicalAtomist/principia
The Principia Rewrite
coq-community/hydra-battles
Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]
aripiprazole/rinha
🧪 | Rinha de Backend Lean4
mo271/FormalBook
Formalizing "Proofs from THE BOOK"
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.
duckki/lean-quantum
Formalized quantum computing in Lean theorem prover
Matafou/LibHyps
A Coq library providing tactics to deal with hypothesis
appliedfm/vstyle
A style guide for Coq
RiccardoBiosas/LeanGPT
Experiments with interactive theorem provers, LLMs and formal systems
SKolodynski/IsarMathLib
IsarMathLib is a library of formalized mathematics for Isabelle/ZF.
expln/metamath-lamp
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).
xamidi/pmGenerator
An exhaustive condensed detachment formal proof generator for Hilbert systems in proof theory.
acorrenson/automatik
A library of formalized automaton algorithms
PragmaTwice/TNT
some simple&naive formal proof of trivial Number Theory, using Agda/Coq, just to practice skills
dtumad/lean-crypto-formalization
Library for formalizing cryptography proofs in Lean 3 (Deprecated)
pitmonticone/LeanInVienna2024
Repository hosting resources for the "Lean Tutorial in Vienna" at TU Wien from September 18 to 20, 2024.
BSI-Bund/CafeOBJ-PACE
CafeOBJ proof of Key Secrecy of PACE with OTS/CafeOBJ.
Zeta611/ebproofx
ebproof extended
Bram-Hub/aris-java
Aris: a logic engine/formal proof interface; 2nd generation, successor to the C version of Aris.
liyang/thesis
Compiling Concurrency Correctly—Verifying Software Transactional Memory
logicalhacking/Featherweight_OCL
Local mirror of Featherweight OCL entry of the Archive of Formal Proofs (AFP).
pitmonticone/FLT3
A formalised proof of Fermat's Last Theorem for exponent 3 in the Lean proof assistant.
bryangingechen/lean-matroids
matroids in lean
jcpaik/erdos-tuza-valtr
A formal verification of a mathematics/combinatorics paper "On the Erdős-Tuza-Valtr Conjecture"
joonazan/justified-type-inference
An implementation of Algorithm W in Idris with a complete proof
Hacker-Code-J/Cryptol-CraftCodeLab
Mastering the Art of Cryptol Programming
hvanz/PaxosInPluscal
Paxos algorithm specified and proved in TLA+/PlusCal, with separate processes and invariants for proposers and acceptors.
ata-keskin/martingales
A Formalization of Martingales using Isabelle/HOL
pitmonticone/FLT
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
pthariensflame/agda-fumulas
An exploration of fumulas in Agda—a new perspective on ring theory