Skip to content

@FormalMathematicsLab Formal Mathematics Lab

Change the repository type filter

All

    Repositories list

    32 repositories

    • equational_theories

      Public
      A project to map out the relations between different equational theories of Magmas.
      Lean
      •
      Apache License 2.0
      •90•0•0•0•Updated Oct 7, 2024Oct 7, 2024

    • type_checking_in_lean4

      Public
      Type Checking in Lean 4
      JavaScript
      •
      Apache License 2.0
      •9•0•0•0•Updated Sep 1, 2024Sep 1, 2024

    • ICL_Course_FormalMathematics_2024

      Public
      Repository hosting resources for the 2024 course in Formal Mathematics at @ImperialCollegeLondon taught by Kevin Buzzard (@kbuzzard).
      mathematicsformalizationformal-mathematics
      Lean
      •
      Apache License 2.0
      •55•0•0•0•Updated Aug 22, 2024Aug 22, 2024

    • DL4TP

      Public
      A Survey on Deep Learning for Theorem Proving
      MIT License
      •16•2•0•0•Updated May 15, 2024May 15, 2024

    • UniBonn_Course_Lean4_2023-2024

      Public
      Repository hosting resources for the 2023/2024 course in Lean at the University of Bonn taught by Floris Van Doorn (@fpvandoorn).
      Lean
      •
      Apache License 2.0
      •21•0•0•0•Updated May 11, 2024May 11, 2024

    • odyssey-math

      Public
      Python
      •
      MIT License
      •13•1•0•0•Updated Apr 30, 2024Apr 30, 2024

    • human-style-atp

      Public
      CSS
      •
      MIT License
      •2•0•0•0•Updated Apr 29, 2024Apr 29, 2024

    • blog

      Public
      Source for the community blog
      Python
      •26•0•0•0•Updated Apr 28, 2024Apr 28, 2024

    • ntptutorial-II

      Public
      Neural theorem proving tutorial, version II
      Jupyter Notebook
      •
      MIT License
      •5•0•0•0•Updated Apr 19, 2024Apr 19, 2024

    • llmlean

      Public
      LLMs + Lean, on your laptop or in the cloud
      formalizationformal-mathematicsinteractive-theorem-provingautomated-theorem-provinglean4llm
      Lean
      •
      MIT License
      •31•2•0•0•Updated Apr 18, 2024Apr 18, 2024

    • lean4-logic

      Public
      Lean4 Logic Formalization.
      Lean
      •12•0•0•0•Updated Apr 16, 2024Apr 16, 2024

    • theorem_proving_in_lean4

      Public
      Theorem Proving in Lean 4
      JavaScript
      •
      Apache License 2.0
      •122•0•0•0•Updated Apr 7, 2024Apr 7, 2024

    • LFTCM2024

      Public
      Repository hosting resources for the 2024 workshop "Lean for the Curious Mathematician".
      workshopconferenceformalizationlean4
      Lean
      •
      Apache License 2.0
      •6•0•0•0•Updated Apr 2, 2024Apr 2, 2024

    • leanblueprint

      Public
      plasTeX plugin to build formalization blueprints.
      Python
      •
      Apache License 2.0
      •55•0•0•0•Updated Mar 31, 2024Mar 31, 2024

    • mathlib4

      Public
      The math library of Lean 4.
      Lean
      •
      Apache License 2.0
      •1.1k•0•0•0•Updated Feb 25, 2024Feb 25, 2024

    • Website_LeanInRome

      Public
      Website for the formalisation of mathematics and Lean event in Rome
      Vue
      •
      MIT License
      •1•0•0•0•Updated Feb 1, 2024Feb 1, 2024

    • fpv2023

      Public
      Lecture notes, exercises, homeworks for Brown CS1951x 2023
      Lean
      •13•0•0•0•Updated Jan 31, 2024Jan 31, 2024

    • lean4

      Public
      Lean 4 programming language and theorem prover
      Lean
      •
      Apache License 2.0
      •750•0•0•0•Updated Jan 31, 2024Jan 31, 2024

    • leanprover-community.github.io

      Public
      Hosts the website for mathlib and other Lean community infrastructure.
      CSS
      •
      MIT License
      •169•0•0•0•Updated Jan 31, 2024Jan 31, 2024

    • STG4

      Public
      Set Theory Game
      Lean
      •10•0•0•0•Updated Jan 30, 2024Jan 30, 2024

    • PNT-Plus

      Public
      blueprint for prime number theorem and more
      Lean
      •
      Apache License 2.0
      •71•0•0•0•Updated Jan 30, 2024Jan 30, 2024

    • Arithmetization

      Public
      Formalization of Arithmetization of Metamathematics
      Lean
      •2•0•0•0•Updated Jan 30, 2024Jan 30, 2024

    • UniRome_Workshop_Lean_2024

      Public
      Repository hosting resources for the 2024 workshop "Computer-Verified Proofs: 48 Hours in Rome" organised by @oliver-butterley, @RafaelGreenblatt and @marcolenc…
      mathematicsformal-methodsformalizationformal-verificationformal-mathematicslean4formalisation-mathematics
      Lean
      •3•0•0•0•Updated Jan 26, 2024Jan 26, 2024

    • mathematics_in_lean_source

      Public
      Source code for the Mathematics in Lean tutorial.
      Lean
      •96•0•0•0•Updated Jan 19, 2024Jan 19, 2024

    • pfr

      Public
      Repository for formalization of the Polynomial Freiman Ruzsa conjecture (and related results)
      Lean
      •41•0•0•0•Updated Jan 17, 2024Jan 17, 2024

    • lean4-metaprogramming-book

      Public
      Lean
      •
      Apache License 2.0
      •70•0•0•0•Updated Jan 14, 2024Jan 14, 2024

    • mathlib4-all-tactics

      Public
      Markdown file of the list and explanations of all mathlib4 tactics
      Lean
      •
      Apache License 2.0
      •7•0•0•0•Updated Jan 6, 2024Jan 6, 2024

    • ntptutorial

      Public
      Tutorial on neural theorem proving
      Jupyter Notebook
      •
      MIT License
      •16•0•0•0•Updated Jan 5, 2024Jan 5, 2024

    • logical_verification_2023

      Public
      Hitchhiker's Guide to Logical Verification (2023 Edition)
      Lean
      •19•0•0•0•Updated Nov 22, 2023Nov 22, 2023

    • HausdorffSchoolLean

      Public
      Repository for the September 2023 Hausdorff School on Lean
      Lean
      •
      Apache License 2.0
      •3•0•0•0•Updated Nov 15, 2023Nov 15, 2023