Ubuntu Updated 2025-03-28 +Created 1970-01-01
View more
Ciro Santilli's Linux distro of choice as of 2019.
It ain't perfect, but it's decent enough.
The greatest advantage of it being that it has the likely largest desktop user base, and therefore the highest likelihood that your problems are solved on Ask Ubuntu, and goes together with Ciro's philosophy that "people should do everything in the same way to factor stuff out", especially the open source losers.
Ciro considers that the killer flaw of Ubuntu, and most desktop distros of 2020, is that no one under the Sun knows how to build them fully from source: Linux distribution buildable from source. This is why Ciro based the Linux Kernel Module Cheat on Buildroot, see also: Linux distribution buildable from source.
Read the full article
I ended up doing tech rather than content as usual Updated 2025-03-28 +Created 2025-03-08
View more
At first I had intended to create a lot more content for the world class university located where I lived, but I ended up not doing that and just improving the project tech instead.
There are a few reasons for this, good or bad:
  • as a tech nerd, my natural tendency is to first sit down by myself and code to solve big general problems rather than go out and try to solve specific people's specific problems to obtain money and users
  • at one point I got the feeling that helping students with a bunch of small courses might be useful, and that instead I might get more impact by instead by focusing on creating content for a next big thing area such as:
    because many of the courses are fundamentally useless by design due to misalignment between university and reality.
    I'm still not sure what to do about that, but I do think I'll try to do a bit of course solving at least and see how it goes.
    One thing I've learned first hand through Ciro Santilli's Stack Overflow contributions and Linux Kernel Module Cheat is that the barrier to make money from a useful open source learning project that benefits a large number of people a little bit is huge, perhaps infinite, and that it might be better to instead focus more intensely on fewer users. This insight pushes me more towards going for solving local courses.
    Another consideration that supports going for courses is that being close to students is perhaps my only unfair advantage. There is likely no one else in the world in the same position that I'm at, with some "free time" to chill with undergrads and help them with 100% of my undivided attention and passion.
    A point that pulls me towards the big tutorials however is that my time is almost up, and focusing on them would increase the chances that I will be work in those fields afterwards. This feeling may go against the best interests of the project, but it is perhaps an inevitable self preservation consideration unless someone decides to free me from that forever with the 2M :-)
  • the entry barrier to help students of a top university is rather high. The students are already extremely busy and pressured (this is pe), and if it is in the slightest hard to explain their problems to you because you are not fluent enough in their subject, they will find a faster way to obtain the knowledge and never come to you.
  • I also did a bit of procrastinating with a few quick few exploration into cute programming projects. Nothing too crazy long however, just the usual. It's in my nature to have broad interests, and perhaps only such a person can make a OurBigBook.com. I'm not a fast worker. But I never stop. Once something is in my "this must be done or learnt list", I just keep coming back to it again and again until it happens.
The downsides of going for tech first are severe:
  • you risk being misaligned with what users want and spend enormous amounts of time on useless features
  • it is also rather demotivating that you are working hard on a really cool feature but you know that there are no users yet so no one will benefit from it, and that this feature alone is not enough to attract the users anyways
There are however counterpoints to these as for anything else:
  • I'm a user and I'm always improving it for myself. If there are other people like me out there, they will love it. If there aren't, perhaps I'll never be able to do anything that caters for them well enough anyways.
  • as the two users made me understand, once someone touches your thing, they expect it to be perfect, and their standards are extremely high. This is understandable in part given the large number of note taking apps in existence, and notably WYSIWYG ones. As such, there is some rationale for improving tech.
Read the full article
Website front-end for a mathematical formal proof system Updated 2025-03-28 +Created 1970-01-01
View more
When Ciro Santilli first learnt the old Zermelo-Fraenkel set theory and the idea of formal proofs, his teenager mind was completely blown.
Finally, there it was: a proper and precise definition of mathematics, including a definition of integers, reals and limits!
Theorems are strings, proofs are string manipulations, and axioms are the initial strings that you can use.
Once proved, press a button on your computer, and the proof is automatically verified. No messy complicated "group of savants" reading it for 4 years and looking for flaws!
There are a few proof assistant systems with several theorems in their Git tracked standard library. The hottest ones circa 2020 are:
And here are some more interesting links:
However, as expressed by the QED manifesto, is unbelievable that there isn't one awesome and dominating website, that hosts all those proofs, possibly an on the browser editor, and which all mathematicians in the world use as the one golden reference of mathematics to rule them all!
Just imagine the impact.
Standard library maintainers don't have to deal with the impossible question of what is "beautiful" or "useful" enough mathematics to deserve merged: users just push content to the online database, and star what they like!
We then just use GitHub-like namespaces for each person's theorem, e.g. "cirosantilli/fundmaental-theorem-of-calculus" or "johndoe/fundmaental-theorem-of-calculus" so that each person owns their own preferred definition IDs, which others can reuse.
No more endless bikeshedding over what insane level of generality do your analysis theorems need to be (Ciro Santilli attended at talk about Lean where the speaker mentioned this was a problem)!
This would move things more out of the "pull request and Git tracked code" approach, into a more "database with entries" version of things.
Furthermore, it is just a matter of time until the "single standard library" approach starts to break down, as the git clone becomes impossibly large. At this point, people have to start publishing separate packages. And when this happens, you would need to retest every package that you add to your project. This is why a centralized database is just inevitable at some point, it just scales better.
Interested in a conjecture? No problem: just subscribe to its formal statement + all known equivalents, and get an email on your inbox when it gets proved!
Are you a garage mathematician and have managed to prove a hard theorem, but no "real" mathematician will read your proof because your unknown? Fuck that, just publish it on the system and let it get auto verified. Overnight fame awaits.
Notation incompatibility hell? A thing of the past, just automatically convert to your preferred representation.
Such a system would be the perfect companion to OurBigBook.com. Just like computer code offers the backbone of Linux Kernel Module Cheat Linux kernel tutorials, a formal proof system website would be the backbone of mathematics tutorials! You know what, if OurBigBook.com becomes insanely successful, Ciro is going to add this to it later on.
Furthermore, it would not be too hard to achieve this system!
All we would need would be something analogous to a package registry like PyPI or NodeJS' registry.
Then, each person can publish packages containing proofs.
Packages can rely on other packages that contain pre-requisites definition or theorem.
Packages are just regular git repos, with some metadata. One notable metadata would be a human readable description of the theorems the package provides.
The package registry would then in addition to most package registries have a CI server in it, that checks the correctness of all proofs, generates a web-page showing each theorem.
All proofs can be conditional: the package registry simply shows clearly what axiom set a theorem is based on.
This is a close as we can get to Erdős' book.
Maybe Ciro will just stuff this into OurBigBook.com once that takes over the world.
This project could be seen as a more automated/less moderated version of ProofWiki.
Bibliography:
Ciro Santilli pinging people:
Read the full article
x86 bare metal examples Updated 2025-03-28 +Created 1970-01-01
View more
As mentioned at Section "Linux Kernel Module Cheat", this should be merged into that other project.
Read the full article