Interest in Optics

Stream: PhysLean

[ZhiKai Pong]

Hi, I'm a PhD student in optical engineering writing up my thesis, and I've been wanting to try my hands at lean for a while now but haven't really got the time. The mathematical side of formalization does seem to be a bit too intimidating especially for someone without proper mathematical training like myself, and I came across PhysLean which looks much more familiar to what I know. Joseph just posted #PhysLean > Mini projects a couple days ago, I had a look at the linked page and I'm curious as to whether it is something suitable for a beginner to get started.

To be more specific, what is the expected expertise to start working on such a project? Is there a concrete plan on what is expected to be formalized, and how would one begin to contribute to this project? Many thanks!

[Joseph Tooby-Smith]

Hey @ZhiKai Pong, nice to meet you! I you are doing a phd in optical engineering I think you have more than enough expertise to start this project! I think it would be good for a beginner because a lot of the 'translating things into type theory' has been done for you.

There is a corresponding paper here: https://arxiv.org/pdf/1403.3039

I think as a first goal formalizing the definitions and results from this paper (/convert them into lean) and build the corresponding theorems and lemmas and documentation around it would be good! Although you probably know more about the area then I do - so perhaps there is more interesting things to be done here.

No one else that I know of has started this, so its really up to you how you start.

As a starting step, one could write the results into PhysLean using informal_lemma and informal_definition. These can be used to write english versions of the results and plan what needs doing without having

I would recommend contributing to PhysLean in small steps - don't wait until the end to PR it. I'm happy to help in anyway I can :)

[ZhiKai Pong]

Thanks Joseph! I'm submitting my thesis end of April (fingers crossed) and I hope to start working on this afterwards, will try to read the paper as a starting point and see how it goes from there!

[Joseph Tooby-Smith]

Good luck with your thesis! :)

[Alex Meiburg]

Nice! I'm also happy to try to offer some support if necessary. :) I glanced at your Google Scholar profile a bit. Do you have a particular idea of things you'd like to try to write down?

I'm not in optics, but maybe something like - a theory of some basic optical field configurations, some operations on them, and then some proofs about how they compose? (Like how polarizers compose etc.)
Looking at https://www.nature.com/articles/s41377-024-01659-z it would be very cool to formalize some ideas about topologically protected states, like formalizing the notion of Skyrmion number. You could plug into the rich topology theory in Mathlib. I'm sure there are other mathy people that would be happy to help with that too

[ZhiKai Pong]

Thanks Alex, I wasn't prepared to be scrutinized so soon haha! the short story is that my PhD topic (on direct laser writing) isn't actually on this, instead I'm going to join the team afterwards as a postdoc and work on developing the theory and applications for optical Skyrmions.

Part of my motivation to do lean is to actually make sure I go through the maths here :sweat_smile: I'm only scratching the surface of the maths side of this area and still have a lot more to learn, so I'm not sure when I'll be able to actually formalize these results. Nevertheless, the maths required (I believe) is actually laid out quite detailedly in the methods section of the paper, so yes that's a goal that hopefully I'll be able to formalize that in the not-too-distant future. From my observation this is still a relatively new area where the people working on it don't really understand the maths, and people who know the maths aren't in this area, so maybe having lean say "look this is proven correct" would make the results more convincing.

I'd imagine what I want to do for a short term goal is something like this:

Starting from Maxwell's equations ->
define free space propagation (wave equations etc.) ->
define polarization in terms of Stokes parameters and Muller matrices ->
define optical components (polarizers, waveplates etc.) in terms of Muller matrices and show that their action on stokes parameter is as expected

and then maybe move on to more fancy stuff like topological properties of optical Skyrmions. otherwise it might also be possible to try something that's more established such as OAM light via Laguerre–Gaussian modes.

Another branch of optics that I'm interested in is waveguide theory, but I feel that's much more complicated (Bessel functions, boundary conditions etc.) and might leave that for later.

Given this I'm probably more interested in wave and electromagnetic optics, but if there's interest in geometrical/quantum optics I'm open to discussions and see how I can contribute as well :)

[Alex Meiburg]

It looks like Bessel functions aren't even in Mathlib! Which is kinda funny. I guess they feel kind of "old school" math in certain ways - and they're very useful for numerics and asymptotic analysis, but I guess they're not so crucial for mathematical proofs (in the sense of Mathlib) as much.

