Lean 4 formalizations of proofs from Stephen Abbott's Understanding Analysis textbook

The Complex Number Game. Make the complex numbers in Lean.

Automata theory in Lean

Formalisms Every Computer Scientist Should Know (course at ISTA)

Formalisms Every Computer Scientist Should Know course at ISTA 2023

Printable (A4) overview of tactics in Lean 4 for beginners

Convex optimization modeling in Lean 4

How to read Lean

Declarative binary reading and writing: bit-level, symmetric, serialization/deserialization

A GPT-2 style transformer language model implemented from scratch in Rust for educational purposes.

Example formalization of Game Theoretic concepts in Lean

Generating structured data from arbitrary, unstructured input.

🧸 A Hugo theme based on »Bear Blog«. Free, no-nonsense, super-fast blogging. This theme now includes a dark color scheme to support dark mode 🦉 ⬛️!

Lean Companion to the Category Theory in Context textbook by Emily Riehl

This formalization uses the De Bruijn indices, the objective is to formalize the Church-Rosser theorem

Natural language tactics to teach mathematics using Lean 4

Verified Rust for low-level systems code

Bandit algorithms in Lean

Formalization of Markov Chain Monte Carlo in Lean 4

Mathematical terms, definitions, and propositions in as many languages as possible

A template for blueprint-driven formalization projects in Lean.

plasTeX is a Python package that processes LaTeX documents into an XML-DOM-like object which can be used to generate various types of output.

plasTeX plugin to build formalization blueprints.

Formalization of Mathematical Logic

A menagerie of cute implementations of modern typechecking algorithms