opinionated emoji variation formatter

Formal verification of algorithms using Lean4 and Rocq

AuroExplorer: 亞斯/自閉光譜 AI 社交探索小幫手

Mechanized classifications of 2-groups

nova plugins for forester

Transparent file encryption in git

A purely functional programming language with first class types

Formal proof of the Four Color Theorem [maintainer=@ybertot]

A formalization of System Fω in Agda

Formalizations of Gradually Typed Languages in Agda

Algebraic, staged parsing for OCaml: typed, compositional, and faster than yacc

Agda is a dependently typed programming language / interactive theorem prover.

justfont collaborates with calligrapher Daphne to release Elffont (精靈文), a unique typeface blending Bopomofo phonetic symbols with a mystical "Elvish" style.

Extensions to cubical for categorical logic/type theory

Ongoing Lean formalisation of the proof of Fermat's Last Theorem

Reading group for Cisinski's higher categories and homotopical algebra

Examples of technical drawing with John Hobby's MetaPost language

A Rust/WASM implementation of homotopy.io

A graduate course on formalized mathematics at the Faculty of Mathematics and Physics, University of Ljubljana, Fall semester 2024/25

Formal proofs related to coslice colimits and 2-coherent left adjoints

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

Open Source Continuous File Synchronization

Formalizing the fact that countable choice implies postnikov effectiveness in HoTT

Public-facing information about WITS

formalization of an equivariant cartesian cubical set model of type theory

antifunext