The purpose of the library is to provide a Digital Mathematics Library (DML) for the worldwide scientific community as a public service with the aim to help scientists locate the information that is distributed in various digital repositories, discover information related to their work in optimal way and be exhaustive and comprehensive in the field of mathematics.
zbMATH Open (formerly known as Zentralblatt MATH) is the world's most comprehensive and longest-running abstracting and reviewing service in pure and applied mathematics. It is edited by the European Mathematical Society (EMS), the Heidelberg Academy of Sciences and Humanities, and FIZ Karlsruhe.
A repository of freely downloadable mathematical works in progress hosted by the American Mathematical Society as a service to researchers, teachers and students. These draft works include course notes, textbooks, and research expositions in progress. They have not been published elsewhere, and, as works in progress, are subject to significant revision. Visitors are encouraged to download and use these materials as teaching and research aids, and to send constructive comments and suggestions to the authors.
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 book is intended to accompany my book How To Prove It: A Structured Approach, 3rd edition. The purpose of this book is to show you how to use a computer software package called Lean to help you master the techniques presented in HTPI.
The HOL interactive theorem prover is a proof assistant for higher-order logic: a programming environment in which theorems can be proved and proof tools implemented. Built-in decision procedures and theorem provers can automatically establish many simple theorems (users may have to prove the hard theorems themselves!) An oracle mechanism gives access to external programs such as SMT and BDD engines. HOL is particularly suitable as a platform for implementing combinations of deduction, execution and property checking.