Authors: Nicolò Cavalleri under the supervision of Dr. Anthony Bordg
Update: Due to the covid-19 pandemic the project is taking place online in a dedicated channel of the Schrödinger's Chat.
The project has also a dedicated channel on the Xena project Discord server of Prof. Kevin Buzzard.
The official webpage of the theorem prover Lean (for download + documentation). You should use Lean 3.
The Lean Zulip chat (for questions, beginners welcome). You can start by skimming through the new-members stream. Note that there is a private stream "cambridge" on the Lean Zulip chat for the students in Cambridge interested in Lean.
An online tutorial by Prof. Kevin Buzzard for beginners.
You don't need to know much about tactics in Lean to start working on the preliminary challenges (see the tex file prelim_challenges in the master branch), since they focus on definitions and statements, no proof required.
Please have a look at the manifold directory of the Mathlib library, and the corresponding topic manifolds on the Zulip chat.
Of course, also note that mathlib contains many repositories, especially algebra, linear_algebra and topology which will be useful.
Biliography:
- Gauge Fields, Knots and Gravity, by John Baez and Javier Muniain.
- Introduction to Lie groups and Lie algebras, by Alexander Kirillov Jr.