Repositories list

• equational_theories

  Public
  A project to map out the relations between different equational theories of Magmas.

  Lean

  •

  Apache License 2.0

  •51•0•0•0•Updated Oct 7, 2024Oct 7, 2024

• type_checking_in_lean4

  Public
  Type Checking in Lean 4

  JavaScript

  •

  Apache License 2.0

  •6•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

  •36•0•0•0•Updated Aug 22, 2024Aug 22, 2024

• DL4TP

  Public
  A Survey on Deep Learning for Theorem Proving

  MIT License

  •9•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

  •8•1•0•0•Updated Apr 30, 2024Apr 30, 2024

• human-style-atp

  Public
  CSS

  •

  MIT License

  •3•0•0•0•Updated Apr 29, 2024Apr 29, 2024

• blog

  Public
  Source for the community blog

  Python

  •20•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-proving+ 3automated-theorem-provinglean4llm

  Lean

  •

  MIT License

  •15•1•0•0•Updated Apr 18, 2024Apr 18, 2024

• lean4-logic

  Public
  Lean4 Logic Formalization.

  Lean

  •5•0•0•0•Updated Apr 16, 2024Apr 16, 2024

• theorem_proving_in_lean4

  Public
  Theorem Proving in Lean 4

  JavaScript

  •

  Apache License 2.0

  •92•0•0•0•Updated Apr 7, 2024Apr 7, 2024

• LFTCM2024

  Public
  Repository hosting resources for the 2024 workshop "Lean for the Curious Mathematician".

  workshopconferenceformalization+ 1lean4

  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

  •28•0•0•0•Updated Mar 31, 2024Mar 31, 2024

• mathlib4

  Public
  The math library of Lean 4.

  Lean

  •

  Apache License 2.0

  •341•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

  •2•0•0•0•Updated Feb 1, 2024Feb 1, 2024

• fpv2023

  Public
  Lecture notes, exercises, homeworks for Brown CS1951x 2023

  Lean

  •12•0•0•0•Updated Jan 31, 2024Jan 31, 2024

• lean4

  Public
  Lean 4 programming language and theorem prover

  Lean

  •

  Apache License 2.0

  •424•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

  •123•0•0•0•Updated Jan 31, 2024Jan 31, 2024

• STG4

  Public
  Set Theory Game

  Lean

  •8•0•0•0•Updated Jan 30, 2024Jan 30, 2024

• PNT-Plus

  Public
  blueprint for prime number theorem and more

  Lean

  •

  Apache License 2.0

  •26•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 @marcolenci.

  mathematicsformal-methodsformalization+ 4formal-verificationformal-mathematicslean4formalisation-mathematics

  Lean

  •2•0•0•0•Updated Jan 26, 2024Jan 26, 2024

• mathematics_in_lean_source

  Public
  Source code for the Mathematics in Lean tutorial.

  Lean

  •70•0•0•0•Updated Jan 19, 2024Jan 19, 2024

• pfr

  Public
  Repository for formalization of the Polynomial Freiman Ruzsa conjecture (and related results)

  Lean

  •33•0•0•0•Updated Jan 17, 2024Jan 17, 2024

• lean4-metaprogramming-book

  Public
  Lean

  •

  Apache License 2.0

  •55•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

  •15•0•0•0•Updated Jan 5, 2024Jan 5, 2024

• logical_verification_2023

  Public
  Hitchhiker's Guide to Logical Verification (2023 Edition)

  Lean

  •17•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

  •2•0•0•0•Updated Nov 15, 2023Nov 15, 2023