Lean 4 programming language and theorem prover

The math library of Lean 4

An experimental library for Cubical Agda

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

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

Master programming by recreating your favorite technologies from scratch.

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

HoTTEST Summer School materials