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".

1
DEPLOY_NIGHTLY_GITHUB_USER=leanprover-community-bot
2

3
set -e
4
set -x
5

6
# By default, github actions overrides the credentials used to access any
7
# github url so that it uses the github-actions[bot] user.  We want to access
8
# github using a different username.
9
git config --unset http.https://github.com/.extraheader
10

11
git_hash="$(git log -1 --pretty=format:%h)"
12
git clone https://github.com/leanprover-community/doc-gen.git
13
cd doc-gen
14
sed -i "s/rev = \"\S*\"/rev = \"$git_hash\"/" leanpkg.toml
15
echo -e "builtin_path\npath ./src\npath ../src" > leanpkg.path
16
git clone "https://$DEPLOY_NIGHTLY_GITHUB_USER:$DEPLOY_NIGHTLY_GITHUB_TOKEN@github.com/leanprover-community/mathlib_docs.git"
17
rm -rf mathlib_docs/docs/
18
elan override set leanprover-community/lean:nightly
19
python3 -m pip install --upgrade pip
20
pip3 install markdown2 toml
21
./gen_docs -w -r "../" -t "mathlib_docs/docs/"
22
cd mathlib_docs/docs
23
git config user.email "leanprover.community@gmail.com"
24
git config user.name "leanprover-community-bot"
25
git add -A .
26
git commit -m "automatic update to $git_hash"
27
git push
28

29