Real-time collaboration for Jupyter Notebooks, Linux Terminals, LaTeX, VS Code, R IDE, and more,
all in one place.
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".
License: APACHE
How to install Lean and mathlib on Debian/Ubuntu
This document explains how to get started with Lean and mathlib if you are using a Linux distribution derived from Debian (Debian itself, Ubuntu, LMDE,...).
If you get stuck, please come to the chat room to ask for assistance.
Installing Lean and mathlib
Here we will discuss the fast way, assuming a lot of trust from you. It will install Lean, with supporting tools elan and leanpkg, the supporting tool update-mathlib for Lean's mathematical library, as well as the code editor VScode and its Lean plugin, and other dependencies you probably already have, like curl, git, python3, and pip3. If you don't like this method, there is a detailed webpage which will decompose the process into described stages, and won't ask for a blind sudo.
The fast way is: open a terminal and type:
You can now read instructions about creating and working on Lean projects