lean-perfectoid-spaces
A formalization of the concept of a perfectoid space in the Lean formal proof verification system.
By Kevin Buzzard, Johan Commelin, and Patrick Massot.
See the project website.
There are no reviews yet. Be the first to send feedback to the community and the maintainers!
A formalization of the concept of a perfectoid space in the Lean formal proof verification system.
By Kevin Buzzard, Johan Commelin, and Patrick Massot.
See the project website.
mathlib3
Lean 3's obsolete mathematical components library: please use mathlib4mathlib4
The math library of Lean 4lean
Lean 3 Theorem Prover (community fork)mathematics_in_lean
The user home repository for the Mathematics in Lean tutorial.batteries
The "batteries included" extended library for the Lean programming language and theorem proverlean4-metaprogramming-book
tutorials
Some Lean tutorialsaesop
White-box automation for Lean 4lean-liquid
💧 Liquid Tensor Experimentlean4game
Server to host lean games.ProofWidgets4
Helper toolkit for creating your own Lean 4 UserWidgetsNNG4
Natural Number Gamequote4
Intuitive, type-safe expression quotations for Lean 4.con-nf
A formal consistency proof of Quine's set theory New Foundationslean-auto
Experiments in automation for Leanlftcm2020
Lean for the Curious Mathematician 2020lean4web
The Lean 4 web editorformat_lean
A Lean file formatteriris-lean
Lean 4 port of Iris, a higher-order concurrent separation logic frameworklean4-mode
Emacs major mode for Lean 4leanprover-community.github.io
Hosts the website for mathlib and other Lean community infrastructure.flt-regular
Fermat's Last Theorem for regular primeslean-client-python
Python talking to the Lean theorem provermathport
Mathport is a tool for porting Lean3 projects to Lean4sphere-eversion
Formalization of the existence of sphere eversionsmathlib-tools
Development tools for https://github.com/leanprover-community/mathlibmathzoo
Lean mathzoorepl
A simple REPL for Lean 4, returning information about errors and sorries.doc-gen
Generate HTML documentation for mathlib and Leanleancrawler
An obsolete python library which gathers statistics and relational information about Lean 3 libraries.llm
Interfacing with Large Language Models (remote and local) from Lean.mathlib3port
Synport output from mathport for mathlib3lean-sensitivity
A formalization of Huang's degree theoremduper
mathlib4_docs
highlightjs-lean
A highlight.js language grammar for the Lean theorem proving language.import-graph
Tool to analyse the import structure of lean projects.blog
Source for the community blogmathlib_docs
Hosts the HTML documentation for mathlib.liquid
Website and documentation for the Liquid Tensor Experimentlt2021
Website for Lean Together 2021plausible
lean-mode-contrib
mathlib-nursery
yasnippet-lean
mathlib-port-status
Tools for managing the status of the portarchive-old
LeanSearchClient
Syntax for searching with natural language from Lean, using https://leansearch.net/ (may extend to other services)logic_and_proof
archive
Replacement for the archive repomathlib_docs_demo
tutorials4
Lean 4 tutorial fileslean3port
Stub for downloading mathport artifacts for Lean 3test-mathport
mathlib_stats
Display gitstats output on the mathlib websitewitt-vectors
azure-scripts
scripts and cron jobs for Azuremathlib-nightly
stores nightly releases of mathlibLove Open Source and this site? Check out how you can help us