Lean 3's obsolete mathematical components library: please use mathlib4
-
Updated
Jun 28, 2024 - Lean
Lean 3's obsolete mathematical components library: please use mathlib4
LLMs as Copilots for Theorem Proving in Lean
The Principia Rewrite
The matrix cookbook, proved in the Lean theorem prover
The Slate Interactive Theorem Prover
Template for blueprint-driven formalization projects in Lean.
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.
rubikcubegroup魔方定理证明+视频分享。discuss here: https://lean4daydayup.zulipchat.com/join/45reytdk5yv7t7sheywhulw3/
Library for formalizing cryptography proofs in Lean 3 (Deprecated)
A formalization of graded rings in Lean, corresponding to a CICM 2022 submission
Repository hosting resources for the "Lean Tutorial in Vienna" at TU Wien from September 18 to 20, 2024.
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
matroids in lean
LLMs + Lean, on your laptop or in the cloud
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
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.
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."