HOL Light's new tutorial promises to get you proving theorems fast
HOL Light Tutorial
The HOL Light theorem prover is notoriously hard to start with, and its manual is intimidating. This alternative quick-start guide teaches basic use through a graded set of examples, covering installation on Windows via WSL or Cygwin, OCaml setup, and a Visual Studio Code plugin. It then walks through terms, types, theorems, tactics, inductive definitions, and applications from RSA encryption to real analysis, offering a gentler path into formal verification.
The HOL Light theorem prover can be difficult to get started with. While the manual is fairly detailed and comprehensive, the large amount of background information that has to be absorbed before the user can do anything interesting is intimidating.