Hello, I've been recently learning more about Coq and SSReflect, and wanted to strengthen my knowledge by contributing to this project. Any topics that would be good for a newbie? I just read the Mathematical Components book and I know basic (undergraduate) analysis.

Welcome! I've found this to be a great project for learning more about coq, and formalization in general. There's plenty of undergrad analysis we still don't have, so I'm sure there's a suitable topic for you. Of course asking for help is encouraged (more like required. It's tough stuff for all of us!).

Here are some areas I've been thinking about recently. These are definitely challenges, but hopefully rewarding ones.

- In the topology realm, separation axioms are a thing we only kinda have. Just defining the hierarchy of Hausdorff, regular, normal, etc is a solid challenge. Proving the "easy" implications (EG normal implies regular) may be nice intro proofs. But I'd love to see a PR with just the definitions.
- for more real number focused stuff, apparently we don't have Taylor's theorem. That's non-trivial for sure. Even stating it is a good challenge. Definitely more of a long-term goal than a good first PR.
- We have a notion of exp, but not of log. Doing the theory of (R->R) logarithms, a first PR with its definition as the inverse of exp, is perhaps approachable.

Definitely the third one seams the easiest haha but I'll try to explore at least a bit of each suggestion, thanks!

Agreed. I'll think on this a bit more as well. Others should definitely chime in too, if there's an better candidate.

Good luck! Please do reach out here with any questions. Personally, I'm always happy to talk about math, and eager to hear about first-time experiences with the library.

hmmm I think there's some basic facts about (natural) logarithms in `exp.v`

(`Definition ln x`

), in fact I think all the useful ones are already there

I think only thing that's missing is its integral, or maybe did you mean something else?

There are some recent lecture notes specifically about MC-A: https://www.math.nagoya-u.ac.jp/~garrigue/lecture/2022_affeldt/index.html

oh they look great, thanks!

I think there's some basic facts about (natural) logarithms

Ah, my bad. I totally forgot that existed. Logs of other bases is certainly a nice generalization. Having the example of `ln`

to work from is probably helpful too.

What about the continuity of x |-> x * ln x?

(or more generally properties of ln useful to deal with Shannon's entropy)

Last updated: Jun 22 2024 at 15:01 UTC