An experimental library for Cubical Agda

HoTTEST Summer School materials

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

The math library of Lean 4

Lean 4 programming language and theorem prover

《用Rust实现Lua解释器》 / _Build a Lua Interpreter in Rust_

Master programming by recreating your favorite technologies from scratch.

🧮 Path to a free self-taught education in Mathematics!