Formal prime certificates in Lean 4

Formalisations relating to https://mathoverflow.net/q/501066/117945

Disproof of the Aharoni–Korman conjecture

Exceptions to the ABC conjecture in Lean

The (currently unofficial) sublibrary of Mathlib dedicated to additive combinatorics

Course notes for Formalising Mathematics 2025

A silly 4D physics simulation.

Topos theory in lean

Lecture notes from Cambridge maths

The 'Robot' theorem prover. Fork of github.com/mg262/research

Smuggle arbitrary values in ()