Follow
Big news: My friend William DeMeo has announced that he's formalised Birkhoff HSP Theorem in Martin-Löf type theory using Agda. Details on ualib.gitlab.io. (https://nest.jakl.one/notes/2021-01-25-l2akz/)
Server run by the main developers of the project 
It is not focused on any particular niche interest - everyone is welcome as long as you follow our code of conduct!