Where to start getting my hands a bit dirty

Stream: new members

[Keith Rush]

Hi all,

My name is Keith Rush, and I'm excited to have discovered Lean and its community.

My background is as a mathematician--in the circle of stuff around real and harmonic analysis, mathematical physics, and approximation theory. These days however I tend to work more with empirics than theory, particularly with ML and AI things. (I was in grad school during the deep learning revolution, which is what convinced me I needed to actually learn how to program and build systems).

I've always retained a soft spot for the concerns of mathematics, though I've gone a bit far afield. I'm the type of nerd who got very excited upon finding Lean and its capabilities, so the last week or so I've been poking around mathlib, playing through the NNG, and working through a couple simple examples. From my time in programming, though, I tend to feel there is no better approach to learning something new than just tackling a real problem or two, nevermind the fact that one is likely to flail for a while (and possibly just fail).

So I'm curious: is there a natural way or place for someone like me to start getting their hands dirty? I thought about formalizing some of the proofs from my recent works as an exercise (which, from a mathematical perspective, are pretty elementary). But I figured that this may be too difficult, and perhaps might require chasing some things down that I'm not prepared for (e.g., it's not obvious to me if the square root of a positive definite matrix is defined anywhere). So I'm wondering if anyone has experience in a similar situation--should I just 'take direction' from someone and attempt some basic contributions (e.g. some stuff in calculus that is known to be needed but maybe doesn't exist yet), or have others successfully just 'formalized backwards' from work they are familiar with (like their own)?

[Yaël Dillies]

Welcome! :wave: Squareroot of a positive matrix was just done by a student of @David Loeffler

[Keith Rush]

Awesome! I realize now I was poking around mathlib instead of mathlib4 :smile:

[Josha Dekker]

I started very recently as well, I just went through the list of issues on GitHub and checked if there was something that I knew how to do/for which I knew the math, and started doing that!