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. (nest.jakl.one/notes/2021-01-25)

Sign in to participate in the conversation
Mastodon

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!