Ciro Santilli @cirosantilli 37

This is good. But it misses some key operations, so much so that makes Ciro not want to learn/use it daily.

Mahayana adds a bunch of stuff on top of the Pali Canon. Most of it appears to be random mysticism. Maybe there is something good in it... maybe.

Ciro Santilli believes that molecular biology technologies will be a large part of the next big things as shown at: Section "Molecular biology technologies".

Bibliography:

The name cirodown should not appear anywhere now, except with very few exceptions, e.g.:

I have also squatted OurBigBook on all major social media handles for near future usage, e.g.: twitter.com/ourbigbook and so on.

I was going to do this sooner or later, it was inevitable, but the timing was partly triggered due to noticing that English speakers (and likely many other nationalities) are not able to easily read/hear/pronounce "Ciro".

Issue report at: github.com/ourbigbook/ourbigbook/issues/198 Suppose you had:

programming-language.ciro

= Programming language

\Image[https://raw.githubusercontent.com/cirosantilli/media/master/python-logo.jpg]
{title=The \x[python-programming-language] logo}

== Python
{c}
{disambiguate=programming-language}

logos-i-like.ciro

= Logos I like

\x[image-the-python-logo]

Now, when rendering \x[image-the-python-logo], we would need to fetch two IDs:

But after group all SQL queries together was done, there was no way to know that rendering image-the-python-logo would imply also fetching python-programming-language.

This was solved by adding a new database entry type, REFS_TABLE_X_TITLE_TITLE to the existing References table, which tracks dependencies between IDs.

After this was setup, we can now know that image-the-python-logo depends on image-the-python-logo, and then fetch both of them together in a single JOIN.

The best open source implementation as of 2020 seems to be: Mozilla rr.

This is not a label that Ciro Santilli likes to give lightly. But maybe sometimes, it is inevitable.

Bibliography:

Originally it was likely created to study constrained mechanical systems where you want to use some "custom convenient" variables to parametrize things instead of global x, y, z. Classical examples that you must have in mind include:lagrangian mechanics lectures by Michel van Biezen (2017) is a good starting point.

When doing lagrangian mechanics, we just lump together all generalized coordinates into a single vector $\overrightarrow{q}(t):\mathbb{R}\to {\mathbb{R}}^n$ that maps time to the full state:where each component can be anything, either the x/y/z coordinates relative to the ground of different particles, or angles, or nay other crazy thing we want.

The Lagrangian is a function ${\mathbb{R}}^n\times {\mathbb{R}}^n\times \mathbb{R}\to \mathbb{R}$ that maps:to a real number.

Then, the stationary action principle says that the actual path taken obeys the Euler-Lagrange equation:This produces a system of partial differential equations with:

The mixture of so many derivatives is a bit mind mending, so we can clarify them a bit further. At:the $q_i$ is just identifying which argument of the Lagrangian we are differentiating by: the i-th according to the order of our definition of the Lagrangian. It is not the actual function, just a mnemonic.

Then at:

However, people later noticed that the Lagrangian had some nice properties related to Lie group continuous symmetries.

Basically it seems that the easiest way to come up with new quantum field theory models is to first find the Lagrangian, and then derive the equations of motion from them.

For every continuous symmetry in the system (modelled by a Lie group), there is a corresponding conservation law: local symmetries of the Lagrangian imply conserved currents.
Genius: Richard Feynman and Modern Physics by James Gleick (1994) chapter "The Best Path" mentions that Richard Feynman didn't like the Lagrangian mechanics approach when he started university at MIT, because he felt it was too magical. The reason is that the Lagrangian approach basically starts from the principle that "nature minimizes the action across time globally". This implies that things that will happen in the future are also taken into consideration when deciding what has to happen before them! Much like the lifeguard in the lifegard problem making global decisions about the future. However, chapter "Least Action in Quantum Mechanics" comments that Feynman later notice that this was indeed necessary while developping Wheeler-Feynman absorber theory into quantum electrodynamics, because they felt that it would make more sense to consider things that way while playing with ideas such as positrons are electrons travelling back in time. This is in contrast with Hamiltonian mechanics, where the idea of time moving foward is more directly present, e.g. as in the Schrödinger equation.

Furthermore, given the symmetry, we can calculate the derived conservation law, and vice versa.

And partly due to the above observations, it was noticed that the easiest way to describe the fundamental laws of particle physics and make calculations with them is to first formulate their Lagrangian somehow: S.

TODO advantages:

Bibliography:

The basis of 1970-20XX computers, gotta understand them I guess?

The website was dead as of February 2025. Last archive: web.archive.org/web/20240418004442/http://www.themathgenome.com/ Pings:They were seeking help on May 2024:so its likely the followup death. LinkedIn post gives basic stack: MERN stack, Heroku, Supabase/MongoDB Atlas.

Appears to support multiple proof assistant backends including Lean, Hol and Coq.

A discussion on the Lean Zulip: leanprover.zulipchat.com/#narrow/stream/113488-general/topic/The.20Math.20Genome.20Project/near/352639129. Lean people are not convinced about the model in general it seems however.

TODO closed source? Really? www.themathgenome.com/pricing

TODO not viewable without login?

Has conjectures feature.

Built by this dude John Mercer:He must be independently wealthy or something to do such a project? What a hero. But he seems to have jobs. On the side? Hardcore.

A failed Hacker News self post: news.ycombinator.com/item?id=35775071

Ciro Santilli asked: discord.com/channels/1096393420408360989/1096393420408360996/1137047842159079474Owner:So apparently there will be proof checking, but no dependencies between proofs, you still have to pull request everything back and face the pain.

Bibliography: