Repository hosting resources for the 2024 workshop "Computer-Verified Proofs: 48 Hours in Rome" organised by @oliver-butterley, @RafaelGreenblatt and @marcolenci.
-
Updated
Jan 26, 2024 - Lean
Repository hosting resources for the 2024 workshop "Computer-Verified Proofs: 48 Hours in Rome" organised by @oliver-butterley, @RafaelGreenblatt and @marcolenci.
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
mai: MAth Interpreter with standard foundations
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
Library for formalizing cryptography proofs in Lean 3 (Deprecated)
A formalization of graded rings in Lean, corresponding to a CICM 2022 submission
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.
A style guide for Coq
The Slate Interactive Theorem Prover
The matrix cookbook, proved in the Lean theorem prover
The Principia Rewrite
LLMs as Copilots for Theorem Proving in Lean
Lean 3's obsolete mathematical components library: please use mathlib4
Add a description, image, and links to the formal-mathematics topic page so that developers can more easily learn about it.
To associate your repository with the formal-mathematics topic, visit your repo's landing page and select "manage topics."