LLMs + Lean, on your laptop or in the cloud
-
Updated
Apr 18, 2024 - Lean
LLMs + Lean, on your laptop or in the cloud
Library for formalizing cryptography proofs in Lean 3 (Deprecated)
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).
A style guide for Coq
A formalization of graded rings in Lean, corresponding to a CICM 2022 submission
[WIP] A formalised proof of a generalised Carleson's Theorem in the Lean proof assistant.
A formalised proof of Fermat's Last Theorem for exponent 3 in the Lean proof assistant.
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
The Slate Interactive Theorem Prover
matroids in lean
HLM mathematical library for the Slate interactive theorem prover
mai: MAth Interpreter with standard foundations
The Principia Rewrite
The matrix cookbook, proved in the Lean theorem prover
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.
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."