Source code:
- github.com/leanprover/lean4 why a separate repo per version... but it is what it is.
- github.com/leanprover/lean
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
Kudos for being a not-for-profit. Also, anyone can create content: e-learning websites must allow students to create learning content. Oh, but TODO is possible for anyone to make content publicly visible? Course join links lik: www.khanacademy.org/join/MJZ6NSV7 require login. webapps.stackexchange.com/questions/165132/how-to-create-a-course-that-is-publicly-visible-without-the-need-to-login-on-kha If that's the case, it is a fatal flaw not shared by OurBigBook.com.
Another cool aspect is that they have the "physical world teacher pull student accounts in" approach built-in quite well at course creation. This is a very good feature.
As of 2021 they were a bit struggling for money it seems: www.youtube.com/watch?v=I8XdUy-wyyM?
FBI vs Un-Defuseable Bomb by Qxir (2021)
Source. Tells the story of Harvey's Resort Hotel bombing (1980)See: exam.
There are unlisted articles, also show them or only show them.