# Zulip Chat Archive

## Stream: new members

### Topic: Starting with formalizing undergraduate math

#### Chris M (Jun 16 2020 at 11:34):

Johan Commelin said:

I still think that some topic like this is the easiest way to get started (Chris M)

I just happen not to be very interested in this topic, so I wouldn't be as motivated to keep going.

#### Johan Commelin (Jun 16 2020 at 11:35):

Ok, that's fine (-;

#### Johan Commelin (Jun 16 2020 at 11:35):

Then we should find some other topic. I suggested it because it's somewhat "algebraic".

#### Chris M (Jun 16 2020 at 11:36):

Johan Commelin said:

I think that in a typical argument in probability theory there is a lot of stuff going on that works just fine, but that you can't turn into a formal argument without completely changing the structure of the proof beyond recognition.

Could you point to roughly an example of the type of thing that becomes difficult when you start to formalize? Just out of curiosity, I'm not set on doing probability theory.

#### Johan Commelin (Jun 16 2020 at 11:36):

Bigger project: classification of platonic solids ??

#### Chris M (Jun 16 2020 at 11:37):

Johan Commelin said:

Then we should find some other topic. I suggested it because it's somewhat "algebraic".

Would topics in multivariate differential calculus be bad?

#### Johan Commelin (Jun 16 2020 at 11:42):

Sounds like it might be hard

#### Johan Commelin (Jun 16 2020 at 11:42):

But I'm not the right person to ask

#### Sebastien Gouezel (Jun 16 2020 at 11:42):

Something we don't have, but for which you don't need any new definition: the second derivative of a `C^2`

function on a real vector space is symmetric (or more generally the `n`

-th derivative is symmetric). (I don't even know what the right generality for this is, i.e., does it work on any nondiscrete normed field, but just proving it over the reals would already be a nice project).

#### Sebastien Gouezel (Jun 16 2020 at 11:43):

Or, state and prove that a `C^k`

function is approximated by its `k`

-th Taylor series up to `o(norm(h) ^ k)`

.

#### Johan Commelin (Jun 16 2020 at 11:44):

Another idea: "Commuting operators are simultatneously diagonalizable"

#### Sebastien Gouezel (Jun 16 2020 at 11:45):

This one needs a definition of diagonalizable first, no? And you are missing an assumption :-)

#### Johan Commelin (Jun 16 2020 at 11:45):

I just gave a slogan (-;

#### Johan Commelin (Jun 16 2020 at 11:46):

But yes, this might actually be a tricky project. Because we don't have eigenspaces/vectors in mathlib yet.

#### Johan Commelin (Jun 16 2020 at 11:46):

Someone had them, but it hasn't been PRd yet.

#### Johan Commelin (Jun 16 2020 at 11:46):

@orlando Are you planning to PR your eigen* stuff?

#### orlando (Jun 16 2020 at 12:06):

Hello @Johan Commelin Yes ! @Patrick Massot explain me how to PR ! I'm taking a little vacation. But I do things on the eigenvalues and characteristic polynomial

#### Johan Commelin (Jun 16 2020 at 12:06):

Tres bien!

#### Johan Commelin (Jun 16 2020 at 12:06):

Enjoy your holiday!

#### orlando (Jun 16 2020 at 12:07):

Thx mountain :grinning_face_with_smiling_eyes:

Last updated: May 09 2021 at 18:17 UTC