Starting with formalizing undergraduate math

Stream: new members

[Chris M]

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]

Ok, that's fine (-;

[Johan Commelin]

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

[Chris M]

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]

Bigger project: classification of platonic solids ??

[Chris M]

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]

Sounds like it might be hard

[Johan Commelin]

But I'm not the right person to ask

[Sebastien Gouezel]

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]

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]

Another idea: "Commuting operators are simultatneously diagonalizable"

[Sebastien Gouezel]

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

[Johan Commelin]

I just gave a slogan (-;

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[orlando]

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]

Tres bien!

[Johan Commelin]

Enjoy your holiday!

[orlando]

Thx mountain :grinning_face_with_smiling_eyes: