Here are links to external resources for Lean4. They are not suitable for regular use in this class, as they mostly assume considerable background knowledge, but I provide them as you might occasionally find them useful, and if you're really interested in what we cover in this class, by all means dive in to the world of dependable and automated reasoning.