Raoult's law is a principle in chemistry that relates to the vapor pressure of components in a solution. Specifically, it states that the partial vapor pressure of each component in an ideal solution is directly proportional to its mole fraction in the solution. In simpler terms, it means that the more of a particular component there is in a solution, the greater its contribution to the total vapor pressure of the solution.
Pullip is a type of doll that originated in South Korea. It was first introduced by the company Cheonsang Cheonha in 2003. Pullip dolls are characterized by their large heads, expressive eyes, and the ability to change eyes and make various facial expressions. They are typically made of plastic and have articulated bodies, allowing for a wide range of poses. Each Pullip doll has a unique design, often inspired by various themes such as fashion, fantasy, or anime.
Interatomic potential refers to the energy associated with interactions between atoms in a material. It describes how atoms in a substance affect one another through various types of forces, such as ionic, covalent, and van der Waals interactions. These potentials are crucial in computational physics and chemistry, as they allow researchers to model and predict the behavior of materials at the atomic level.
The Knudsen force refers to a phenomenon observed in systems where gas flows through a porous medium or around particles, particularly when the mean free path of the gas molecules is comparable to or larger than the characteristic dimensions of the flow obstacles, such as pores or particles. This condition is often encountered in micro- or nanoscale systems, where conventional fluid dynamics equations may not be sufficient to describe the behavior of the gas.
A **compact semigroup** is a mathematical structure that arises in the field of functional analysis and dynamical systems. To understand what a compact semigroup is, it's important to break down the concepts involved: 1. **Semigroup**: A semigroup is a set equipped with an associative binary operation.
Division by zero is an undefined operation in mathematics. To understand why, it's helpful to consider what division means. Division can be thought of as determining how many times one number (the divisor) fits into another number (the dividend). For example, if you divide 10 by 2, you are asking how many times 2 fits into 10, which is 5. However, when you try to divide any number by zero (e.g.
Metafont is a font definition language and a system developed by Donald Knuth as part of his TeX typesetting system. Introduced in the late 1970s, Metafont is primarily used to define and create bitmap fonts based on mathematical equations and descriptions. Unlike traditional font design, where fonts are typically created using graphical design tools, Metafont allows designers to specify a font's characteristics through a programming-like syntax.
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.
This would be a bit like erdosproblems.com, but with formal proofs. Note for example that Formal Conjectures has formalized these specific problems at: github.com/google-deepmind/formal-conjectures/tree/main/FormalConjectures/ErdosProblems
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.
- Registered domain
proofoverflow.com. - www.newton.ac.uk/event/bprw03/ 2025 Big Proof workshop at the University of Cambridge
Ciro Santilli pinging people:
- mastodon.social/@cirosantilli/114201226569666331 Terence Tao, why not, he's interested in formal!
Main section: fusion power.
An X-ray machine is a medical imaging device that utilizes X-rays to create images of the inside of the body. X-rays are a form of electromagnetic radiation, similar to visible light but with much higher energy. The machine operates by directing X-ray beams towards the body, and as the rays pass through, they are absorbed in varying degrees by different tissues based on their density.
Or: how to learn X.
That is the wrong question.
Then, once you decide to try one, if that involves programming, only then learn to program to achieve that goal. And don't stop learning what's needed until you either get the thing done, or decide that it is actually not a good idea, or not possible, or that there is something else more important to be done first.
But if doesn't involve programming, then don't learn to program, and learn whatever you actually need to reach that goal instead.
Having that goal is the only way to be motivated to do something.
This is the essence of backward design.
Another very important point to keep in mind is: Section "When in doubt, choose the course that has the most experimental work".
Ciro Santilli has mixed feelings about animal rights.
On one hand, his irrational side wants of course all animals to be happy.
On the other, he does not care about this enough to not kill and eat them, even though he believes that you could live off plants relatively well.
His more rational side says: humans are sacred. Either because you believe in the soul, or because your built-in empathy behaviours. If it is not a human, do whatever you want to it. Killing is already undoubtedly the greatest sin. It is not OK to kill a human painlessly is it? So if torturing it brings humans good, then do it.
Of course, this does get use close and closer to "the what is a human" question, which is more relevant than ever in the awakening of genetics: all species are after all a continuum right?
And Ciro does not have a simple solution to this problem, besides that in 99.9999% the answer is obvious to 99.9999% of the people, and for the others cases, we have to do it like the law and make flawed rules to cover the remaining 0.000099999% cases and let juries decide the rest.
The only other sensible sacredness barrier is the common vegetarian "nervous systems are sacred" one. But how can you believe that if you also follow the religion of physics, where everything is just made of atoms?
Is it evil to take one neuron and torture it? What does that even mean? It will be fun when pain and pleasure are fully understood.
And you are going to have a really hard time when mosquitoes start transmitting deadly diseases that kill your family.
Laws in most 2020 Western modern societies have converged to a hypocritical balance between not offending people too much by hiding the killing and minimizing the pain when possible at low cost. Killing animals painlessly is basically always fine if it brings any "non sadistic" pleasure to humans. And torturing animals is fine with approval e.g. to make medicines.
This has the downside of increasing costs for society. Maybe there are practical benefits besides people feeling bad about animals? Maybe we would have more serial killers if people were free to torture animals? Maybe people in butcher shops would become depressive if their bosses weren't forced to use more expensive painless killing methods? Neither of those seems like huge arguments though.
It eventually comes down to: "how much more is a human life worth than that of an animal" which brings Jesus's Matthew 6:25-34 "Do Not Worry" (archive) quote to mind:
Therefore I tell you, do not worry about your life, what you will eat or drink; or about your body, what you will wear. Is not life more than food, and the body more than clothes? Look at the birds of the air; they do not sow or reap or store away in barns, and yet your heavenly Father feeds them. Are you not much more valuable than they?
Non-vegetarian pets owners also baffle Ciro, as most of them basically extend the sacred human line further arbitrarily to certain other cute looking animals like dogs, cats or rabbits, but will gladly kill a cow indirectly by paying someone to pay someone to pay someone to cut it into small pieces. Or they believe that certain specific individuals are sacred. Admittedly, the latter is more rational, and looks a lot of how we treat our own families well, and can accept that other families are not doing so well.
Ciro's even more rational evil side says: the real reason why humans are sacred is a practical one: people have families that love them, and they come to kill you if you kill them, and this starts endless chains of violence that make society unbearable.
From the abstract:Ciro Santilli couldn't agree more... notably students must have a flexible choice of what to learn.
Much money, his student went on to say, is spent by various Governments in attempting to discover those people whose thorough education may be expected to bring in a return of value to the State, and the question how best to discover latent genius is an eminently practical one. After cogitation, Prof. Ostwald came to the conclusion that it is those students who cannot be kept on the rails - that is, who are not contented with methodical teaching - who have within them the seeds of genius
In the field of Love and Friendship, Ciro is a big believer in the merciless application of tit for tat. Never desire someone's love if you give and what comes back is not proportional. Cut your attempts to reach out immediately in such cases.
Never tell a woman you like her before she is in your bed.
If someone likes you and you don't like them as much, make that clear to them. Don't put this off, be it for compassion, curiosity, loneliness, or narcissism.
youtu.be/Sb0VHGnhX4M?t=174 from Video "Charles Bukowski Scandanavian TV interviews":
The way to get a woman is not to have money, not to look nice, not to have a nice personality. The way to get a woman, is to always be available, night or day. Any time you phone, you're there, or you're at the bar. They know that you are available at all times. It is very, very important to a woman.
See also: Section "Ciro Santilli's wife".
2019 cell phones are glued together with adhesive, which makes them impossible to repair them unless you have a heat gun, spend hours and hours learning and planning, and accept the risk of breaking the screen
Repairability scores: www.ifixit.com/smartphone-repairability
If you take a phone less than 300 dollars to a repair shop in the first world, they will say: I've never repaired this crap, and likely for the price of the repair you should just buy a new one, and so to the trash goes the old one, polluting the planet, and in comes a new one, enriching the manufacturer further.
Oh, there is some 2017 EU action actually: (archive) www.europarl.europa.eu/news/en/press-room/20170629IPR78633/making-consumer-products-more-durable-and-easier-to-repair
Why Ciro Santilli removed Disqus comments from his website in 2019-05-04 by 
Ciro Santilli 40 Updated 2025-07-16
Ciro Santilli 40 Updated 2025-07-16Commit: 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:
- Disqus discoverability is bad:
- Disqus archival is bad: web.archive.org/ does not work, and no one knows how to export the issues: www.archiveteam.org/index.php?title=Disqus
- before, there were two places where people could comment, Disqus and GitHub issues. Now there is just one.
- Disqus has ads if you ever reach enough traffic, which unacceptable, especially if the website owner don't get paid for them! It also makes page loads slower, although that likely does not matter much.
Downsides:
- people are more likely to comment on Disqus than to create an issue on GitHub, especially because most people use GitHub professionally. But this has the upside that there will be less shitposts as well.
- with Disqus you can see all issues attached to a page automatically, which is nice. But for as long as Ciro is alive, he intends to just solve the issues, cross link between content and issues and tag things appropriately.
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
It is true that one image is worth a thousand words, but unfortunately it is also true that one image takes up at least as much bytes as a thousand words!
Having one single page to rule them all is of course the ideal setup for a website, as you can Ctrl + F one ToC and quickly find what you want.
And, with Linux Kernel Module Cheat Ciro noticed that it is very hard to write so much intelligent prose that becomes larger than reasonable to load on a single webpage.
He then started using this technique for everything he writes, including this page and Chinese government.
However, if there are too many images on the page, the loading of the last images would take forever in case users want to view the last sections.
There are two solutions to that:
- be traditional and create separate web pages
- be bold and load images as they appear on the viewport: stackoverflow.com/questions/2321907/how-do-you-make-images-load-only-when-they-are-in-the-viewport/57389607#57389607Edit: OK, it was standardized with
loading=lazy, without need JavaScript!Now the last awesome thing would be a method that loads first images in viewport, then those below, and then those above, that would be the ultimate solution.This question comes close: stackoverflow.com/questions/7906348/change-loading-order-of-images-already-on-page
Ciro is still deciding between those two. The traditional approach works for sure but loses the one page to rule them all benefits.
The innovative approach will work for interactive viewing, but archive.org will fail to load the images for example, and there may be other unforseen consequences.
Wikimedia Commons is awesome and automatically converts and serves smaller versions of images, so always choose the smallest images size needed by the output document. Readers can then find the higher resolution versions by following the page source.
This also comes to mind: motherfuckingwebsite.com
zettelkasten.de/posts/overview/ from zettelkasten:
How many Zettelkästen should I have? The answer is, most likely, only one for the duration of your life. But there are exceptions to this rule.
How to develop Ciro Santilli's website before the OurBigBook migration by Ciro Santilli 40 Updated 2025-07-16
Ciro Santilli 40 Updated 2025-07-16The website moved from AsciiDoctor to OurBigBook Markup in 2020, making this section mostly useless. But hey, history!
The source code is located at: github.com/cirosantilli/cirosantilli.github.io
Build locally, watch for changes and rebuild automatically, and start a local server with:
git clone --recursive https://github.com/cirosantilli/cirosantilli.github.io
cd cirosantilli.github.io
bundle install
npm install
./runSource:
./run.The website will be visible at: localhost:4000.
Tested on the latest Ubuntu.
Publish changes to GitHub Pages:
git add -u
git commit -m 'make yourself look sillier'
./publishSource:
./publish.GitHub forces us to use the master branch for the build output... so the actual source is in the branch
dev.Update the gems with:
bundle update
git add Gemfile.lock
git commit -m 'update gems'His website was originally written in markdown, however those were deprecated in favour of AsciiDoctor when Ciro saw the light, rationale shown at: markdown-style-guideuse-asciidoc
GitHub pages is chosen instead of a single page GitHub README.adoc for the following reasons:
- Ciro will want some unsupported extensions, notably mathematics, likely with KaTeX server side:
- github.com/asciidoctor/asciidoctor/pull/3338
- stackoverflow.com/questions/11256433/how-to-show-math-equations-in-general-githubs-markdownnot-githubs-blog
- g14n.info/2014/09/math-on-github-pages/
- stackoverflow.com/questions/11256433/how-to-show-math-equations-in-general-githubs-markdownnot-githubs-blog
- www.quora.com/How-can-I-combine-latex-and-markdown-in-GitHub
- when GitHub dies, Ciro's website URL still lives and retains the PageRank!
Pinned article: Introduction to the OurBigBook Project
Welcome to the OurBigBook Project! Our goal is to create the perfect publishing platform for STEM subjects, and get university-level students to write the best free STEM tutorials ever.
Everyone is welcome to create an account and play with the site: ourbigbook.com/go/register. We belive that students themselves can write amazing tutorials, but teachers are welcome too. You can write about anything you want, it doesn't have to be STEM or even educational. Silly test content is very welcome and you won't be penalized in any way. Just keep it legal!
Intro to OurBigBook
. Source. We have two killer features:
- topics: topics group articles by different users with the same title, e.g. here is the topic for the "Fundamental Theorem of Calculus" ourbigbook.com/go/topic/fundamental-theorem-of-calculusArticles of different users are sorted by upvote within each article page. This feature is a bit like:
- a Wikipedia where each user can have their own version of each article
- a Q&A website like Stack Overflow, where multiple people can give their views on a given topic, and the best ones are sorted by upvote. Except you don't need to wait for someone to ask first, and any topic goes, no matter how narrow or broad
This feature makes it possible for readers to find better explanations of any topic created by other writers. And it allows writers to create an explanation in a place that readers might actually find it.
Figure 1. Screenshot of the "Derivative" topic page. View it live at: ourbigbook.com/go/topic/derivativeVideo 2. OurBigBook Web topics demo. Source. - local editing: you can store all your personal knowledge base content locally in a plaintext markup format that can be edited locally and published either:This way you can be sure that even if OurBigBook.com were to go down one day (which we have no plans to do as it is quite cheap to host!), your content will still be perfectly readable as a static site.
- to OurBigBook.com to get awesome multi-user features like topics and likes
- as HTML files to a static website, which you can host yourself for free on many external providers like GitHub Pages, and remain in full control
Figure 3. Visual Studio Code extension installation.
Figure 4. Visual Studio Code extension tree navigation.
Figure 5. Web editor. You can also edit articles on the Web editor without installing anything locally.Video 3. Edit locally and publish demo. Source. This shows editing OurBigBook Markup and publishing it using the Visual Studio Code extension.Video 4. OurBigBook Visual Studio Code extension editing and navigation demo. Source. 
- Infinitely deep tables of contents:
All our software is open source and hosted at: github.com/ourbigbook/ourbigbook
Further documentation can be found at: docs.ourbigbook.com
Feel free to reach our to us for any help or suggestions: docs.ourbigbook.com/#contact