Repository hosting resources for the 2024 workshop "Computer-Verified Proofs: 48 Hours in Rome" organised by @oliver-butterley, @RafaelGreenblatt and @marcolenci.

Personal blog about formal mathematics.

Repository hosting resources for the 2024 course in Formal Mathematics at @ImperialCollegeLondon taught by Kevin Buzzard (@kbuzzard).

[WIP] A formalised proof of a generalised Carleson's Theorem in the Lean proof assistant.

LLMs + Lean, on your laptop or in the cloud

Ongoing Lean formalisation of the proof of Fermat's Last Theorem

matroids in lean

A formalised proof of Fermat's Last Theorem for exponent 3 in the Lean proof assistant.

HLM mathematical library for the Slate interactive theorem prover

mai: MAth Interpreter with Standard Foundations

Repository hosting resources for the "Lean Tutorial in Vienna" at TU Wien from September 18 to 20, 2024.

Library for formalizing cryptography proofs in Lean 3 (Deprecated)

A formalization of graded rings in Lean, corresponding to a CICM 2022 submission

rubikcubegroup魔方定理证明+视频分享。discuss here: https://lean4daydayup.zulipchat.com/join/45reytdk5yv7t7sheywhulw3/

A style guide for Coq

Solutions to Imperial College London's Natural Number Game, a gamified formal mathematics course on the Peano axioms using an interactive + automated theorem prover developed by Microsoft Research called Lean.

The Slate Interactive Theorem Prover

Template for blueprint-driven formalization projects in Lean.

The matrix cookbook, proved in the Lean theorem prover

The Principia Rewrite