TheoremDB is a public workspace designed for machine mathematics, currently in alpha. It allows live contributions, including Lean proof submissions, and aims to reduce redundancy in research efforts.