Theories of Quantum Matter by Austen Lamacraft Quantum Hall Effect Fractional Charge Updated 2025-07-11 +Created 1970-01-01
A cool thought: bacteria like E. Coli replicate every 20 minutes. A human replicates every 15 years. So how can multicellular beings possibly cope with the speed of evolution of parasites?
The answer is that within us, the adaptive immune system is a population of cells that evolves very quickly. So in a sense, within our bodies there is fast cell-level non-inheritable evolution happening daily!
Ciro Santilli had once assigned this as one of Ciro Santilli's best random thoughts, but he later found that Wikipedia actually says exactly that: en.wikipedia.org/wiki/Reverse_engineering ("similar to scientific research, the only difference being that scientific research is about a natural phenomenon") so maybe that is where Ciro picked it up unconsciously in the first place.
Website front-end for a mathematical formal proof system Updated 2025-07-11 +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!
He does lots of little experiments which is cool.
Binds an amino acid to the correct corresponding tRNA sequence. Wikipedia mentions that humans have 20 of them, one for each proteinogenic amino acid.
Unfortunately accused of sexual misconduct: www.theguardian.com/technology/2019/mar/11/google-executive-payout-harassment-amit-singhal. But one can still do good despite our defects:
Pitched OurBigBook.com to him:
Idea: make all Sitare University materials open, and allow students to write the content
Includes:
Does not include amphibians. If you include them, you have the tetrapods.
Unit of electric current.
Affected by the ampere in the 2019 redefinition of the SI base units.
Starting in the 2019 redefinition of the SI base units, the elementary charge is assigned a fixed number, and the Ampere is based on it and on the second, which is beautiful.
This choice is not because we attempt to count individual electrons going through a wire, as it would be far too many to count!
Rather, it is because because there are two crazy quantum mechanical effects that give us macroscopic measures that are directly related to the electron charge. www.nist.gov/si-redefinition/ampere/ampere-quantum-metrology-triangle by the NIST explains that the two effects are:
- quantum Hall effect, which has discrete resistances of type:for integer values of .
- Josephson effect, used in the Josephson voltage standard. With the Inverse AC Josephson effect we are able to produce:per Josephson junction. This is about 2 microvolt / GHz, where GHz is a practical input frequency. Video "The evolution of voltage metrology to the latest generation of JVSs by Alain Rüfenacht" mentions that a typical operating frequency is 20 GHz.But this is possible to implement in a single chip with existing micro fabrication techniques, and is exactly what the Josephson voltage standard does!
Those effect work because they also involve dividing by the Planck constant, the fundamental constant of quantum mechanics, which is also tiny, and thus brings values into a much more measurable order of size.
Notably used for the pattern of the double-slit experiment.
Main implementations: the same as electronic switches: vacuum tubes in the past, and transistors in the second half of the 20th century.
To test it, let's get two computers on the same local area network, e.g. connected to Wi-Fi on the same home modem router.
On computer B:
- find computer IP with the
ipCLI tool. Suppose it is 192.168.1.102 - then run Ciro's
ncHTTP test server
Output on terminal 1:TODO understand them all! Possibly correlate with Wireshark, or use
17:14:22.017001 IP ciro-p14s.55798 > 192.168.1.102.8000: Flags [S], seq 2563867413, win 64240, options [mss 1460,sackOK,TS val 303966323 ecr 0,nop,wscale 7], length 0
17:14:22.073957 IP 192.168.1.102.8000 > ciro-p14s.55798: Flags [S.], seq 1371418143, ack 2563867414, win 65160, options [mss 1460,sackOK,TS val 171832817 ecr 303966323,nop,wscale 7], length 0
17:14:22.074002 IP ciro-p14s.55798 > 192.168.1.102.8000: Flags [.], ack 1, win 502, options [nop,nop,TS val 303966380 ecr 171832817], length 0
17:14:22.074195 IP ciro-p14s.55798 > 192.168.1.102.8000: Flags [P.], seq 1:82, ack 1, win 502, options [nop,nop,TS val 303966380 ecr 171832817], length 81
17:14:22.076710 IP 192.168.1.102.8000 > ciro-p14s.55798: Flags [P.], seq 1:80, ack 1, win 510, options [nop,nop,TS val 171832821 ecr 303966380], length 79
17:14:22.076710 IP 192.168.1.102.8000 > ciro-p14s.55798: Flags [.], ack 82, win 510, options [nop,nop,TS val 171832821 ecr 303966380], length 0
17:14:22.076727 IP ciro-p14s.55798 > 192.168.1.102.8000: Flags [.], ack 80, win 502, options [nop,nop,TS val 303966383 ecr 171832821], length 0
17:14:22.077006 IP ciro-p14s.55798 > 192.168.1.102.8000: Flags [F.], seq 82, ack 80, win 502, options [nop,nop,TS val 303966383 ecr 171832821], length 0
17:14:22.077564 IP 192.168.1.102.8000 > ciro-p14s.55798: Flags [F.], seq 80, ack 82, win 510, options [nop,nop,TS val 171832821 ecr 303966380], length 0
17:14:22.077578 IP ciro-p14s.55798 > 192.168.1.102.8000: Flags [.], ack 81, win 502, options [nop,nop,TS val 303966384 ecr 171832821], length 0
17:14:22.079429 IP 192.168.1.102.8000 > ciro-p14s.55798: Flags [.], ack 83, win 510, options [nop,nop,TS val 171832824 ecr 303966383], length 0-A option to dump content. Unlisted articles are being shown, click here to show only listed articles.