Basic Mathematics

• Basic Mathematics
  • Usage
    • Getting started
    • Building

This project is a attempting to formalize the mathematics developed in the book Basic Mathematics by the legendary Serge Lang.

The formalization is done using the lean4 theorem prover/programming language.

Usage

Getting started

BasicMathematics depends on mathlib4. To sync the project with the required dependencies and the correct lean4 version, run the following command:

lake exe cache get

Assuming this finished without errors, the project should now be in a working state.

Building

lake build