Incoming links: Ciro Santilli
- 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
Website front-end for a mathematical formal proof system Updated 2025-04-18 +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!
Many East Asians, notably Chinese immigrants, choose to adopt a Western name pseudonym to make it easier for Western people who don't speak the language to call them and remember their name.
Cowards! Ciro Santilli would much rather just torture foreigners into learning his language. But fair play.
More interestingly however, some of the names chosen are not typical names, and some end up being very cute or mildly funny. Perhaps it is partly linked to given names are getting weirder.
Like all poor countries, Brazil's lack of money and scientific culture severely limit its ability to make technological and scientific advances.
While this sounds obvious, Ciro Santilli has felt it first hand since he moved from Brazil to Europe, and it is just shocking.
Don't force international exchange students to come back early Updated 2025-04-18 +Created 1970-01-01
Many of the student exchange programs Ciro witnessed in the 2010's in Brazil were inefficient because they were requiring students to come back immediately after university or PhD in fear that those students will never come back.
This is useless, because you don't learn anything unique during university: the truly valuable knowledge is obtained when you work for several years as a postdoc in a world class research laboratory or as an engineer in a world class company.
Therefore, Brazil should learn from the Chinese exchange system, which lets students go do whatever they want, and once they are Gods of the domain, entices them back with great positions and pay as heads of laboratory back in China. Just don't do fraudulent stuff like this like China did, or else you will get a bad rep.
To help this university collaboration happen, we should create communication channels between exchange students and professors of the origin country who work on the same domain so that they can discuss the subject. For example, once Ciro Santilli wanted to contact some of his former teachers at the University of São Paulo about "advanced" topics he had been exposed to as part of his job. However, they didn't even reply to his email, and Ciro didn't know who else to contact. This must never happen. We need a way to informally contact several professors of a given domain informally, to increase the chances that at least one might be interested. It is pointless to just let students loose abroad and hope that they will bring things back to their home country: a more cohesive infrastructure is needed to nurture that.
There is basically one sane way to achieve these goals: the exchange programs must be organized at a national level, not in an ad-hoc per-university manner.
Another good idea is to have taxes that depend on your nationality alone and which only start collecting when you reach a very high amount of net worth. So e.g. if someone leaves the country and makes it big, then and only then does the Government starts clawing back the benefits of its investments in the person. Furthermore, such taxes could be reduced if the person brings some of the business back to the country. And mandatory taxes should be charged if the person decides to drop their nationality at some point.
The above points would also be greatly eased by having a national-level exchange program. E.g. in Brazil in the 2010's which Ciro experience, every university had different terms and conditions, which made everything a mess. Exchange programs must be treated as a unified federal policy.
Ciro actually had to return for just six months from the École Polytechnique to the University of São Paulo, to finish a course he had only done the generic Maths/Physics introduction to. Students from other Brazilian universities were forced to return for up to 3 years even to get their Brazilian diplomas! Ciro was lucky that his teachers understood the situation, and allowed him to develop online learning projects instead of his supposed control engineering projects, which hopefully will have led to changing the world with motivation one day. And for this, Ciro is eternally thankful.
This shows the complete and total lack of any Brazilian strategy to send its students abroad to really learn valuable things and then come back. There is no strategy at all. Things have just reached an equilibrium point of bureaucracies, Brazilian universities trying to bring students back to validate useless diploma pieces of paper, and foreign universities no caring about that, and just wanting the students to say abroad forever.
Ciro was once talking about why so few Brazilians go study abroad compared to the Chinese. Besides the likely true "there are a lot of Chinese" argument, his wife made another: good point Brazil is not so bad to live in, because you have good food and freedom, while China only has good food.
But Ciro still fells bad that so few of his University of São Paulo colleagues, who learnt automation and control engineering, are doing deep tech. Nor physical engineering. They have all basically become computer people like Ciro.
This is not their fault. They basically don't have a choice: all physical science and technology is done in rich countries.
Yes, someone has to implement the newest tech to improve local country efficiency in projects that will never spread abroad.
But who will be left then for the next big thing problems that would really make Brazil richer? 6 out of 30 person class ended up working on a gaming company at one point, even though they were not crazy passionate about the field! What could possibly be a worst investment for society?
This lack of technological innovation can also be clearly seen when you research investment options available in Brazil. Huge emphasis is put on fixed return financial products (often inflation adjusted) linked to base non-tech business such as housing market and agriculture. And when you look to the returns of the stock market on s&P 500-analogue backed exchange-traded funds, they do not seem obviously better, especially considering inflation and taxation benefits that exist for some of the other investment possibilities.
When the companies of a country are not clearly the best investment, you know that something is wrong. They are highly specialized money making machines, remember! And housing and agriculture are not such innovative markets where people can hugely influence efficiency.
When it is best to send students is a good question. Undergrad studies could be easily reproduced in poor countries if they had any intelligence at all, since even in rich countries laboratory usage is always limited. Masters and PhD are generally more valuable moments to send people out. The question is if the students will actually have a fighting chance without having been out, in particular in terms of language skills. Ciro feels that Masters are a good focus point for entry, as that is where PhD links are more actively done.
When in doubt, choose the course that has the most experimental work Updated 2025-04-18 +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.
Ciro Santilli started taking some notes at: github.com/cirosantilli/awesome-whole-cell-simulation. but they are going to be all migrated here.
It is interesting to note how one talks about single cell analysis, in contrast to whole cell simulation: experimentally it is hard to analyse a single cell. But theoretically, it is hard to simulate a single cell. This mismatch is perhaps the ultimate frontier of molecular biology.
Why are complex numbers used in the Schrodinger equation? Updated 2025-04-18 +Created 1970-01-01
This useless video doesn't really explain anything, he just says "it's needed because the equation has an in it".
The real explanation is: they are not needed, they just allow us to write the equation in a shorter form, which is always a win: physics.stackexchange.com/questions/32422/qm-without-complex-numbers/557600#557600
Why it takes several days to enter inflammatory phase in COVID-19? Updated 2025-04-18 +Created 1970-01-01
Why is it there such a clear separation of phases?
Why do people with mild symptoms go on to die? It is a great mystery.
Ciro Santilli's theory is that COVID is extremely effective at avoiding immune response. Then, in people where this is effective, things reach a point where there is so much virus, that the body notices and moves on to take a more drastic approach. This is compatible with the virus killing older people more, as they have weaker immunes systems. This is however incompatible with the fact that people don't seem to be contagious after the viral phase is over...
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 ;-)
The problem with virtually all sleeping masks on the market is that they leave a lot of room near your nose for light to come in.
Ciro Santilli discovered a useful workaround for that: make the mask tighter with a swimming goggles!
Just make the goggles as loose as possible to not put pressure on your eyes, and then strap them over the sleeping mask.
If you are a back sleeper, put the googles forward as normal. If you are a stomach sleeper, put the googles on the back of your head, and the straps over the mask. This way you wont get your head squished by the goggles and the bed.
Once Ciro understood the idea, Googling "swimming googles sleeping mask" led to: mantasleep.uk/ might be a good option.
Amazing self-directed learning direction:
world.hey.com/gwyn/no-excuses-bc4152fb mentions that the founder was inspired by other schools: High Tech High and Expeditionary Learning.
Lots of focus on showcase student work.
The founder Gwyn ap Harri is quite dirty mouthed, which is also cool.
Ciro Santilli tried to contact them in 2021 at: twitter.com/cirosantilli/status/1448924419016036353 and on website contact form to see if we could do some project together, but no reply.
OK, now we're talking, two liner and you get a window showing bounding box object detection from your webcam feed!The accuracy is crap for anything but people. But still. Well done. Tested on Ubuntu 22.10, P51.
python -m pip install -U yolov5==7.0.9
yolov5 detect --source 0