The general and ideal user acquisition is of course organic Googling:
- user does not understand his teacher's explanation of a subject
- user Googles into rare specific subject
- looks around, then login/create account with OAuth to leaves a comment or upvote
- notice that you can fork anything
- mind = KABOOM
However, before that point, it is very likely that Ciro will have to physically do some very hard and specific user acquisition work at some University. Maybe there is a more virtual way of achieving this.
This work will involve going through some open set of university lecture notes, and creating a superior version of them on OurBigBook.com, and somehow getting students to notice it and use it as a superior alternative to their crappy lecture notes.
Another very promising route is publishing the answers to old examination questions on the website. It is likely that we will be able to overcome any copyright issues by uploading only the answers to numbered questions. There is a minor risk that these would be considered derivative works of the copyrighted questions. But universities would have to be very anal to enforce a DMCA for that!!!
Getting in contact with students is an epic challenge, as an incredibly deep chasm separates us:
- it is basically impossible to try and approach teachers: how to convince teachers to use CC BY-SA
- and on the other hand, how will you get university students to trust you are not a pedophile and that you actually want to help them?The missing aspect is how to join their main "class communication group", e.g. a WhatsApp or Discord chat they have. That would be the perfect entry point to communicate with the end users. But that entry point is also generally closed exclusively for students, and sometimes lecturers, and will not accept anyone external.Perhaps Ciro would be able to do something with one of the two Universities he attended in the past: École Polytechnique or University of São Paulo. But there was no clear channel in those institutions for that. There is either an "infinitely noisy Facebook with everyone that bothered" or silence, deathly silence and isolation of no contact. The key hard part is getting a per-course granularity chat. Discord Student Hubs are a fantastic initiative in that area. Shame that Discord is an unusable mess with zero ways to select which notifications you care about: Section "Discord email notifications"!One approach method that shows some promise is to follow the Student societies, which often host open events of interest outside of work hours.
Walking with advertisement t-shirts mentioning specific course names in some university location is something Ciro seriously considers, that's how desperate things are. Watch out: docs.ourbigbook.com/#public-relations for T-shirt news!
The natural sciences are not just a tool to predict the future.
They are a reminder that the lives that we live daily are mere illusions, religious concepts such as Maya and Samsara come to mind.
We as individuals perceive nothing about the materials that we touch every day really work, nor more importantly how our brain and cell work.
Everything is magic out of our control.
The natural sciences allow us peek, with huge concentrated effort, into tiny little bits a little of those unknowns, and blow our minds as we notice that we don't know anything.
For all practical purposes in life, there is a huge macro micro gap. We are only able to directly perceive and influence the macro events. And through those we try to affect micro events. Because for good or bad, micro events reflect in the macro world.
It is as if we live in a different plane of existence above molecules, and below galaxies. The hierarchy of Figure "xkcd 435: Fields arranged by purity" puts that nicely into perspective, shame it only starts at the economical level, not going up to astronomy.
The great beauty of science is that it allows us to puncture through some of the layers of reality, either up or down, away from our daily experience.
And the great beauty of artificial intelligence research is that it allows to peer deeper into exactly our layer of existence.
Every one or two weeks Ciro Santilli remembers that he and everything he touches are just a bunch of atoms, and that is an amazing feeling. This is Ciro's preferred source of Great doubt. Another concept that comes to mind is when you see it, you'll shit bricks.
Perhaps, the feeling of physics and the illusion of life reaches its peak in molecular biology.
Just look at your fucking hand right now.
Do you have any idea of each of the cells in it work? Isn't is at least 100 times more complex than the materials of the table you hand is currently resting on?
This is the non-science fiction version of the lotus-Eater Machine.
Alan Watts's "Philosopher" talk mentions related ideas:
The origin of a person who is defined as a philosopher, is one who finds that existence itself is exceedingly odd.
The toddler of a friend of Ciro Santilli's wife asked her mum:Our perception of the macroscopic world is so magic that children have to learn the difference between living and non-living things.
Why doesn't my tiger doll close its eyes when we sleep?
James Somers put it very well as well in his article I should have loved biology by James Somers, this quote was brought to Ciro's attention by Bert Hubert's website[ref].The same applies to other natural sciences.
I should have loved biology but I found it to be a lifeless recitation of names: the Golgi apparatus and the Krebs cycle; mitosis, meiosis; DNA, RNA, mRNA, tRNA.In the textbooks, astonishing facts were presented without astonishment. Someone probably told me that every cell in my body has the same DNA. But no one shook me by the shoulders, saying how crazy that was. I needed Lewis Thomas, who wrote in The Medusa and the Snail:For the real amazement, if you wish to be amazed, is this process. You start out as a single cell derived from the coupling of a sperm and an egg; this divides in two, then four, then eight, and so on, and at a certain stage there emerges a single cell which has as all its progeny the human brain. The mere existence of such a cell should be one of the great astonishments of the earth. People ought to be walking around all day, all through their waking hours calling to each other in endless wonderment, talking of nothing except that cell.
Only after Ciro became an adult did he finally understand that Sun Wukong was the basis for Dragon Ball as mentioned at: Figure "19th century illustration of the Journey to the West protagonist Sun Wukong". And that Sun Wukong was a million times more famous overall. Mind blown.
His given name "Wukong" literally means "the one who mastered the void" (Wu = Comprehend, Kong = void), so clearly a Dharma name. Edit: it is actually given in the novel, he was born without name. They seem to be Taoist however.
The family name sun1 孙 is the same character as "grandson", but most educated Chinese people seem to be able to recognize it as a reference to "monkey" from some archaic context not anymore in current usage.
Website front-end for a mathematical formal proof system Updated 2024-12-15 +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!
All we would need would be something analogous to a package registry like PyPI or NodeJS' registry.
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.
This is a close as we can get to Erdős' book.
Maybe Ciro will just stuff this into OurBigBook.com once that takes over the world.
This project could be seen as a more automated/less moderated version of ProofWiki.
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