Ciro Santilli @cirosantilli 37

Ciro Santilli is fond of cynicism, see also ciro Santilli's film tastes.

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

Their 2025 current installation method is bullshit, recommends VS Code extension on Ubuntu. Lol.

From CLI:Then when you run:it downloads the lean executable for you. Insane shit, could only come from a Microsoft mindset.

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?

A form is a function from a vector space to elements of the underlying field of the vector space.

Examples: