Real-time collaboration for Jupyter Notebooks, Linux Terminals, LaTeX, VS Code, R IDE, and more,
all in one place.

Try doing some basic maths questions in the Lean Theorem Prover. Functions, real numbers, equivalence relations and groups. Click on README.md and then on "Open in CoCalc with one click".

Archive

This is an archive for formalizations which don't have a good place in mathlib, probably because there is (almost) no math depending on these results.

We keep these formalizations here so that when mathlib changes, we can keep these formalizations up to date.

Contributing

If you have done a formalization which you want to add here, just make a pull request to mathlib.

When you make a pull request, do make sure that you put all lemmas which are generally useful in right place in mathlib (in the src/ directory).

Try to adhere to the guidelines for mathlib. They will be much less strictly enforced for the archive, but we still want you to adhere to all the conventions that make maintenance easier. This ensures that when mathlib is changing, the mathlib maintainers can fix these contributions without much effort. Here are the guidelines:

• The style guide for contributors.

• The git commit conventions.

• You don't have to follow the naming conventions.