Stars
A comprehensive and searchable database of categories and their properties
SorryDB indexes sorries in public lean repositories
A file-based mirror of the nLab wiki (Markdown+itex2MML format).
Formalization of de Rham cohomologies of a smooth manifold
A collection of formalized statements of conjectures in Lean.
A formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory
computable implementation of real numbers in Lean4
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
Blueprint for the PNT+ Project
Shadertoy for WebGPU compute shaders.
SnapPy is a package for studying the topology and geometry of 3-manifolds, with a focus on hyperbolic structures. It is based on the SnapPea kernel written by Jeff Weeks.
The official repository and issue-tracker for Enigmatica 6
Lean 3's obsolete mathematical components library: please use mathlib4
Building the natural numbers in Lean 3. The original natural number game, now frozen. See README for Lean 4 information.
Syntax highlighting for JS and TS tagged template strings using comments to specify language
Simple attendance registration for universities having pandemics. ("anwesende" is German for "people that are being present".)
📐 Javascript Geometric Algebra Generator for Javascript, c++, c#, rust, python. (with operator overloading and algebraic literals) -
A community-maintained Python framework for creating mathematical animations.
Derived from https://github.com/Syntopia/Fragmentarium/