LaTeX

It is encouraged, but not required, that you use LaTeX for typesetting your homework assignments. LaTex is a powerful markup language for typing up mathematics and is used in many technical fields. Appendix D of our textbook has a nice introduction to the basic features of LaTeX. I will make homework files available in LaTex format so you can start using it right away. If this is your first time using LaTeX, I recommend that you start by using an online editor (e.g. Overleaf).

There are also offline TeX editors which you can install on your commputer:

Here are some guides to the basic elements of LaTeX:

If you are interested in pushing your LaTeX skills further, the best place on the web for Q&A about LaTeX is tex.stackexchange.

Lean

The Lean theorem prover is a proof assistant developed principally by Leonardo de Moura at Microsoft Research.

The Lean mathematical library, mathlib, is a community-driven effort to build a unified library of mathematics formalized in the Lean proof assistant. The library also contains definitions useful for programming. This project is very active, with many regular contributors and daily activity.

Find more information about Lean proof assistant here.