Incoming links: Ciro Santilli
Those guys are really good, Ciro Santilli especially enjoyed their quantum mechanics playlist: www.youtube.com/playlist?list=PL193BC0532FE7B02C
The quantum electrodynamics one was a bit too slow paced for Ciro unfortunately, too much groundwork and too little results.
Ciro Santilli used to play video games when he was young. But after he reached 18 he got bored of them.
The problem is that no matter how you look at, the how to become famous in the real world game is just always more interesting and fulfilling.
Therefore adult Ciro enjoys only the following types of video game content in video form, so that other people waste their lives playing the games while you only see the highlights:
- speedrunning, including:
- tool-assisted speedrun, Ciro's favorite by far
- real-time attack speedrun
- meta breaking glitches, including in speedrunning and on PvP-games.
- Magic: The Gathering
- Video game reviews
The aspect Ciro enjoys about non-PvP games is atmosphere. Not as conveyed by useless story telling, but as conveyed by music and graphics, and the context deep idea. Legend of Zelda and Metroid come to mind.
And too many games commit the sins of dependency of dexterity, no save states, how do I skip this boring part, or jump straight to the beautiful one?
Another important point is; the perfect video game is an infinitely hard one.
It also doesn't help if you are already typing on a computer all day long on your job. Hands get tired. Eyes have an infinite capacity to consume useless YouTube videos however. Medically proved.
As a result, Ciro just watches videos about video games. Notably games he played when he was a teenager and already understand the rules for.
And things got even worse as after Ciro Santilli's Open Source Enlightenment, and he started to feel bad about playing any game that is not open source.
Supercut of Doug S02E13 "Doug's Lost Weekend" (1992)
Source. Ciro Santilli used to watch Doug as kid. Of all the episodes, only this one stuck to his mind as an adult. It really drove the point home. The pain and joy of being addicted to anything really. Thankfully wheneve Ciro got addicted to a video game, he also quickly got tired of it. His last temporary addiction episode as of 2022 was Cataclysm DDA!
It is also so awesome how the episode pictures Dougs imagination while playing the video game, which is much more realistic than the actual crude graphics. The Nintendo hard reference is also clear.
Another great point of the episode is how good it is to play a single player video game taking turns with a friend on your side. Both people have to be fully engaged, and the game has to be hard. Perhaps those days are over now that everyone has their own computer and can each play together... and that is a huge shame. When playing on the couch with a friend, the one who is not playing can act as a copilot and thing more broadly as the other focuses on more specific details of execution. One is also reminded of pair programming.
Another great point is, partially when you are addicted, to play the video game at night until late, or very early in the morning. Ciro has fantastic memories of playing Zelda on the Nintendo 64 on Sunday mornings, or his emulation experiences from late weekend evenings at university: Video "Samba e Amor by Caetano Veloso (1975)".
The followup lucky hat segment is also amazing: doug.fandom.com/wiki/Doug%27s_Lucky_Hat
Ciro Santilli's favorites are:He used to also play some first-person shooters as they can be fun to empty your brain.
Some that Ciro Santilli likes:
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
This is the most accessible DNS database online, as it does not require login or payment.
They have reasonable data. It's not fully complete as Ciro Santilli saw on CIA 2010 covert communication websites, but it is very valuable.
Tested as of 2025, they seem to have removed the pre-IP checks on web interface, and just instead use Cloudfare to check that you are human from time to time, which allows for a lot manual searching to be done! Awesome!
Previously, tou could only get about 250 queries on the web interface, then 250 queries per free account via API. They check your IP when you signup, and you can't sign in twice from the same IP. They also state that Tor addresses are blacklisted. They also normalize dots in gmail addresses, so you need more diverse email accounts. But they haven't covered the
.gmail vs .googlemail trick.Their data is also quite disjoint from the data of the 2013 DNS Census. There is some overlap, but clearly their methodology is very different. Some times they slot into one another almost perfectly.
Talks about rebellion of the oppressed (and bandits), and therefore has been controversial throughout the many Chinese dictatorships.
The book is based on real events surrounding 12th century rebel leader Song Jiang during the Song dynasty.
It is also interesting that Mao Zedong was apparently a fan of the novel, although he had to hide that to some extent due to the controversial nature of the material, which could be said to instigate rebellion.
The incredible popularity of the novel can also be seen by the large number of paintings of it found in the Summer Palace.
This is a good novel. It appeals to Ciro Santilli's sensibilities of rebelling against unfairness, and in particular about people who are at the margin of society (at the river margin) doing so. Tax the rich BTW.
It also has always made Ciro quite curious how such novels are not used as a way to inspire people to rebel against the Chinese Communist Party.
Full text uploads of Chinese versions:
- www.gutenberg.org/cache/epub/23863/pg23863.html No table of contents.
- Suikoden, JRPG that Ciro Santilli played that one when he was a teenager!
Obviously coupled with measures to prevent capital flight. This would be a required step to achieve Ciro Santilli's dream of unconditional basic income.
Why don't the poor vote in mass for it is incomprehensible considering e.g. the wealth inequality in the United States as of 2020!
Perhaps the election of Donald Trump in 2016 woke up the democrats at last, that they were just making empty promises without actually benefiting the poor? www.vox.com/2019/3/19/18240377/estate-tax-wealth-tax-70-percent-warren-sanders-aoc. Or is just another facade?
Bibliography:
- www.npr.org/sections/money/2019/02/26/698057356/if-a-wealth-tax-is-such-a-good-idea-why-did-europe-kill-theirs If a Wealth Tax is Such a Good Idea, Why Did Europe Kill Theirs?
- www.youtube.com/watch?v=XzonR81vVzM The Mayfair Set, Episode 2 - Entrepreneur Spelt S.P.I.V. (1999) by Adam Curtis explains nicely how in the 60's, Jim Slater bought stock of inefficient companies, and sold off inefficient assets to make a profit.He managed to do that because previously people had regarded those companies as family companies, and never looked into the fact that they families weren't actually majority shareholders anymore.While this increased efficiency, it also fired many people, and the government didn't manage to change legislation fast enough to tax those profits to increase welfare.
The remedy to cowardice, inattention, censorship and amorality.
Due to Ciro Santilli's campaign for freedom of speech in China, Ciro Santilli maintains information on this at mostly at:
Dan Dascalescu's "Web page archiving" comparison table: web.archive.org/web/20130922192354/http://wiki.dandascalescu.com/reviews/online_services/web_page_archiving
Without me, my stack is useless. Without my stack, I am useless. I must fire my requests true. I must shoot straighter than my hackers who are trying to kill me. I must shoot him before he shoots me. I will ...My stack is human, even as I am human, because it is my life. Thus, I will learn it as a brother. I will learn its weaknesses, its strength, its parts, its accessories, its ORMs and its asset bundlers. I will keep my stack clean and ready, even as I am clean and ready. We will become part of each other. We will ...
Explanation: this is an allusion to the Rifleman's Creed. This particular version talks about the website stack chosen for a website, i.e. the libraries used.
Ciro Santilli has always felt that choosing a stack is an almost religious choice. It is perhaps part of why the prayer style of the original Rifleman's Creed resonates with the web stack choice.
It is very hard to know how things are going go, the ups and downs, before putting big hours into it.
And once you start, it is hard, though not impossible, to move away.
A quick hands-on introduction to the software by Ciro Santilli can be found at: github.com/cirosantilli/cirosantilli.github.io/issues/198
- www.trussel.com/ Stephen (Kepano) Trussel. Started mega early in 1996 until his death in 2020. First found by Ciro Santilli due to his Inspector Maigret section: www.trussel.com/f_maig.htm
Website front-end for a mathematical formal proof system Updated 2025-06-02 +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!