Matthew Dawson

Stream: new members

[Matthew Dawson]

Dear Lean/Mathlib community,

I am a mathematician from a representation theory / non-commutative harmonic analysis background. I am a complete novice to formal theorem provers, but do have experience (and formal training as an undergraduate) in using traditional procedural programming languages. I became interested in Lean and mathlib after seeing that people have been formalizing modern mathematical analysis in it.

From what I have read, this community appears to have grown quite a bit in size over the past four or five years, and I am somewhat curious as to whether there is still "room" for more people to join and actively work on extending the library. I am particularly curious as to whether anyone is working on, say, formalizing the general results from harmonic analysis on locally-compact groups or perhaps something like the Plancherel Theorem for semisimple Lie groups. And, if not, does this sound like a goal worth attempting?

Maybe these are naïve questions on my part. I offer my apologies in advance.

Sincerely,
Matthew Dawson
CONAHCYT Research Fellow
Centro de Investigación en Mathematics (CIMAT)
Mérida, Yucatán, México

[Matthew Dawson]

P.S. I am currently working through "Theorem Proving in Lean 4". So for sure I will almost certainly not make any meaningful contribution of any kind for quite some time (if ever!).

[mars0i]

I'm not part of the Mathlib community--I'm interested in Lean for other reasons--and no doubt you'll get more specific answers about your areas of interest. I hope I am not speaking out of turn, but I've seen enough know that there definitely is room for more people to contribute to Mathlib.

[Johan Commelin]

@Matthew Dawson Welcome! There's definitely room for more people. We have Lie groups, but not yet semisimple ones. What other resources have you been using besides #tpil? Do you know about #nng and #mil?

[Matthew Dawson]

Thanks very much for your kind replies, @mars0i and @Johan Commelin.

As far as the other resources, I am aware of Mathematics in Lean and my plan had been to work through it after finishing Theorem Proving in Lean. But maybe I should do both at the same time? I was not aware of the Natural number Game, which I will definitely check out!

[Kevin Buzzard]

We need the trace formula so we can get cyclic base change for GL(2) so we can prove Fermat's Last Theorem! So definitely more harmonic analysis people needed :-)