A cube attack is a cryptographic attack primarily used against symmetric key ciphers, specifically those that use block ciphers. It was introduced by researchers to exploit certain properties of the S-boxes (substitution boxes) used in cryptographic algorithms. ### Key Concepts of Cube Attack: 1. **Cube Polynomial Representations**: - Every function, including cryptographic functions, can be expressed as a polynomial over a finite field.
"A.I. Rising" is a science fiction film released in 2018, directed by Lazar Bodrozic. The movie is set in a future where humanity has developed advanced artificial intelligence and explores the complexities of human-A.I. relationships. The story revolves around a space mission where a human astronaut forms a bond with a humanoid A.I. named KIKI, who is designed to serve and assist the crew.
A coframe refers to a mathematical construct in differential geometry and is often used in the context of differentiable manifolds. Specifically, a coframe is a set of differential one-forms that provide a dual basis to a frame, which is a set of tangent vectors. Here's a more detailed breakdown: 1. **Frame**: Given a manifold, a frame at a point is essentially a set of linearly independent tangent vectors that span the tangent space at that point.
Libration is a phenomenon observed in celestial mechanics, particularly in the context of the Moon's orbit around the Earth. It refers to the oscillating motion that allows us to see slightly more than half of the Moon's surface from Earth over time. This effect occurs due to the Moon's elliptical orbit and its axial tilt. There are two primary types of libration: 1. **Libration in Longitude**: This occurs because the Moon's orbital speed varies as it travels along its elliptical path.
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!
As of 2019, the silicon industry is ending, and molecular biology technology is one of the most promising and growing field of engineering.
Ciro Santilli is especially excited about DNA-related technologies, because DNA is the centerpiece of biology, and it is programmable.
First, during the 2000's, the cost of DNA sequencing fell to about 1000 USD per genome in the end of the 2010's: Figure 2. "Cost per genome vs Moore's law from 2000 to 2019", largely due to "Illumina's" technology.
The medical consequences of this revolution are still trickling down towards medical applications of 2019, inevitably, but somewhat slowly due to tight privacy control of medical records.
Ciro Santilli predicts that when the 100 dollar mark is reached, every person of the First world will have their genome sequenced, and then medical applications will be closer at hand than ever.
But even 100 dollars is not enough. Sequencing power is like computing power: humankind can never have enough. Sequencing is not a one per person thing. For example, as of 2019 tumors are already being sequenced to help understand and treat them, and scientists/doctors will sequence as many tumor cells as budget allows.
Then, in the 2010's, CRISPR/Cas9 gene editing started opening up the way to actually modifying the genome that we could now see through sequencing.
What's next?
Ciro believes that the next step in the revolution could be could be: de novo DNA synthesis.
This technology could be the key to the one of the ultimate dream of biologists: cheap programmable biology with push-button organism bootstrap!
Just imagine this: at the comfort of your own garage, you take some model organism of interest, maybe start humble with Escherichia coli. Then you modify its DNA to your liking, and upload it to a 3D printer sized machine on your workbench, which automatically synthesizes the DNA, and injects into a bootstrapped cell.
You then make experiments to check if the modified cell achieves your desired new properties, e.g. production of some protein, and if not reiterate, just like a software engineer.
Of course, even if we were able to do the bootstrap, the debugging process then becomes key, as visibility is the key limitation of biology, maybe we need other cheap technologies to come in at that point.
This a place point we see the beauty of evolution the brightest: evolution does not require observability. But it also implies that if your changes to the organism make it less fit, then your mutation will also likely be lost. This has to be one of the considerations done when designing your organism.
Other cool topic include:
- computational biology: simulations of cell metabolism, protein and small molecule, including computational protein folding and chemical reactions. This is basically the simulation part of omics.If we could only simulate those, we would basically "solve molecular biology". Just imagine, instead of experimenting for a hole year, the 2021 Nobel Prize in Physiology and Medicine could have been won from a few hours on a supercomputer to determine which protein had the desired properties, using just DNA sequencing as a starting point!
- microscopy: crystallography, cryoEM
- analytical chemistry: mass spectroscopy, single cell analysis (Single-cell RNA sequencing)
Ciro is sad that by the time he dies, humanity won't have understood the human brain, maybe not even a measly Escherichia coli... Heck, even key molecular biology events are not yet fully understood, see e.g. transcription regulation.
One of the most exciting aspects of molecular biology technologies is their relatively low entry cost, compared for example to other areas such as fusion energy and quantum computing.
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.
Accounts controlled by Ciro Santilli on Twitter:
- twitter.com/cirosantilli primary channel, contains only updates on Ciro's best technical content. Low volume.
- twitter.com/cirosantilli2 secondary channel, contains smaller technical updates that didn't make it to the primary channel, and some China fun. Higher volume.
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.
Ciro feels that this resonates a lot with his OurBigBook.com.
Supercut:
The minute I dropped out I could stop taking the required classes that didn't interest me, and begin dropping in on the ones that looked far more interesting.And much of what I stumbled into by following my curiosity and intuition turned out to be priceless later on.Because I had dropped out and didn't have to take the normal classes, I decided to take a calligraphy class to learn how to do this.If I had never dropped in on that single course in college, the Mac would have never had multiple typefaces or proportionally spaced fonts.Of course it was impossible to connect the dots looking forward when I was in college. But it was very, very clear looking backward 10 years later.Again, you can't connect the dots looking forward; you can only connect them looking backward. So you have to trust that the dots will somehow connect in your future. You have to trust in something — your gut, destiny, life, karma, whatever. This approach has never let me down, and it has made all the difference in my life.
Then:
You've got to find what you love.Your work is going to fill a large part of your life, and the only way to be truly satisfied is to do what you believe is great work.And the only way to do great work is to love what you do. If you haven't found it yet, keep looking.So keep looking until you find it.Don't settle.
And:Mirror and morning are not required though, a computer screen will do just fine: www.reddit.com/r/depression/comments/6jtamj/im_at_work_just_staring_at_my_computer_screen/
When I was 17, I read a quote that went something like: "If you live each day as if it was your last, someday you'll most certainly be right."
And then he quotes form the Whole Earth Catalog, a paper Atlas from the '70s he admired:
Stay Hungry. Stay Foolish
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.
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