Zulip Chat Archive

Stream: new members

Topic: Starting with formalizing undergraduate math


view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 16 2020 at 11:35):

Ok, that's fine (-;

view this post on Zulip Johan Commelin (Jun 16 2020 at 11:35):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 16 2020 at 11:36):

Bigger project: classification of platonic solids ??

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jun 16 2020 at 11:42):

Sounds like it might be hard

view this post on Zulip Johan Commelin (Jun 16 2020 at 11:42):

But I'm not the right person to ask

view this post on Zulip 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).

view this post on Zulip 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).

view this post on Zulip Johan Commelin (Jun 16 2020 at 11:44):

Another idea: "Commuting operators are simultatneously diagonalizable"

view this post on Zulip Sebastien Gouezel (Jun 16 2020 at 11:45):

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

view this post on Zulip Johan Commelin (Jun 16 2020 at 11:45):

I just gave a slogan (-;

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 16 2020 at 11:46):

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

view this post on Zulip Johan Commelin (Jun 16 2020 at 11:46):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jun 16 2020 at 12:06):

Tres bien!

view this post on Zulip Johan Commelin (Jun 16 2020 at 12:06):

Enjoy your holiday!

view this post on Zulip orlando (Jun 16 2020 at 12:07):

Thx mountain :grinning_face_with_smiling_eyes:


Last updated: May 09 2021 at 18:17 UTC