The most important projects Ciro Santilli wants to do

They are sorted in order of "most likely to get done first".

Top one: OurBigBook.com

Actual section at: Section "OurBigBook.com"

Prototype: github.com/cirosantilli/Urho3D-cheat

Prior art research: github.com/cirosantilli/awesome-reinforcement-learning-games

Less good discrete prototype: github.com/cirosantilli/rl-game-2d-grid YouTube demo: Video 1. "Top Down 2D Continuous Game with Urho3D C++ SDL and Box2D for Reinforcement learning by Ciro Santilli (2018)".

The goal of this project is to reach artificial general intelligence.

A few initiatives have created reasonable sets of robotics-like games for the purposes of AI development, most notably: OpenAI and DeepMind.

However, all projects so far have only created sets of unrelated games, or worse: focused on closed games designed for humans!

What is really needed is to create a single cohesive game world, designed specifically for this purpose, and with a very large number of game mechanics.

Notably, by "game mechanic" is meant "a magic aspect of the game world, which cannot be explained by object's location and inertia alone" in order to test the the missing link between continuous and discrete AI.

Much in the spirit of gvgai, we have to do the following loop:

The question then becomes: do we have enough computational power to simulation a game worlds that is analogous enough to the real world, so that our AI algorithms will also apply to the real world?

To reduce computation requirements, it is better to focus on a 2D world at first. Such world with the right mechanics can break any AI, while still being faster to simulate than a 3D world.

The initial prototype uses the Urho3D open source game engine, and that is a reasonable project, but a raw Simple DirectMedia Layer + Box2D + OpenGL solution from scratch would be faster to develop for this use case, since Urho3D has a lot of human-gaming features that are not needed, and because 2019 Urho3D lead developers disagree with the China censored keyword attack.

Simulations such as these can be viewed as a form of synthetic data generation procedure, where the goal is to use computer worlds to reduce the costs of experiments and to improve reproducibility.

Ciro has always had a feeling that AI research in the 2020's is too unambitious. How many teams are actually aiming for AGI? When he then read Superintelligence by Nick Bostrom (2014) it said the same. AGI research has become a taboo in the early 21st century.

Related projects:

Related ideas:

Bibliograpy:

It is unbelievable that you can't find easily on YouTube recreations of many of the key physics/chemistry experiments and of common laboratory techniques.

Experiments, the techniques required to to them, and the history of how they were first achieved, are the heart of the natural sciences. Without them, there is no motivation, no beauty, no nothing.

School gives too much emphasis on the formulas. This is bad. Much more important is to understand how the experiments are done in greater detail.

The videos must be completely reproducible, indicating the exact model of every experimental element used, and how the experiment is setup.

A bit like what Ciro Santilli does in his Stack Overflow contributions but with computers, by indicating precise versions of his operating system, software stack, and hardware whenever they may matter.

It is understandable that some experiments are just to complex and expensive to re-create. As an extreme example, say, a precise description of the Large Hadron Collider anyone? But experiments up to the mid-20th century before "big science"? We should have all of those nailed down.

We should strive to achieve the cheapest most reproducible setup possible with currently available materials: recreating the original historic setup is cute, but not a priority.

Furthermore, it is also desirable to reproduce the original setups whenever possible in addition to having the most convenient modern setup.

Lists of good experiments to cover be found at: the most important physics experiments.

This project is to a large extent a political endeavour.

Someone with enough access to labs has to step up and make a name for themselves through the huge effort of creating a baseline of amazing content without yet being famous.

Until it reaches a point that this person is actively sought to create new material for others, and things snowball out of control. Maybe, if the Gods allow it, that person could be Ciro.

Tutorials with a gazillion photos and short videos are also equally good or even better than videos, see for example Ciro's How to use an Oxford Nanopore MinION to extract DNA from river water and determine which bacteria live in its for an example that goes toward that level of perfection.

The Applied Science does well in that direction.

This project is one step that could be taken towards improving the replication crisis of science. It's a bit what Hackster.io wants to do really. But that website is useless, just use OurBigBook.com and create videos instead :-)

We're maintaining a list of experiments for which we could not find decent videos at: Section "Physics experiment without a decent modern video".

Ciro Santilli visited the teaching labs of a large European university in the early 2020's. They had a few large rooms filled with mostly ready to run versions of several key experiments, many/most from "modern physics", e.g. Stern-Gerlach experiment, Quantum Hall effect, etc.. These included booklets with detailed descriptions of how to operate the apparatus, what you'd expect to see, and the theory behind them. With a fat copyright notice at the bottom. If only such universities aimed to actually serve the public for free rather than hoarding resources to get more tuition fees, university level education would already have been solved a long time ago!

Related:

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: