universal-algebra

The agda-unimath library

The Agda Universal Algebra Library (html docs available at the url below)

Algebraic proof discovery in Agda

The Agda Universal Algebra Library (UALib) is a library of types and programs (theorems and proofs) that formalizes the foundations of universal algebra in dependent type theory using the Agda proof assistant language.

First Order Logic Python Library

Mathematics Distillation Challenge, Equational Theories. Stage 1 cheatsheet and Stage 2 Lean 4 certificate solver for the SAIR Foundation competition.

Small library of concepts in the theory of Constraint Satisfaction Problem and Universal Algebra

Universal algorithm for deterministic resolution of alternating-turn games, based on the Gn/Px/Tz framework and backward induction.

Evolution of Algebraic Terms

Personal website and blog of William DeMeo: formal verification in Agda, universal algebra, and AI tooling for interactive theorem proving. Built with MkDocs Material.

The Agda Universal Algebra Library (html docs available at the url below)

Kernel-checked Lean 4 proof that no infinite simple paramedial quasigroups exist (Loops '03 open problem).

Repository for global spectrum algorithms

Algorithms for generating clones above an algebra that has a majority term.

Formalizing the clone theory in type theory and Agda

Mathematical exploration tool for finite Magmas and equational theories

🦀 Analyze zero-sum games with the Deterministic Solution Algorithm for optimal outcomes, ensuring victory or minimizing loss in complex game scenarios.