Kalle Kytölä

Stream: new members

[Kalle Kytölä]

Hello everyone!

This is me, Kalle Kytölä := by refl.

I consider myself a mathematical physicist --- which could of course mean just about anything... So more specifically I work on certain two-dimensional statistical physics models and related conformal field theories. To a mathematician that might still not be particularly informative, so as a good first approximation what I do is probability theory and representation theory.

I am not yet a complete beginner at formalization, but I (might) aspire to become one.

[Kalle Kytölä]

I think there's something about this stuff in general, but I specifically got hooked by the Natural Number Game and the super helpful atmosphere here on this Zulip chat.

Btw, for those fortunate enough to have the NNG ahead of them --- don't wait, it's amazing! One part of it just completely blew my mind (in a good way). Overall, it is just a really well designed puzzle game, and absolutely impeccably and insightfully narrated! I think it should be nominated for a ... well I don't know if there are prizes in that category, but it is the best natural number game I ever saw. Thank you so much, Kevin Buzzard and Mohammad Pedramfar!

Looking for a sequel to the NNG, I also did half of Kevin Buzzard's course so far. I look forward to a few more spare moments to look at the rest of it.

Inspired by those, I finally did my first own attempts at formalizing something I thought should be sufficiently easy. And well, I was wrong.

[Scott Morrison]

(Part of my mathematical background is in topological phases --- e.g. modular tensor categories, fusion categories, etc, so not-so-far from what you do. I'd be really excited to see some more physically-motivated maths coming to Lean!)

[Kalle Kytölä]

Yeah, not that far from the topics!

I hope to finish some work in the near future about braided tensor category structure of a (certain) category of modules of a generic Virasoro vertex operator algebra (not the rational VOAs of the minimal models, but slightly more badly behaved ones). And a dream would be to formalize something to that direction, but I'll probably start from something else :grinning_face_with_smiling_eyes:.

Still, much of what I do is probability, which is quite different :smile:.

[Bryan Gin-ge Chen]

Welcome! I was once a condensed matter theorist, and while I never worked with CFTs directly in my research, I did learn enough about them to be fascinated by their "magic". I think your research topics are closely related to those of @Vincent Beffara, who was hanging out here a bit (though sadly he hasn't been active in about a year; hopefully this ping is not unwelcome).

As far as I know, we only have a very small amount of probability theory in mathlib at the moment. Maybe @Rémy Degenne, @Martin Zinkevich and @Floris van Doorn can say a bit about what's there and what's to come?

[Kalle Kytölä]

Is @Vincent Beffara here?!? Wow. Hi!

Because among the people I imagined might have an interest in trying to formalize similar things, he was actually the first who came to my mind (and he is certainly more competent with computers than I am). But I never talked with him about this yet :speechless:.

Thanks for pointing out, superb!

[Floris van Doorn]

I was also asked in a private meddage by @Joao Bregunci about probability theory, so let me reply to both Joao and @Kalle Kytölä about the state of probability theory in Lean.

There is quite an extensive library of measure theory in Lean, with a lot of properties about measures and integrals. Probability distributions are a special case of measures, which are defined here: docs#measure_theory.probability_measure. However, there is not much work on probability theory specifically yet. The probability folder only contains 2 files:

• independence.lean about independent sets and (more generally) independent sigma-algebras.
• integration.lean which mostly contains the proof that independent random variables satisfy E[f * g] = E[f] * E[g]. As you can see, the statement of this fact (docs#probability_theory.lintegral_mul_eq_lintegral_mul_lintegral_of_indep_fun) doesn't look very "probabilistic" yet. Though we could add notations like 𝔼 f := ∫⁻ x, f x.
  So there isn't much probability theory yet, though of course we also have many facts about probabilities that hold for general measures (the additivity of expected values, for example).

But if you want to extend the library, you can add - for example - variance, standard deviation, covariance, cumulants, conditional probability (which will be a multiple of docs#measure_theory.measure.restrict), martingales (which will be significantly harder), or your favorite theorem from probability theory.
I don't know what's coming in probability theory, I'm not working on anything in probability myself, at the moment.

[Joao Bregunci]

Thanks for replying Floris. I am going to take a look at the measure theory library and see if there is a way in which I can meaningfully contribute. One of my only worries for now is that I've seen a Lean library called Formal ML that seems to do a lot in the ways of formalizing probability from @Martin Zinkevich. I wanted to know if there any plans to incorporate any part of Formal ML in the Mathlib (Martin as already contributed Probability Theory in Lean also).

[Kalle Kytölä]

Thank you Floris! This is very useful information!

To be very clear, I will not anytime soon reach a level where I can actually contribute, so for now I'm just creating exercises for myself (and I keep getting stuck at the syntax).

That said, one reason I chose conditional expected values as my first exercise is that if conditional expected values could be formalized, then much of discrete time martingale theory does not appear an awful lot harder (?). And martingale theory would have some really nice consequences (including an alternative proof of the Radon-Nikodym theorem, although I heard from Heather Macbeth that a proof of it is already being PR'd). Anyways, my level is far from a contributor, so right now I'm treating these as just additional levels of the NNG. If and when someone serious independently does the mathlib version of the topics I'm playing with, that's great for everyone.

[Jason Rute]

There is a nice martingale proof also of the SLLN.

[Heather Macbeth]

Joao Bregunci said:

One of my only worries for now is that I've seen a Lean library called Formal ML that seems to do a lot in the ways of formalizing probability from Martin Zinkevich. I wanted to know if there any plans to incorporate any part of Formal ML in the Mathlib (Martin as already contributed Probability Theory in Lean also).

Martin can probably tell you more himself, but I believe his plan is to gradually PR the material from his Formal ML library into mathlib.

[Heather Macbeth]

Actually ... maybe he would be glad of some help on this!

[Joao Bregunci]

Heather Macbeth , if this is his plan I would love to help him if possible. Do you know how can I reach him? He seems to not be here on Zulip as of recently...

[Heather Macbeth]

It's a good question! He makes PRs on mathlib from time to time so maybe Github is a better place to reach him, or maybe someone like @Rémy Degenne who has reviewed his work often will have a better idea.

[Heather Macbeth]

I am not sure what the etiquette here is, not to mention the ethics and the law -- if a person writes a Lean package under an open-source license (as Martin did with FormalML), is it ok for someone else to PR parts of it, keeping the copyright and authorship intact?

[Heather Macbeth]

It would certainly be very nice to get the rest of Martin's work into mathlib.