In any case, the outcome of that is that the tech has improved. And I have done a relatively good job of clearly publishing any "more user visible" improvements to docs.ourbigbook.com/news and social media such as though it is important to note that there have been more than one "fix a hard bug" weeks that were not published because they would just bore readers.
During this period the main focus has been on improving OurBigBook Web, i.e. the dynamic website that powers OurBigBook.com. There are two reasons for that:As a result, Web is now way less buggy and much more usable.
- Web is what has the OurBigBook topics feature for mind-melding, which is the killer feature of OurBigBook compared to other note taking apps and therefore deserves the highest levels of priorityStatic website generation is an indispensable escape valve that ensures that your content can be published forever even if OurBigBook.com goes down one day, which it won't as long as I live. But the innovation is Web.
- static website generation was closer to good enough, but web was much further and is fundamentally harder.I'm extremely satisfied with OurBigBook static website generation and haven't touched it as much. It wasn't easy to reach this state, but I'm there.But Web is a different and much more complex beast.Making CLI software that will run on a person's local computer under full trust and building a bunch of HTML from lightweight markup in bulk is one thing.But making a public dynamic website that has to continuously maintain a coherent database state on granular updates, while giving users some trust but not enough for them to blow everything up is on a totally different level. See e.g. the recent SPAM attack we've had to fend off.And then there's also the issue of front-end being mega-hard to get right.
If you look through the list of Web updates, there is nothing specifically mind blowing. The core ideas have largely crystallized, and we are just trying to making them click. I have a few more punches up my sleeve, but the core is decided.
OurBigBook Web search
. Source. This is one of the many basic quality of life improvements that have been done on OurBigBook Web.OurBigBook Web article announcement
. Source. Another cute new feature, you can send an email to your followers about a new amazing article you created.Web process has been somewhat slower than what I'd like. Of course, it is the case of any project that things are easily said than done. But there are two other main structural factors that have played into it:
- For example, we could have put him on childcare a bit earlier, but due to inexperience we've kept him a bit longer than we maybe should have.Things are well sorted out now, but not matter how good your support system is, at the end of the day, and more often night, it is you the parents that have to deal with a lot of inevitable baby issues. Unless you want them to turn into psychopaths and drug addicts that is, which I don't. I've reached the point of semi failure middle age that the baby feels like my best moonshot.But at least with the donations I was able to work on OurBigBook at all. Because if it weren't for that, I would have to focus entirely on the generic job instead and OurBigBook would have been put on hold.
- the choice of Web stack. I was allured by Next.js. I can see the beauty and usefulness of a Node.js render front-end that also runs on backend and hydration. That is awesome.But:
- React is insanely hard to learn and understand. Furthermore, it is also hard to understand the performance problem that it solves, and actually have a benchmark where this problem is solved faster than just delivering some HTML files with ad-hoc Js on top.
- the lack (or perhaps excess of shitty) actual web framework like Ruby on Rails and Django means that I have to rediscover the wheel many times over for all the essential support activities like testing, login and so one
At this point a rewrite is out of the question. I've managed to master things well enough to get a decent result, and given up on the few things that I couldn't for the life of me achieve, after documenting them very well for posterity of course.
Aside from Web, there was only one thing that received a significant improvement, and that was the OurBigBook VS Code extension. The extension is not perfect, and it is not the "final UI", which has to be some WYSIWYG implementation, and there are some fundamental limitations that cannot be overcome without patching VS Code itself. However, the extension is already extremely usable, and I'm writing this on it right now. Basics like syntax highlighting, jump to definition and autocomplete are very useful and usable.
Tree navigation in the OurBigBook Visual Studio Code extension
. Updates I ended up doing tech rather than content as usual Updated 2025-05-23 +Created 2025-03-08
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:There are however counterpoints to these as for anything else:
- 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
- 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.
It is unbelievable that you can't find easily on YouTube recreations of many of the key physics/chemistry experiments and of common laboratory techniques.
Experiments, the techniques required to to them, and the history of how they were first achieved, are the heart of the natural sciences. Without them, there is no motivation, no beauty, no nothing.
School gives too much emphasis on the formulas. This is bad. Much more important is to understand how the experiments are done in greater detail.
The videos must be completely reproducible, indicating the exact model of every experimental element used, and how the experiment is setup.
A bit like what Ciro Santilli does in his Stack Overflow contributions but with computers, by indicating precise versions of his operating system, software stack, and hardware whenever they may matter.
It is understandable that some experiments are just to complex and expensive to re-create. As an extreme example, say, a precise description of the Large Hadron Collider anyone? But experiments up to the mid-20th century before "big science"? We should have all of those nailed down.
We should strive to achieve the cheapest most reproducible setup possible with currently available materials: recreating the original historic setup is cute, but not a priority.
Furthermore, it is also desirable to reproduce the original setups whenever possible in addition to having the most convenient modern setup.
Someone with enough access to labs has to step up and make a name for themselves through the huge effort of creating a baseline of amazing content without yet being famous.
Until it reaches a point that this person is actively sought to create new material for others, and things snowball out of control. Maybe, if the Gods allow it, that person could be Ciro.
Tutorials with a gazillion photos and short videos are also equally good or even better than videos, see for example Ciro's How to use an Oxford Nanopore MinION to extract DNA from river water and determine which bacteria live in bacteria for an example that goes toward that level of perfection.
The Applied Science does well in that direction.
This project is one step that could be taken towards improving the replication crisis of science. It's a bit what Hackster.io wants to do really. But that website is useless, just use OurBigBook.com and create videos instead :-)
We're maintaining a list of experiments for which we could not find decent videos at: Section "Physics experiment without a decent modern video".
Ciro Santilli visited the teaching labs of a large European university in the early 2020's. They had a few large rooms filled with mostly ready to run versions of several key experiments, many/most from "modern physics", e.g. Stern-Gerlach experiment, Quantum Hall effect, etc.. These included booklets with detailed descriptions of how to operate the apparatus, what you'd expect to see, and the theory behind them. With a fat copyright notice at the bottom. If only such universities aimed to actually serve the public for free rather than hoarding resources to get more tuition fees, university level education would already have been solved a long time ago!
One thing we can more or less easily do is to search for existing freely licensed videos and add them to the corresponding Wikipedia page where missing. This requires knowing how to search for freely licensed videos:
- Wikimedia Commons video search, e.g.: commons.wikimedia.org/w/index.php?search=spectophotometry&title=Special:MediaSearch&go=Go&type=video
- YouTube creative commons video search
Related:
- relevant University YouTube channels:
- K-12 demo projects:
- books:
- Practical approach series by Oxford University Press: global.oup.com/academic/content/series/p/practical-approach-series-pas
2023-11-17 bitcointalk.org/index.php?topic=5478677.0 "I Bought vistomail.com. Now What?" Restricted topic, but Google caught it: archive.ph/wip/dDxqi The message:
I am dedicating the next few months, and perhaps even years, to researching Satoshi Nakamoto and the intricacies of blockchain technology. About four weeks ago, I came across vistomail.com for sale on afternic.com and decided to purchase it. I added vistomail.com to my proton.me account and configured it to catch all emails. As a result, numerous emails started flowing in. Subsequently, I connected satoshi@vistomail.com and discovered significant information that I am excited to share with you in the coming months.To be clear, I want to emphasize that I am not Satoshi Nakamoto. My interest lies in understanding the future plans for Bitcoin and its impact on the world. I invite you to join me on this journey, contributing your knowledge to the collective understanding. I believe there is a possibility of uncovering the ultimate treasure, and I am eager to share it with all of you.twitter @alexelbanna
2023-11-17, 06:46:25 PM. bitcointalk.org/index.php?topic=5474482.0 vistomail.com for sale, Restricted topic, but Google caught it: archive.ph/wip/GARBy The message:
Email address: satoshi@vistomail.com$50,000 obo for vistomail.com. Buy Now: www.afternic.com/listings/778206How it would be of value:You would open a proton.me account add domain vistomail.com. Then you create an address such as: satoshi@vistomail.com and the you can set the domain to a catch all address. All satoshi@vistomail.com emails will come into your inbox. All emails from @vistomail.com going to vistomail.com will now be in your inbox.BUY NOW: www.afternic.com/listings/778206See other domains Satoshi Nakamoto owned here: www.afternic.com/listings/778206Michael Weber
Domain Registrar
mweber@dosidos.net
They updated the page to a more scammy one as of 2024: web.archive.org/web/20240310205138/https://www.vistomail.com/ mentioning x1coin.org. But still Alex no doubt: twitter.com/AlexElbanna/status/1763575552538001530 | github.com/bLeYeNk
As of 2024-04-10, it was now a Ghost blogging intance still by Alex: www.vistomail.com/articles-coming-soon/ He added Ciro Santilli as a collaborator, but Ciro could only draft articles which Alex could then review. He allowed a cheeky link to OurBigBook.com in: archive.ph/8l6az epic. Let's see if it gives traffic!
www.vistomail.com/non-profits/ claims they were giving out grants via satoshin@nt-medic.com and provided address 1BCwUg3PsLK9wJK815RkmzSMdAnALNHu64
Website front-end for a mathematical formal proof system Updated 2025-05-23 +Created 1970-01-01
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:
- github.com/HOL-Theorem-Prover/HOL
- github.com/seL4/isabelle. Rumours have it that this is "uncompilable" from source without blobs. It does however offer a very rich IDE.
- github.com/coq/coq
- Metamath this one is likely an older and less powerful system, but the web presentation and tutorial are very good! Source: github.com/metamath/metamath-exe Here is a proof that 2 + 2 equals 4: us.metamath.org/mpeuni/2p2e4.html
- Lean
- www.bookofproofs.org/branches/fpl-formal-proving-language/ from BookofProofs
And here are some more interesting links:
- github.com/awesomo4000/awesome-provable an awesome list of formal stuff
- devel.isa-afp.org/ Isabelle Archive of Formal Proofs. A curated list of Isabelle proofs, with minimal web UI. This is almost what we need, but without the manual curation, and with a better web UI.
- www.cs.ru.nl/~freek/100/ list of how many of the "arbitrarily" selected the Hundred Greatest Theorems by Paul and Jack Abad (1999) had been proved in several formal systems, serving therefore as a benchmark of sorts
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!
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.
Maybe Ciro will just stuff this into OurBigBook.com once that takes over the world.
Bibliography:
- The Math Genome Project has very similar end goals. Apparently it will run proofs on server against the stdlib, but not allow one proof to depend on another, so in the end you still have to pull request everything back. Also there may be moderation forever, unclear. Ciro tried to create a dummy lolol theorem without any correct syntax and it just became private. Also apparently every single proof needs corresponding LaTeX manually written to be accepted. Cowards!
- math.stackexchange.com/questions/1767070/what-is-the-current-state-of-formalized-mathematics/3297536#3297536
- math.stackexchange.com/questions/2747661/why-is-there-not-a-system-for-computer-checking-mathematical-proofs-yet-2018
- stackoverflow.com/questions/19421234/how-do-i-generate-latex-from-isabelle-hol
- stackoverflow.com/questions/30152139/what-are-the-strengths-and-weaknesses-of-the-isabelle-proof-assistant-compared-t
- arxiv.org/abs/2102.03044 SPIRG, a decentralized version of this
- proofnet.org/: ChatGPT pointed Ciro Santilli to this, but it has like 4 broken archives? web.archive.org/web/20220523140733/http://www.proofnet.org/ Does it really exist or is it just hallucination? There is a AI Math benchmark with that name though: arxiv.org/abs/2302.12433
- formalabstracts.github.io/ is an idea without implementation. By mathematician Thomas Callister Hales.
Ciro Santilli pinging people:
- mastodon.social/@cirosantilli/114201226569666331 Terence Tao, why not, he's interested in formal!
What poor countries have to do to get richer Make your education system more efficient Updated 2025-05-23 +Created 1970-01-01
As Ciro has rambled infinitely at Section "University", the school system is hugely inefficient and a waste of time for everyone involved.
Instead, just use Section "OurBigBook.com" instead.
When in doubt, choose the course that has the most experimental work Updated 2025-05-23 +Created 1970-01-01
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.
Because when this gets converted to a OurBigBook.com page, it will be easier for people to copy paragraphs/fork and write a canonical page about Ciro.
What do you do when creating a pull request? Do you say "I", which is not true because Ciro did not say that, or do you say "John Doe thinks" bla bla?
And because his name is awesome! :-) Just kidding.
This became a micro-meme in 4chan:Correction: cirosantilli.com is not Ciro Santili's resume. It is your life.
- 2020-09-21 archive.vn/wip/Zz7fx (original) "ITT: weird sites you found by accident" a comment reads:
cirosantilli.com/ this is some guys resume who repeats his own name well over 1,000 times.
- 2020-04-30 archive.is/LgDbK (original) "Interesting Website thread" a comment reads:cirosantilli.com/ What is even this?
OMG they have that. Slightly slightly overlap with OurBigBook.com.
The pre-Eternal September feeling is palpable.
People could freely comment their thoughts and sign below, making it much closer to what Ciro Santilli wants OurBigBook.com to be. But with upvotes ;-)