Thread by @Stu_B22

Today's thinking starts from the vision statement currently headlining the Wikimedia foundation home page:
"Imagine a world in which every single human being can freely share in the sum of all knowledge."
wikimediafoundation.org

Let's consider that knowledge sharing in the context of math, physics, and computation, ranging from the more settled foundations to the frontiers such as Hilbert's problems en.wikipedia.org/wiki/Hilbert%2…
and more recently Smale's problems
en.wikipedia.org/wiki/Smale%27s…

In particular let's look into Hilbert's sixth problem, regarding the axiomization of physics: en.wikipedia.org/wiki/Hilbert%2…

Illumination from Bruno Woltzenlogel Paleo: "...in favor of a more prominent role for proofs in the formalization of Physics, and consequently, for proof theory in approaches to Hilbert’s sixth problem and in studies of the foundations of Physics." ncbi.nlm.nih.gov/pmc/articles/P…

That's pretty good stuff, eh? Here is Dr. Paleo's home page. It appears that he likes Scala! paleo.woltzenlogel.org

Now suppose we bring that axiomatic mindset to discussion of two topics in large-scale physics that I've seen recent popSci articles about.
1) Dark Matter+Energy (vs. MOND)

https://twitter.com/RyanFMandelbaum/status/1034470450695479296

2) Ye Olde Bigge Bange

https://twitter.com/StartsWithABang/status/1036978007850725377

We see that folks can take different positions on those physics topics. Let's lump them as "cosmology" for tweet-brevity today. The big question I am trying to open up in this thread is, how can we investigate proposed cosmological models in an open, shared, axiom-grounded way?

Example:
Does your analytical model treat speed-of-light-in-vacuum as a constant, axiomatically?
Or does that constancy drop out as a theorem from some other axioms?
#ShowUsTheAxioms

A much deeper example: Paleo's paper linked above cites this one from 2008
"Axiomatizing relativistic dynamics without conservation postulates."
by Andréka, Madarász X., Németi, and Székely.
philsci-archive.pitt.edu/3861

So the big topic we want to open with folks like @OpenDreamKit community
is how our digital tools can help apply this axiomatic thinking to our analysis
and exploration of physics around the big topics like cosmology, e.g. the two
PopSci articles linked earlier in this thread.

Some more challenges, and some more popSci, just quickly illustrating the many kinds of interesting things that more people could be learning about and thinking about, on an increasingly serious level, if we had the right support
from interactive tools:
newscientist.com/round-up/6-phy…

When we look to see what kinds of tools exist now, we can find popSci articles like this one, focusing on numerical simulations of cosmology models. But what about direct analysis and exploration of the models themselves, and their grounding? quantamagazine.org/coder-physicis…

🚨🚔Roo Roo Roo. MP-Gadget, the equation police 👮‍♀️👮‍♂️are pulling
you over. We want you to stop burning electricity with your mountain of
parallel C code, until you can #ShowUsTheAxioms. (Of course I am kidding,
but do y'all see what I mean?)
github.com/MP-Gadget/MP-G…

Following citations of Andreka's paper leads us to
"Using Isabelle/HOL to Verify First-Order Relativity Theory" by Stannett and Nemeti, 2014. Full-text PDF can be found on ResearchGate and perhaps elsewhere.
link.springer.com/article/10.100…

On a less-lofty plane, if science is an open-source project, then where is our issue tracking system? (I.E. our "bug database"!) Maybe we can do better than this?
mathoverflow.net/questions/2750…

That page links to this one. Let's imagine how these different gaps could be presented in terms of hyperlinks into our axiom-grounded model corpus, as shown in Paleo's work and the relativity logic models. Imagine visual branches
of possible resolutions.
web.math.princeton.edu/~aizenman/Open…