Stream: math-comp devs

Topic: Student projects


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

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

view this post on Zulip Huỳnh Trần Khanh (Oct 25 2023 at 12:00):

even mathlib doesn't have this

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

view this post on Zulip Cyril Cohen (Oct 25 2023 at 13:27):

also

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

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

view this post on Zulip 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: Jul 23 2024 at 20:01 UTC