Ciro Santilli @cirosantilli 35

Once you hear about the uncomputability of such problems, it makes you see that all Diophantine equation questions risk being undecidable, though in some simpler cases we manage to come up with answers. The feeling is similar to watching people trying to solve the Halting problem, e.g. in the effort to determine BB(5).

XML predecessor.

To remove and install Shimano and ISIS Drive splined 20-tooth bottom bracket cups.

Bought: 2020-11-07. Also getting a park Tool PAW-12 adjustable wrench to use with it.

They seem to do some cool stuff.

They have also declined every one of Ciro Santilli's applications for software engineer jobs before any interview. Ciro always wondered what does it take to get an interview with them. Lilely a PhD? Oh well.

In the early days at least lots of gamedev experience was enough though: www.linkedin.com/in/charles-beattie-0695373/.

Ciro Santilli has a hard time understanding why this is possible, e.g. many people use short 4 digit pins, or a short swipe pattern. Why can't this be cracked easily offline?

This is the discrete logarithm problem where the group is a cyclic group.

In this case, the problem becomes equivalent to reversing modular exponentiation.

This computational problem forms the basis for Diffie-Hellman key exchange, because modular exponentiation can be efficiently computed, but no known way exists to efficiently compute the reverse function.

Circa 2023, the feed is an unbearable list of stupid suggestions, never-ending idiotic memes, and you just end up missing posts you actually care about from people you actually follow.

Yet, all breakthroughs, comes from them, because the people who are crazy enough to believe they can change the world are the ones who actually do ;-)

How to deal articles:

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!

This was THE craze thing in Brazil before Pokemon, it was shown from 1994 to 1997. In particular the collectible action figures! It was possibly more popular in Brazil than e.g. in the US: www.quora.com/Why-was-Saint-Seiya-so-popular-in-Brazil

The thing as quite violent, rated for 14-year olds, but no one gave a fuck, 7 yo Ciro was happily watching it. We protect children too much.

That series also had quite a religious feel to it (as obviously suggested by the series English name itself). It must also have been a great motivator to getting young kids into astronomy!

Ciro's favorite character was definitely Andromeda Shun. He was smart and thoughtful, and had the coolest most complex weapon: his chain whips. He's also a bit effeminate, with his pink clothing and a gentle way. Perhaps that is the reason for adult Ciro's mild fascination with the Andromeda Galaxy.

The English name is horrendous... the Portuguese/French name is so much better: Knights of the Zodiac! Saying this in English just reminded Ciro Santilli of the Zodiac Killer. But nevermind.

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:

Ciro Santilli pinging people: