Ciro Santilli @cirosantilli 35

The order of a algebraic structure is just its cardinality.

Sometimes, especially in the case of structures with an infinite number of elements, it is often more convenient to talk in terms of some parameter that characterizes the structure, and that parameter is usually called the degree.

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

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:

And here are some more interesting links:

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:

Mission: to live in a world where you can learn university-level mathematics, physics, chemistry, biology and engineering from perfect free books that anyone can write to get famous.

Live website: ourbigbook.com

Further information and rationale: Section "OurBigBook.com"

The project's mission is one of, or perhaps the most important, life objective of Ciro Santilli. Reproductive goals aside. These two types of goal are incommensurable. This is one of the great challenges of life.

This is ongoing project.

Ciro's goals in advertising this half done project are is partly to obtain some feedback, and partly to give the idea to someone else who might help push it further, be it in this stack or not.

Better editing support is a must, likely WYSIWYG.

But besides that, it is already in broad strokes the best approach Ciro Santilli can come up with to try and reach the mission statement only with technical advances, i.e. without large amounts of money or political influence which Ciro Santilli does not have.

Maybe that website isn't enough of a technical advance to reach its mission. Maybe there is some further not yet imagined technical insight that would push it into viability. Maybe not. But one must try. Only God can know the answer to these questions.

As of 2022, Ciro has spent about 2.5 years full time working on this project. First he spent about 1 year in 2014 on the first iteration: github.com/booktree/booktree, a GitLab fork, but then decided it was not the way to go.

Then around 2021 he put in some more 1.5 year of full time work, now with a possibly overly complicated (or perhaps just insane/immature) Next.js/Sequelize from scratch website stack.

It makes Ciro a bit ashamed to see that "so little user visible stuff was achieved in so much time". It is partly because he and many people underestimate the difficulty of web development. Perhaps there were some bad stack/useless feature choices issues. And a good dose of indulging in studying the natural sciences to bootstrap content and have fun. But really trying is the only way to learn.

Randomly reproduced at: web.archive.org/web/20080105074243/http://personal.stevens.edu/~nkahl/Top100Theorems.html

Good place to hunt for the beauty of mathematics.

Cirists,

Ah, some of the coolest places on Earth?

Ciro's best quotes selected by no one other than Ciro can be found at: Ciro Santilli's best random thoughts.

Jesus has some nice ones: Section "Quote by Jesus".

Related to technology:

Basically the Royal Society's scientific vulgarization cousin.