matroids in lean
-
Updated
Dec 21, 2020 - Lean
#
formal-mathematics
Here are 39 public repositories matching this topic...
A style guide for Coq
c haskell dependent-types style-guide ocaml coq proof formal-semantics verification proof-assistant software-engineering formal-methods formal-verification formal-mathematics formal-specification formal-proofs appliedfm
-
Updated
Nov 30, 2021
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.
lean natural-numbers formal-mathematics peano theorem-prover microsoft-research lean-theorem-prover imperial-college-london gamified-learning
-
Updated
Dec 12, 2021
A formalization of graded rings in Lean, corresponding to a CICM 2022 submission
-
Updated
Sep 21, 2022 - Lean
HLM mathematical library for the Slate interactive theorem prover
web-app mathematics collaboration proof-assistant mathematical-expressions mathematical-logic formal-mathematics interactive-theorem-proving
-
Updated
Nov 5, 2022 - Shell
The Slate Interactive Theorem Prover
web-app collaboration proof-assistant mathematical-expressions mathematical-logic formal-mathematics interactive-theorem-proving
-
Updated
Jan 9, 2023 - TypeScript
Repository hosting resources for the 2024 workshop "Computer-Verified Proofs: 48 Hours in Rome" organised by @oliver-butterley, @RafaelGreenblatt and @marcolenci.
mathematics formal-methods formalization formal-verification formal-mathematics lean4 formalisation-mathematics
-
Updated
Jan 26, 2024 - Lean
Library for formalizing cryptography proofs in Lean 3 (Deprecated)
-
Updated
Apr 8, 2024 - Lean
rubikcubegroup魔方定理证明+视频分享。discuss here: https://lean4daydayup.zulipchat.com/join/45reytdk5yv7t7sheywhulw3/
-
Updated
Apr 16, 2024 - Lean
LLMs + Lean, on your laptop or in the cloud
-
Updated
Apr 18, 2024 - Lean
Lean 3's obsolete mathematical components library: please use mathlib4
-
Updated
Jun 28, 2024 - Lean
[WIP] A formalised proof of a generalised Carleson's Theorem in the Lean proof assistant.
analysis mathematics proof-assistant formal-methods formalization fourier-analysis formal-mathematics interactive-theorem-proving theorem-prover harmonic-analysis lean4
-
Updated
Jul 3, 2024 - TeX
A formalised proof of Fermat's Last Theorem for exponent 3 in the Lean proof assistant.
algebra mathematics proof-assistant lean formal-methods formalization number-theory formal-mathematics interactive-theorem-proving theorem-prover formal-proofs mathematical-programming lean4
-
Updated
Aug 21, 2024 - TeX
Repository hosting resources for the 2024 course in Formal Mathematics at @ImperialCollegeLondon taught by Kevin Buzzard (@kbuzzard).
-
Updated
Aug 22, 2024 - Lean
mai: MAth Interpreter with Standard Foundations
first-order-logic proof-assistant set-theory formal-mathematics foundations-of-mathematics automated-theorem-proving
-
Updated
Sep 10, 2024 - Prolog
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
algebra lean formal-methods number-theory formal-mathematics formal-proofs fermat-last-theorem lean4
-
Updated
Sep 28, 2024 - Lean
Repository hosting resources for the "Lean Tutorial in Vienna" at TU Wien from September 18 to 20, 2024.
tutorial research logic mathematics proof-assistant lean formal-methods formal-mathematics interactive-theorem-proving tu-wien formal-proofs formalisation leanprover lean4 formalized-mathematics formalisation-mathematics
-
Updated
Jan 14, 2025 - Lean
構成的素数構造（6n±1）と除去関数により、Goldbach予想・Bertrand仮説・Catalan予想を共通基盤から再構成。非構成的証明とも形式整合し、論理強度と実行再現性の両立を実現。GitHubにて統合証明パッケージとして公開。 Using the 6n±1 prime structure and composite exclusion, we reconstruct and unify constructive proofs of Goldbach, Bertrand, and Catalan conjectures, demonstrating formal alignment with classical non-constructive methods.
prime-numbers number-theory mathematical-logic formal-mathematics goldbach-conjecture constructive-proof catalan-conjecture bertrand-postulate github-research
-
Updated
Jul 2, 2025 - Python
The matrix cookbook, proved in the Lean theorem prover
-
Updated
Sep 16, 2025 - Lean
Lean formalizations of IMO problem statements
-
Updated
Oct 23, 2025 - Lean
Improve this page
Add a description, image, and links to the formal-mathematics topic page so that developers can more easily learn about it.
Add this topic to your repo
To associate your repository with the formal-mathematics topic, visit your repo's landing page and select "manage topics."