Skip to content

@leanprover-community leanprover-community

Change the repository type filter

All

    Repositories list

    82 repositories

    • queueboard

      Public
      AspectJ
      •
      Apache License 2.0
      •0•0•0•3•Updated Dec 4, 2025Dec 4, 2025

    • hammer-bench

      Public
      Benchmark suite for hammer tactics
      Python
      •0•0•0•0•Updated Dec 4, 2025Dec 4, 2025

    • mathlib4

      Public
      The math library of Lean 4
      lean4
      Lean
      •
      Apache License 2.0
      •909•2.6k•266•1.9k•Updated Dec 4, 2025Dec 4, 2025

    • blog

      Public
      Source for the community blog
      Python
      •26•7•4•4•Updated Dec 4, 2025Dec 4, 2025

    • mathlib4-nightly-testing

      Public
      nightly-testing and lean-pr-testing branches of Mathlib
      Lean
      •
      Apache License 2.0
      •909•0•0•10•Updated Dec 4, 2025Dec 4, 2025

    • batteries

      Public
      The "batteries included" extended library for the Lean programming language and theorem prover
      leanlean4
      Lean
      •
      Apache License 2.0
      •126•341•25•42•Updated Dec 4, 2025Dec 4, 2025

    • leanprover-community.github.io

      Public
      Hosts the website for mathlib and other Lean community infrastructure.
      CSS
      •
      MIT License
      •165•68•18•5•Updated Dec 4, 2025Dec 4, 2025

    • aesop

      Public
      White-box automation for Lean 4
      lean4
      Lean
      •
      Apache License 2.0
      •43•315•36•2•Updated Dec 4, 2025Dec 4, 2025

    • mathlib_stats

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

    • duper

      Public
      lean4
      Lean
      •
      Apache License 2.0
      •12•96•1•0•Updated Dec 4, 2025Dec 4, 2025

    • lean-auto

      Public
      Experiments on automation for Lean
      Lean
      •
      Apache License 2.0
      •24•148•9•0•Updated Dec 4, 2025Dec 4, 2025

    • flt-regular

      Public
      Fermat's Last Theorem for regular primes
      Lean
      •
      Apache License 2.0
      •3•61•0•0•Updated Dec 3, 2025Dec 3, 2025

    • quote4

      Public
      Intuitive, type-safe expression quotations for Lean 4.
      lean4
      Lean
      •
      Apache License 2.0
      •18•102•16•7•Updated Dec 2, 2025Dec 2, 2025

    • lean4web

      Public
      The Lean 4 web editor
      lean4
      TypeScript
      •
      Apache License 2.0
      •43•121•10•5•Updated Dec 1, 2025Dec 1, 2025

    • lean4game

      Public
      Server to host lean games.
      reactlean4
      TypeScript
      •
      GNU General Public License v3.0
      •63•350•101•7•Updated Nov 30, 2025Nov 30, 2025

    • ProofWidgets4

      Public
      Helper toolkit for creating your own Lean 4 UserWidgets
      visualizationleanlean4
      Lean
      •
      Apache License 2.0
      •41•166•13•2•Updated Nov 27, 2025Nov 27, 2025

    • iris-lean

      Public
      Lean 4 port of Iris, a higher-order concurrent separation logic framework
      Lean
      •
      Apache License 2.0
      •20•132•20•17•Updated Nov 25, 2025Nov 25, 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
      •7•27•4•1•Updated Nov 25, 2025Nov 25, 2025

    • sphere-eversion

      Public
      Formalization of the existence of sphere eversions
      Lean
      •
      Apache License 2.0
      •15•45•0•1•Updated Nov 24, 2025Nov 24, 2025

    • queueboard-core

      Public
      testing a split of code and data for the queueboard
      Python
      •
      Apache License 2.0
      •6•2•25•5•Updated Nov 24, 2025Nov 24, 2025

    • repl

      Public
      A simple REPL for Lean 4, returning information about errors and sorries.
      Lean
      •
      Apache License 2.0
      •59•171•25•18•Updated Nov 21, 2025Nov 21, 2025

    • import-graph

      Public
      Tool to analyse the import structure of lean projects.
      lean4
      Lean
      •
      Apache License 2.0
      •13•15•2•0•Updated Nov 21, 2025Nov 21, 2025

    • plausible

      Public
      Lean
      •
      Apache License 2.0
      •14•71•1•4•Updated Nov 21, 2025Nov 21, 2025

    • mathlib-landing

      Public
      HTML
      •0•0•0•0•Updated Nov 21, 2025Nov 21, 2025

    • tutorials4

      Public
      Lean 4 tutorial files
      Lean
      •
      Apache License 2.0
      •8•45•1•1•Updated Nov 21, 2025Nov 21, 2025

    • docgen-action

      Public
      Action to generate Lean documentation pages
      JavaScript
      •3•3•6•1•Updated Nov 17, 2025Nov 17, 2025

    • mathlib-update-action

      Public
      Action for automatically updating to Mathlib releases
      JavaScript
      •
      MIT License
      •3•4•1•0•Updated Nov 11, 2025Nov 11, 2025

    • bors-ng

      Public
      👁 A merge bot for GitHub Pull Requests
      Elixir
      •
      Apache License 2.0
      •181•2•0•0•Updated Nov 9, 2025Nov 9, 2025

    • azure-scripts

      Public
      scripts and cron jobs for Azure
      Python
      •5•1•0•0•Updated Nov 6, 2025Nov 6, 2025

    • mathlib-manual

      Public
      Lean
      •
      Apache License 2.0
      •41•1•0•1•Updated Nov 3, 2025Nov 3, 2025