← All repos

equational_theories

A project to map out the relations between different equational theories of Magmas.

GitHubteorth.github.io/equational_theories/
Browse cluster: Lean4 Formal Verification & Cryptography →
1,777commits
76contributors
17languages

Tech stack & purpose

The equational_theories project maps relationships between different equational theories of magmas using computational and formal methods. It uses the Lean proof assistant to formalize refutations of false implications between equations, leveraging finite magma counterexamples discovered through automated tools including Vampire, Mace4, and Z3. The tech stack includes Lean for formal verification, Haskell tools for optimizing magma selection and proof planning, Python and C for counterexample generation and pruning, and Ruby for graph search and implication processing. The project also maintains data on implications proven or refuted across different equation sets, with infrastructure for brute-forcing small magma structures and searching for proofs via equation rewriting and confluence arguments.

Community & reference links

Languages

Lean
38.7%
C
38.4%
TeX
9.4%
Python
6.8%
JavaScript
3.3%
Ruby
1.4%
HTML
0.9%
Haskell
0.5%
Shell
0.2%
Elm
0.2%
CSS
0.1%
TypeScript
0.0%
PowerShell
0.0%
Nix
0.0%
Batchfile
0.0%
SCSS
0.0%
Perl
0.0%

Contributors (top 30 of 76)