List of proof assistants

Source code:

They are huge fans of Unicode characters! Check this out from a formal proof of the prime number theorem: github.com/AlexKontorovich/PrimeNumberTheoremAnd/blob/fbdbb5310d036d33b9797b35f3b04b08f2447a6e/PrimeNumberTheoremAnd/ZetaBounds.lean

Their dependency graph thingy is just beautiful however: alexkontorovich.github.io/PrimeNumberTheoremAnd/web/dep_graph_document.html

This used to have the best name ever allowing you to say:to English speakers and watch their faces drop.

But in 2023 the bastards renamed it to "Rocq", presumably pronounced "rock". Why, God, why.

This will never work but OK. New custom language after Lean.