.. Example documentation master file, created by
   sphinx-quickstart on Sat Sep 23 20:35:12 2023.
   You can adapt this file completely to your liking, but it should at least
   contain the root `toctree` directive.

Formalising Mathematics
===================================

A handbook for mathematicians. Written by Bhavik Mehta, for his Formalising Mathematics course,
adapted from an earlier handbook by Kevin Buzzard. Thanks to Imperial College London for letting the
course happen.

.. note::

   This document is written for people with some mathematical experience (e.g., people in the final year of an undergraduate mathematics degree). Its aim is to show such people how to formalise mathematics in the Lean theorem prover. We make extensive use of Lean's mathematical library ``mathlib``.

If you're new here, start at the :ref:`introduction <introduction>`.

Here’s a link to the `repository for this course <https://github.com/b-mehta/formalising-mathematics-notes>`_ containing all the code.

Part 1 is a collection of notes on various frequently asked questions that might be helpful for the
course.

Part 2 is a list of many basic tactics including documentation and examples.

.. toctree::
   :maxdepth: 1
   :caption: Contents:

   Introduction/introduction
   Introduction/install

   Part_1/Part_1

   Part_2/Part_2