Stream: math-comp devs

Topic: Student projects

Bas Spitters (Oct 25 2023 at 08:23):

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?

Huỳnh Trần Khanh (Oct 25 2023 at 11:59):

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

Huỳnh Trần Khanh (Oct 25 2023 at 12:00):

even mathlib doesn't have this

Cyril Cohen (Oct 25 2023 at 13:22):

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.

Cyril Cohen (Oct 25 2023 at 13:27):

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

Bas Spitters (Oct 26 2023 at 08:22):

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.)

Cyril Cohen (Oct 26 2023 at 08:26):

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.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.)

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.

Cyril Cohen (Oct 26 2023 at 08:27):

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

Last updated: Oct 13 2024 at 01:02 UTC