Logic and Mechanized Reasoning

slides about 6hole-problem

H.O.T.T. using rewriting in Agda

Language Server for Idris2

LaTeX code for a paper on lean's type theory

Formalization of the existence of sphere eversions

A typst wasm plugin to use graphviz directly inside documents

Combinatorial game library in Lean 4

formalization of music theory

Label-based Caliculi for Modal Logic

Formalize Incompleness Theorem Related Results

Formalization of Arithmetization of Mathematics/Metamathematics

Kites of Logics

Formalization of Mathematical Logic

Read-only mirror (from Tardis GitLab) of the University of Edinburgh fork of community-solutions. Contributions are welcome on the GitLab website! (They will not be accepted here)

Welcome to Better Informatics. The student run website for students in the School of Informatics.

Alternative Mizar proof checker (http://mizar.org/) written in Rust

A systems theorem prover

An implementation of the OpenMP directives for Zig

Graphical rewriting for diagrammatic reasoning in monoidal categories in Lean4

CaDiCaL SAT Solver

Some of my Lean proofs

Code related to the Lean verification of the empty hexagon theorem

Identification of cell type-specific differential features in single-cell and spatial omics data

Backdoor attacks in single-cell pretrained models