Skip to content

@leanprover-community leanprover-community

Change the repository type filter

All

    Repositories list

    76 repositories

    • mathlib4

      Public
      The math library of Lean 4
      lean4
      Lean
      •
      Apache License 2.0
      •438•2k•261•1.6k•Updated Jun 10, 2025Jun 10, 2025

    • queueboard

      Public
      Mathlib4 review and triage dashboard
      Python
      •
      Apache License 2.0
      •9•8•28•2•Updated Jun 10, 2025Jun 10, 2025

    • batteries

      Public
      The "batteries included" extended library for the Lean programming language and theorem prover
      leanlean4
      Lean
      •
      Apache License 2.0
      •119•304•22•62•Updated Jun 10, 2025Jun 10, 2025

    • leanprover-community.github.io

      Public
      Hosts the website for mathlib and other Lean community infrastructure.
      CSS
      •
      MIT License
      •146•62•16•8•Updated Jun 10, 2025Jun 10, 2025

    • mathlib_stats

      Public
      Display gitstats output on the mathlib website
      Python
      •6•2•0•0•Updated Jun 10, 2025Jun 10, 2025

    • mathlib-update-action

      Public
      Action for automatically updating to Mathlib releases
      JavaScript
      •
      MIT License
      •0•0•0•0•Updated Jun 9, 2025Jun 9, 2025

    • blog

      Public
      Source for the community blog
      Python
      •24•7•4•11•Updated Jun 9, 2025Jun 9, 2025

    • lean4-mode

      Public
      Emacs major mode for Lean 4
      emacslean4
      Emacs Lisp
      •
      Apache License 2.0
      •32•93•22•3•Updated Jun 8, 2025Jun 8, 2025

    • flt-regular

      Public
      Fermat's Last Theorem for regular primes
      Lean
      •
      Apache License 2.0
      •3•58•0•0•Updated Jun 7, 2025Jun 7, 2025

    • import-graph

      Public
      Tool to analyse the import structure of lean projects.
      lean4
      Lean
      •
      Apache License 2.0
      •12•13•2•1•Updated Jun 5, 2025Jun 5, 2025

    • repl

      Public
      A simple REPL for Lean 4, returning information about errors and sorries.
      Lean
      •53•130•20•13•Updated Jun 4, 2025Jun 4, 2025

    • aesop

      Public
      White-box automation for Lean 4
      lean4
      Lean
      •
      Apache License 2.0
      •33•273•33•1•Updated Jun 4, 2025Jun 4, 2025

    • ProofWidgets4

      Public
      Helper toolkit for creating your own Lean 4 UserWidgets
      leanlean4visualization
      Lean
      •
      Apache License 2.0
      •38•141•13•0•Updated Jun 4, 2025Jun 4, 2025

    • plausible

      Public
      Lean
      •
      Apache License 2.0
      •8•46•1•3•Updated Jun 4, 2025Jun 4, 2025

    • quote4

      Public
      Intuitive, type-safe expression quotations for Lean 4.
      lean4
      Lean
      •
      Apache License 2.0
      •14•85•14•6•Updated Jun 4, 2025Jun 4, 2025

    • sphere-eversion

      Public
      Formalization of the existence of sphere eversions
      Lean
      •
      Apache License 2.0
      •15•43•0•1•Updated Jun 4, 2025Jun 4, 2025

    • tutorials4

      Public
      Lean 4 tutorial files
      Lean
      •
      Apache License 2.0
      •8•38•0•1•Updated Jun 3, 2025Jun 3, 2025

    • mathematics_in_lean

      Public
      The user home repository for the Mathematics in Lean tutorial.
      HTML
      •250•366•0•0•Updated Jun 3, 2025Jun 3, 2025

    • lean4game

      Public
      Server to host lean games.
      reactlean4
      TypeScript
      •
      GNU General Public License v3.0
      •46•269•92•7•Updated May 28, 2025May 28, 2025

    • con-nf

      Public
      A formal consistency proof of Quine's set theory New Foundations
      set-theorylean4new-foundations
      Lean
      •
      Apache License 2.0
      •7•71•1•0•Updated May 27, 2025May 27, 2025

    • lean-release-tag

      Public
      Action that creates a Git tag when updating to a new Lean release.
      Shell
      •0•0•1•0•Updated May 26, 2025May 26, 2025

    • LeanSearchClient

      Public
      Syntax for searching with natural language from Lean, using https://leansearch.net/ (may extend to other services)
      Lean
      •
      Apache License 2.0
      •6•23•3•0•Updated May 26, 2025May 26, 2025

    • iris-lean

      Public
      Lean 4 port of Iris, a higher-order concurrent separation logic framework
      Lean
      •
      Apache License 2.0
      •12•99•16•6•Updated May 25, 2025May 25, 2025

    • lint-style-action

      Public
      Mathlib style linter
      0•1•0•0•Updated May 22, 2025May 22, 2025

    • duper

      Public
      lean4
      Lean
      •
      Apache License 2.0
      •12•79•0•0•Updated May 21, 2025May 21, 2025

    • lean-auto

      Public
      Experiments in automation for Lean
      Lean
      •
      Apache License 2.0
      •18•113•8•1•Updated May 21, 2025May 21, 2025

    • archive

      Public
      Replacement for the archive repo
      HTML
      •3•3•1•0•Updated May 2, 2025May 2, 2025

    • gh-problem-matcher-wrap

      Public
      Invoke linters, detect errors/warnings, show them as annotations. Supports PRs from forks, unlike other Actions.
      JavaScript
      •
      MIT License
      •7•0•0•0•Updated Apr 23, 2025Apr 23, 2025

    • lean4web

      Public
      The Lean 4 web editor
      lean4
      TypeScript
      •
      Apache License 2.0
      •34•93•9•3•Updated Apr 11, 2025Apr 11, 2025

    • mathlib-manual

      Public
      JavaScript
      •
      Apache License 2.0
      •23•0•0•1•Updated Apr 8, 2025Apr 8, 2025