I have a student who has done my course using software foundations. He would like to a small (10ECTS) project formalizing mathematics in math-comp. Is there a list of open problems ? Any concrete suggestions of what is missing from the library?

given an n*m grid, starting point is top left, destination is bottom right, player can only move right or down, how many paths are there

even mathlib doesn't have this

Bas Spitters said:

I have a student who has done my course using software foundations. He would like to a small (10ECTS) project formalizing mathematics in math-comp. Is there a list of open problems ? Any concrete suggestions of what is missing from the library?

I would like to have in mathcomp:

- the quadractic law of reciprocity (thm 7 from freek's list but in mathcomp)
- some convergence tests in mathcomp analysis. E.g. Cauchy's or Bertrand's (I do not know the english name of this family of sequences), or with lower priority IMO, d'Alembert's or Abel's tests.

also

- https://en.wikipedia.org/wiki/Partial_fraction_decomposition in mathcomp (algebra/field packages)
- (Start) Build(ing) a dictionary of usual integrals: https://en.wikipedia.org/wiki/Lists_of_integrals (some of which rely on the previous item) in mathcomp analysis

Thanks @Cyril Cohen ! Quadratic reciprocity might be a fun one.

We recently worked on this using fiat-crypto in our CCS paper.

https://eprint.iacr.org/2023/1261.pdf

It might also be a good excuse to revisit some of the questions on combining MC and the stdlib. I know mczify, have you tried Trocq to make such connections (It's been a while since I looked at the paper.)

Bas Spitters said:

Thanks Cyril Cohen ! Quadratic reciprocity might be a fun one.

We recently worked on this using fiat-crypto in our CCS paper.

https://eprint.iacr.org/2023/1261.pdfIt might also be a good excuse to revisit some of the questions on combining MC and the stdlib. I know mczify, have you tried Trocq to make such connections (It's been a while since I looked at the paper.)

For now Trocq is still at the stage of proof of concept: we are still far from a release, but it's very promising to me so I intend to work towards a stable release during 2024.

(In particular Trocq is now working solely on top of HoTT, but I am writing the Vanilla version too)

Last updated: Jul 23 2024 at 20:01 UTC