Cosmology Project and dependencies

Stream: PhysLean

[Pedro Bessa]

Hello, I'm a postdoc working in gravitation, cosmology and astrophysics and I got quite interested in the PhysLean project after reading about it on linkedin. I'm able to start working here and there with the Cosmology project, since that is my main background.

I also have a background in mathematics since I started with a B.Sc. in maths, and kept my interest in formalization and axiomatization throughout my change to physics research, so I am not completely unfamiliar to Lean and the proposals. I am new to the Lean 4 language itself, which I'm currently reading and learning to properly start the project, but I think there's nothing better than a project to learn a new language.

What I am most confused about is how we should build the projects from the ground. In particular, I've seen that there is no Riemannian (or Lorentzian) geometry library in mathlib, and although there is very complete Special Relativity library, to properly develop the Cosmology project one would need at least the notions of metric and Levi-Civita connection.

My question then boils down to this: How much should I worry about dependencies before I start working out the fundamentals for the project (Robertson-Walker metric, Friedmann equations, density and pressure terms)? Can I first implement the basics without invoking math dependencies to the underlying structure, such as just describing the systems in terms of the scale factor, density and pressure; or should I first lay the groundwork by defining the Robertson-Walker Lorentzian manifold and describing its connection?

I hope I was able to properly express my doubts and am excited to help with physLean!

[Joseph Tooby-Smith]

Hi Pedro!

Nice to meet you and thank you for your interest in the project!

To answer your main question:

How much should I worry about dependencies before I start working out the fundamentals for the project (Robertson-Walker metric, Friedmann equations, density and pressure terms)? Can I first implement the basics without invoking math dependencies to the underlying structure, such as just describing the systems in terms of the scale factor, density and pressure; or should I first lay the groundwork by defining the Robertson-Walker Lorentzian manifold and describing its connection?

Yes you can implement the basics without invoking the math dependencies to the underlying structure. Indeed, I think if we didn't do this the project overall would become fairly stagnant which is not desirable at this stage (IMO having something is better than having nothing).

When implementing the basics though I would be mindful that in the future we will want the underlying math structure there, so doing it in a way where we can easily refactor to include the underlying math structure when needed will be helpful in the long term. I have done the same with e.g. the Higgs field, really mathematically we would want this defined in a vector bundle associated to the principal bundle of the Standard Model gauge group - but mathlib isn't there just yet - so I did the basics knowing one day it will be refactored.

...to properly develop the Cosmology project one would need at least the notions of metric and Levi-Civita connection.

I note that PhysLean has index notation (which I'm currently trying to improve) so I actually I don't think defining metrics, Christoffel symbols, the Levi-Civita connection etc. would be that hard. Although nevertheless this may not be the best place to start.

Best wishes,
Joseph.

[Joseph Tooby-Smith]

I'm not sure if this helps or hinders - if the latter feel free to complete ignore these. But I've added some informal results related to the FLRW metric. For example:

• semiformal_result (6ZZLH): SpatialGeometry

The others can be found at the same place.

[Pedro Bessa]

Hello Joseph,

Thank you for the clarification, I believe I understand more or less how to proceed then - modularity should be the way then, since we want to be flexible enough so that our codes can later depend on more involved definitions.
I believe I can write out the basics needed for a full description of the Friedmann equations and some of the main results coming from the dynamics. I'll try to structure the main results more or less in the same fashion as you did in the TODO list.

Joseph Tooby-Smith said:

I'm not sure if this helps or hinders - if the latter feel free to complete ignore these. But I've added some informal results related to the FLRW metric. For example:

• semiformal_result (6ZZLH): SpatialGeometry

The others can be found at the same place.

Can I add TODO items and informal definitions? Or is the procedure to first git branch the code and then merge?

Thank you and I hope I can be of help to the project,

Pedro

[Joseph Tooby-Smith]

Hi @Pedro Bessa , great!

Please do add TODO items and informal definitions!

You can either fork the repo and make a pull-request that way, or I can give you write access so you can make a brach and make pull-requests from branches. If the latter works better for you - could you let me know your GitHub username.

In either case, please do make pull-requests even if they only contain TODO items and informal definitions. This is still extremely useful.

Thanks,
Joseph.

[Winston Yin (尹維晨)]

@Pedro Bessa I just saw your message and wanted to say hi! My PhD was in cosmology as well (I develop statistical/observational methods for measuring birefringence), so our interests may align. I've thought throughout my PhD if I could incorporate formalisation in my work somehow, but the goals of the two communities seem to have little overlap as of now.

In terms of Lean work, my approach has been to lay the mathematical groundwork for stating advanced things in physics. That's why I'm building up the differential geometry and dynamical systems libraries. We don't even have solutions to various standard differential equations! I agree with @Joseph Tooby-Smith that the deficiency of such libraries should not block applications to physics, but it does mean that certain problems / statements in physics are more immediately amenable to formalisation than others.

Please keep us updated on your formalisation attempts!

[Kevin Buzzard]

This feels a bit like how mathlib felt when I started doing mathematics; it was a million miles away from anything I found interesting. Maybe choose some appropriate cool targets, solve them, and advertise their solutions in the physics commodity in an attempt to get more adherents?