Can mathematical proof be turned into a puzzle game?

An attempt to formally verify that Dragster cannot be beaten in less than 5.57 seconds.

Research project: directed/modal type theory without the complexity.

Mechanised metatheory experiments

A proof assistant and a dependently-typed language

AirPods liberated from Apple's ecosystem.

A tool for building and visualizing polytopes.

Logical manifestations of topological concepts, and other things, via the univalent point of view.

An interactive Agda tutorial

Latex documentation of our understanding of the synthetic /internal theory of the Zariski-Topos

A mirror for all the links I post on my personal discord server

A formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory

Learn the Agda basics in three 2-hour sessions.

Seventeen tone (per octave) piano

Official OpenDyslexic browser extension

Viewer for cellular automaton on the t{3,7} (hyperbolic soccerball) tiling of the hyperbolic plane (the one used by HyperRogue). (uses Python 3.10.1)

An experimental library for Cubical Agda