Computerized proof system on the web

Supervisionary: a proof-checking system for HOL

How to use KeYmaera X as a library in a Scala code base.

Quite optimized Agda prime numbers generator

Learning how to use the Lean theorem prover

Schrödinger's hats: a puzzle about parities and permutations

Four color theorem, Guthrie, Kempe, Tait and other people and stuff

Step-by-step proof for equivalence in propositional logic and ND prover for first-order logic.

microk8s based ml cluster

Type Theory course ; Master's Degree in Computer Science @ UniPD

Step-by-step small or medium-sized projects in Lean

Automated mathematical theorem formulation deduced from a provided set of axioms. Builds upon the HRL theorem generator.

Solving the mini Rubik (2x2) in Coq

Contains the code from the book "Modelling logic games and puzzles in First Order Logic" https://link.springer.com/book/10.1007/978-3-030-62547-4

A exercise on theorem proving, design and correctness of a floating point adder in ACL2

Formal verification of GT-SMDN framework in Lean 4. 53 theorems formalised, 28 complete proofs. Companion to 'Protecting Critical Infrastructure' book.

A program that verifies proofs in the F0 proof system

A graphical interactive proof assistant designed for education. My contributions: applying rules by elimination, proofs by induction, proofs by cases, multi-axiom element and misc css styling. Honours report grade: 76% 🎉

📖 Verified Functional Programming in Agda

A proof of the Pigeonhole principle. The Pigeonhole principle is a fundamental theorem that is used widely in Computer Science and Combinatorics, it asserts that if you put n things into m containers, and n > m, then at least one of the containers contains more than one thing.