Giter Club home page Giter Club logo

mathlib4's Introduction

mathlib4

GitHub CI Bors enabled project chat

This is a complete port of mathlib to Lean 4. Development of mathlib now takes place in this repository.

Mathlib is a user maintained library for the Lean theorem prover. It contains both programming infrastructure and mathematics, as well as tactics that use the former and allow to develop the latter.

Installation

You can find detailed instructions to install Lean, mathlib, and supporting tools on our website.

Experimenting

Got everything installed? Why not start with the tutorial project?

For more pointers, see Learning Lean.

Documentation

Besides the installation guides above and Lean's general documentation, the documentation of mathlib consists of:

Much of the discussion surrounding mathlib occurs in a Zulip chat room, and you are welcome to join, or read along without signing up. Questions from users at all levels of expertise are welcome! We also provide an archive of the public discussions, which is useful for quick reference.

Transitioning from Lean 3

For users familiar with Lean 3 who want to get up to speed in Lean 4 and migrate their existing Lean 3 code we have:

Contributing

The complete documentation for contributing to mathlib is located on the community guide contribute to mathlib

The process is different from other projects where one should not fork the repository. Instead write permission for non-master branches should be requested on Zulip by introducing yourself, providing your GitHub handle and what contribution you are planning on doing. You may want to subscribe to the mathlib4 stream

  • To obtain precompiled olean files, run lake exe cache get. (Skipping this step means the next step will be very slow.)

  • To build mathlib4 run lake build.

  • To build and run all tests, run make.

  • You can use lake build Mathlib.Import.Path to build a particular file, e.g. lake build Mathlib.Algebra.Group.Defs.

  • If you added a new file, run the following command to update Mathlib.lean

    find Mathlib -name "*.lean" | env LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean

Guidelines

Mathlib has the following guidelines and conventions that must be followed

Downloading cached build files

You can run lake exe cache get to download cached build files that are computed by mathlib4's automated workflow. If tar terminates with an error, it means that you might have ended up with corrupted files. In this case, run lake exe cache get! to overwrite them (get won't try to download the same file again).

Call lake exe cache to see its help menu.

Building HTML documentation

Building HTML documentation locally is straightforward, but it may take a while:

lake -Kdoc=on build Mathlib:docs

The HTML files can then be found in build/doc.

Dependencies

If you are a mathlib contributor and want to update dependencies, use lake update -Kdoc=on. This will update the lake-manifest.json file correctly. You will need to make a PR after committing the changes to this file.

Using mathlib4 as a dependency

Please refer to https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency

Maintainers:

For a list containing more detailed information, see https://leanprover-community.github.io/teams/maintainers.html

  • Anne Baanen (@Vierkantor): algebra, number theory, tactics
  • Matthew Robert Ballard (@mattrobball): algebra, algebraic geometry, category theory, performance
  • Reid Barton (@rwbarton): category theory, topology
  • Riccardo Brasca (@riccardobrasca): algebra, number theory, algebraic geometry, category theory
  • Mario Carneiro (@digama0): lean formalization, tactics, type theory, proof engineering
  • Bryan Gin-ge Chen (@bryangingechen): documentation, infrastructure
  • Johan Commelin (@jcommelin): algebra, number theory, category theory, algebraic geometry
  • Anatole Dedecker (@ADedecker): topology, functional analysis, calculus
  • Rémy Degenne (@RemyDegenne): probability, measure theory, analysis
  • Floris van Doorn (@fpvandoorn): measure theory, model theory, tactics
  • Frédéric Dupuis (@dupuisf): linear algebra, functional analysis
  • Gabriel Ebner (@gebner): tactics, infrastructure, core, formal languages
  • Sébastien Gouëzel (@sgouezel): topology, calculus, geometry, analysis, measure theory
  • Markus Himmel (@TwoFX): category theory
  • Chris Hughes (@ChrisHughes24): algebra
  • Yury G. Kudryashov (@urkud): analysis, topology, measure theory
  • Robert Y. Lewis (@robertylewis): tactics, documentation
  • Jireh Loreaux (@j-loreaux): analysis, topology, operator algebras
  • Heather Macbeth (@hrmacbeth): geometry, analysis
  • Patrick Massot (@patrickmassot): documentation, topology, geometry
  • Bhavik Mehta (@b-mehta): category theory, combinatorics
  • Kyle Miller (@kmill): combinatorics, documentation
  • Scott Morrison (@semorrison): category theory, tactics
  • Oliver Nash (@ocfnash): algebra, geometry, topology
  • Joël Riou (@joelriou): category theory, homology, algebraic geometry
  • Adam Topaz (@adamtopaz): algebra, category theory, algebraic geometry
  • Eric Wieser (@eric-wieser): algebra, infrastructure

Emeritus maintainers:

  • Jeremy Avigad (@avigad): analysis
  • Johannes Hölzl (@johoelzl): measure theory, topology
  • Simon Hudon (@cipher1024): tactics

mathlib4's People

Contributors

adedecker avatar alexjbest avatar arienmalec avatar casavaca avatar chrishughes24 avatar digama0 avatar dwrensha avatar eric-wieser avatar fpvandoorn avatar gebner avatar hrmacbeth avatar int-y1 avatar j-loreaux avatar jcommelin avatar joelriou avatar joneugster avatar kbuzzard avatar kmill avatar komyyy avatar mattrobball avatar mcdoll avatar mo271 avatar ocfnash avatar parcly-taxel avatar ruben-vandevelde avatar semorrison avatar sgouezel avatar urkud avatar xroblot avatar yaeldillies avatar

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.