Log in to Zulip
hol-light
https://hol-light.zulipchat.com
HOL Light is a computer program written by John Harrison to help users prove interesting mathematical theorems completely formally in higher order logic.