Like I said, I don't know much about optics ... I didn't know what Muller matrices were until you mentioned them. (Although, upon a quick Google, they look familiar...) I think defining them and proving basic facts about them would be a great and easy first item. Then you could prove how they work with Maxwell's equations, "linking up" different topics. Of course that's just my suggestion, no need to do that necessarily

[Alex Meiburg]

Like, you could prove that a series of perfect linear polarizers leads has 0 transmission, if and only if some adjacent pair of polarizers is off by 90 degrees. That would be cool

[Alex Meiburg]

I mean, very basic fact. But I think it'd be cool!

[ZhiKai Pong]

Alex Meiburg said:

Like, you could prove that a series of perfect linear polarizers leads has 0 transmission, if and only if some adjacent pair of polarizers is off by 90 degrees. That would be cool

Muller matrices (or Jones matrices) is a tool that allows you to do exactly that! Your statement is equivalent to stating a product of matrices

$$\left(\begin{matrix}\cos^2(\theta_1) \quad \cos(\theta_1)\sin(\theta_1)\\ \cos(\theta_1)\sin(\theta_1) \quad \sin^2(\theta_1)\end{matrix}\right)\left(\begin{matrix}\cos^2(\theta_2) \quad \cos(\theta_2)\sin(\theta_2)\\ \cos(\theta_2)\sin(\theta_2) \quad \sin^2(\theta_2)\end{matrix}\right)\cdots\left(\begin{matrix}\cos^2(\theta_n) \quad \cos(\theta_n)\sin(\theta_n)\\ \cos(\theta_n)\sin(\theta_n) \quad \sin^2(\theta_n)\end{matrix}\right) = \left(\begin{matrix}0 \quad 0 \\ 0 \quad 0\end{matrix}\right)$$

if and only if there exists a pair of $\theta_a, \theta_{a+1}$ with $\lvert\theta_a - \theta_{a+1}\rvert = \pi/2$

So the mathematical language for stating these kinds of scenarios is actually there I just have to figure out how to translate it into lean!

[Kevin Buzzard]

Bessel functions will be needed for non-holomorphic modular forms but we're only just getting our head around the holomorphic case for now

[ZhiKai Pong]

Hi @Joseph Tooby-Smith , I'm trying to set up PhysLean, when I run "lake exe cache get" I got an error saying

 error: compiled configuration is invalid; run with '-R' to reconfigure

Is this a repository issue or a lean issue? there's some related discussion at #mathlib4 > lake exe cache get error but there doesn't seem to be an explicit fix, let me know if I should ask over there.

[Joseph Tooby-Smith]

I don't think this is a PhysLean issue. The penultimate comment to the discussion you linked to said says that removing the .lake might work, so something like:

rm -rf .lake
lake update
lake exe cache get
lake build

[ZhiKai Pong]

oh nevermind, just running lake update works

[ZhiKai Pong]

A more general question: I had a look at SciLean and seems like it could be useful (say working with differential equations), but it's still relatively empty at the moment. May I ask is SciLean expected to be part of the ecosystem, or is it better to stick with what mathlib offers for the time being?

[Joseph Tooby-Smith]

Hey! So ideally I think PhysLean should sit downstream of SciLean and have it be part of the ecosystem.

I think right now there are two technical barriers that I see to including it right now (maybe this is something @Tomas Skrivan can also comment on) .

• The rate at which Lean and Mathlib update mean that PhysLean and SciLean are not on the same versions as each other (and I think therefore it won't actually work if you try and import SciLean into PhysLean).
• SciLean introduces some axioms like sorryProofAxiom which circumvent needing proofs. This is fine, but ideally I would like to keep PhysLean sorry free. This is solvable by having linters which check theorems for these axioms, but this is something which would nee implementing.

[Tomas Skrivan]

I think SciLean should as PhysLean just have specific commits that depend on mathlib with a specific tag. This way you should be able to depend on both projects.

[Joseph Tooby-Smith]

This would be good!

The problem I have with these specific tags is that for mathlib they appear quite far apart in terms of development. That is to say, a lot has happened in mathlib between the tag v4.18.0-rc1 (which PhysLean is currently on) and v4.18.0 (which it needs upgrading to), meaning that every time I want to bump PhysLean its a fair amount of work. We could bump PhysLean to one of the nightly builds but then it would potentially become out of 'sync' with other projects (maybe not so much an issue though).

[Kevin Buzzard]

We bump FLT weekly, I think it's the only way to survive. The quicker you bump the fewer problems you have to deal with.