Ciro Santilli @cirosantilli 35

The only one on GitHub. In RST and renders to HTML with image formulas.

Too "direct formula overload" at first look.

By the creator of SymPy, who works at Los Alamos National Laboratory and has a PhD in chemical physics: swww.linkedin.com/in/ondřej-čertík-064b355b/ Man, big kudos to this dude.

Previously on EdX: www.edx.org/learn/quantum-physics-mechanics/delft-university-of-technology-topology-in-condensed-matter-tying-quantum-knots "DelftX: Topology in Condensed Matter: Tying Quantum Knots".

But then they regained their sanity and put the source code on GitHub: github.com/topocm/topocm_content and is CC BY-SA.

Uses an ungodly combination of Jupyter notebooks and Pelican.

On September 2024, GitHub forbade our China Dictatorship auto-reply bot, the reason given is because they forbid comment reply bots in general. Though it was cool to see a junior support staff person giving out what obviously triggered the action:before a more senior one took over.

Ciro was slightly saddened but not totally surprized by the bloodbath against him on the Reddit the threads he created:

So we observe once again the stupidity of deletionism towards anything that is considered controversial. The West is discussion fatigued, and would rather delete discussion than have it.

We also se people against you having freedom to moderate your own repositories as you like it, with bots or otherwise. Giving up freedoms for nothing, because "bot is evil".

Announcements:

Long story short, the project is so far a complete failure on the most important metric: number of regular users, which current sits at exactly one: myself.

There were notable users who found the project online and who actually tried to use the website for some content and provided extremely valuable feedback:Unfortunately after the period of a few weeks they stopped using it to follow their other priorities instead. Which is of course totally fine, however sad.

I still believe that the OurBigBook Web feature is a significant tech innovation that could make the website go big.

I also believe that the project gets many fundamentals of braindumping right, notably the infinitely deep table of contents without forced scoping, e.g.:does not make Calculus have an ID orr URL of mathematics/calculus, rather it's just calculus.

But there is a fundamental difficulty in reaching critical mass to that self-sustaining point, as people don't seem to be convinced by these logical "my system is better" argument alone, as opposed to having them Google into stuff they need now and then understand that the project is awesome.

A closely related critical mass issue is that existing big multiuser knowledge base websites such as Stack Overflow and Wikipedia have a tremendous advantage on PageRank. No matter how useless a Wikipedia article about something is, it will always be on top of Google within a week of creation for title hits. And since the main goal of publishing your stuff is to get it seen, it makes much more sense for writers to publish on such existing websites whenever possible, because anywhere else it is way way less likely to be seen by anybody.

Even I end up writing way more on Stack Overflow than on OurBigBook as a programmer. But I still believe that there is a value to OurBigBook, for the usual reasons of:

Perhaps what saddens me the most is that even on GitHub stars/Twitter/Hacker news terms there is almost no interest in the project despite the fact that I consider that it has innovations, while many other note taking apps as well in the thousands of stars. Maybe I'm just delusional and all the tech that I'm doing is completely useless?

Part of the issue is probably linked to the fact that most other note taking apps focus on "help me organize my ideas so I can make more money" and often completely ignore "I want to publish my knowledge", and stuff that helps you make money is always easier to sell and promote.

OurBigBook on the other hand a huge focus on "I want to publish me knowledge". It aims almost single mindedly in being the best tool ever for that. However this doesn't make money for people, and therefore there are going to be way less potential users.

I do believe strongly that all it takes is a few users for the project to snowball. For some people, once you start braindumping, it is very addictive, and you never want to stop basically. So with only a few of those we can open large parts of undergrad knowledge to the world. But these people are few, and so far I haven't been able to find even a single one like me, and on top of that convince them that I have created the ultimate system for their knowledge publishing desires.

Another general lesson is that I should perhaps aimed for greater compatibility with existing systems such as Obsidian. Taking something that many people already know and use can have a huge impact on acceptance. E.g. anything that touches Obsidian can reach thousands of stars: github.com/KosmosisDire/obsidian-webpage-export. Note taking apps that aim for "markdown" compatibility also tend to fare better, even if in the end you inevitably have to extend the Markdown for some of your features. And WYSIWYG, which I want but don't have, is perhaps the ultimate familiarity.

Another issue compared to other platforms is that OurBigBook just came out late. Obsidian launched in 2020. Roam Research and Trillium Notes also came earlier. And it is hard to fight the advantage already gained by those on the "I'm going to take some personal notes" area. I do believe however that there a strong separation between "these are my personal notes" and "I want to publish these". Once you decide to publish your knowledge, you immediately start to write in a different way, and it is very hard to convert pre-existing "private" notes into ones suitable for public consumption.

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:

You can always learn pure theory later on for free or very cheap from books.

And above all, you can always learn software engineering later on for free, because the programming community is so much more open than any other so far, notably e.g. with Stack Overflow and GitHub, see also: Section "Ciro Santilli's Open Source Enlightenment". Ciro Santilli is trying to change that with OurBigBook.com, but don't hold your breath. But it is increasingly hard to understand why there isn't an university that forces teachers to publish all their notes and lecture videos (which should be mandatorily recorded) with a Creative Commons License, and then let anyone take whichever exams they want for a small fee or for free.

Actually, there is a good chance you will learn to program, like it or not, because chances are that you won't be able to find as decent a job doing anything else.

But there is one thing you cannot learn for free: laboratory work. Laboratory work is just too expensive to carry out outside of an institution.

Basically, if you don't do laboratory work in undergrad, you will very likely never be able to do so in your entire life.

Because laboratories are so rare and expensive, it is laboratories that put you in the best most unfair position at creating world changing deep tech startups, which is why when in doubt, choose the course that has the most experimental work. Yes, you won't be able to achieve those insanely concentrated equities of the early-Internet, as you will need more venture capital to run your company, but those days are over now, deal with it.

Commit: github.com/cirosantilli/cirosantilli.github.io/commit/794705a201a79b5128934e69df85e3511655c03f

As Ciro started getting a lot of comments on his home page about China, he decided that Disqus does not scale, and that it would be more productive long term to remove it and point people to GitHub issues instead.

Upsides of removal:

Downsides:

Ciro's stance towards China hasn't changed, and China comments and corrections about his website are still welcome as always.

Related issue: github.com/cirosantilli/cirosantilli.github.io/issues/37